Documentation

Mathlib.Topology.Algebra.Constructions.DomMulAct

Topological structure on DomMulAct _ #

In this file we define topology on DomMulAct _ and prove basic facts about this topology. The topology on Mᵈᵐᵃ is the same as the topology on M (formally, it is induced by DomMulAct.mk.symm, since the types aren't definitionally equal).

source
instance DomAddAct.instTopologicalSpace {M : Type u_1} [TopologicalSpace M] :
TopologicalSpace Mᵈᵃᵃ
Equations
source
instance DomMulAct.instTopologicalSpace {M : Type u_1} [TopologicalSpace M] :
TopologicalSpace Mᵈᵐᵃ
Equations
source
theorem DomAddAct.continuous_mk {M : Type u_1} [TopologicalSpace M] :
Continuous ⇑DomAddAct.mk
source
theorem DomMulAct.continuous_mk {M : Type u_1} [TopologicalSpace M] :
Continuous ⇑DomMulAct.mk
source
theorem DomAddAct.continuous_mk_symm {M : Type u_1} [TopologicalSpace M] :
Continuous ⇑DomAddAct.mk.symm
source
theorem DomMulAct.continuous_mk_symm {M : Type u_1} [TopologicalSpace M] :
Continuous ⇑DomMulAct.mk.symm
source
theorem DomAddAct.mkHomeomorph.proof_1 {M : Type u_1} [TopologicalSpace M] :
Continuous DomAddAct.mk.toFun
source
def DomAddAct.mkHomeomorph {M : Type u_1} [TopologicalSpace M] :
M ≃ₜ Mᵈᵃᵃ

DomAddAct.mk as a homeomorphism

Equations
  • DomAddAct.mkHomeomorph = { toEquiv := DomAddAct.mk, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
    source
    theorem DomAddAct.mkHomeomorph.proof_2 {M : Type u_1} [TopologicalSpace M] :
    Continuous DomAddAct.mk.invFun
    source
    @[simp]
    theorem DomAddAct.mkHomeomorph_toEquiv {M : Type u_1} [TopologicalSpace M] :
    DomAddAct.mkHomeomorph.toEquiv = DomAddAct.mk
    source
    @[simp]
    theorem DomMulAct.mkHomeomorph_toEquiv {M : Type u_1} [TopologicalSpace M] :
    DomMulAct.mkHomeomorph.toEquiv = DomMulAct.mk
    source
    def DomMulAct.mkHomeomorph {M : Type u_1} [TopologicalSpace M] :
    M ≃ₜ Mᵈᵐᵃ

    DomMulAct.mk as a homeomorphism.

    Equations
    • DomMulAct.mkHomeomorph = { toEquiv := DomMulAct.mk, continuous_toFun := ⋯, continuous_invFun := ⋯ }
    Instances For
      source
      @[simp]
      theorem DomAddAct.coe_mkHomeomorph {M : Type u_1} [TopologicalSpace M] :
      ⇑DomAddAct.mkHomeomorph = ⇑DomAddAct.mk
      source
      @[simp]
      theorem DomMulAct.coe_mkHomeomorph {M : Type u_1} [TopologicalSpace M] :
      ⇑DomMulAct.mkHomeomorph = ⇑DomMulAct.mk
      source
      @[simp]
      theorem DomAddAct.coe_mkHomeomorph_symm {M : Type u_1} [TopologicalSpace M] :
      ⇑DomAddAct.mkHomeomorph.symm = ⇑DomAddAct.mk.symm
      source
      @[simp]
      theorem DomMulAct.coe_mkHomeomorph_symm {M : Type u_1} [TopologicalSpace M] :
      ⇑DomMulAct.mkHomeomorph.symm = ⇑DomMulAct.mk.symm
      source
      theorem DomAddAct.inducing_mk {M : Type u_1} [TopologicalSpace M] :
      Inducing ⇑DomAddAct.mk
      source
      theorem DomMulAct.inducing_mk {M : Type u_1} [TopologicalSpace M] :
      Inducing ⇑DomMulAct.mk
      source
      theorem DomAddAct.embedding_mk {M : Type u_1} [TopologicalSpace M] :
      Embedding ⇑DomAddAct.mk
      source
      theorem DomMulAct.embedding_mk {M : Type u_1} [TopologicalSpace M] :
      Embedding ⇑DomMulAct.mk
      source
      theorem DomAddAct.openEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      OpenEmbedding ⇑DomAddAct.mk
      source
      theorem DomMulAct.openEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      OpenEmbedding ⇑DomMulAct.mk
      source
      theorem DomAddAct.closedEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      ClosedEmbedding ⇑DomAddAct.mk
      source
      theorem DomMulAct.closedEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
      ClosedEmbedding ⇑DomMulAct.mk
      source
      theorem DomAddAct.quotientMap_mk {M : Type u_1} [TopologicalSpace M] :
      QuotientMap ⇑DomAddAct.mk
      source
      theorem DomMulAct.quotientMap_mk {M : Type u_1} [TopologicalSpace M] :
      QuotientMap ⇑DomMulAct.mk
      source
      theorem DomAddAct.inducing_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Inducing ⇑DomAddAct.mk.symm
      source
      theorem DomMulAct.inducing_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Inducing ⇑DomMulAct.mk.symm
      source
      theorem DomAddAct.embedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Embedding ⇑DomAddAct.mk.symm
      source
      theorem DomMulAct.embedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      Embedding ⇑DomMulAct.mk.symm
      source
      theorem DomAddAct.openEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      OpenEmbedding ⇑DomAddAct.mk.symm
      source
      theorem DomMulAct.openEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      OpenEmbedding ⇑DomMulAct.mk.symm
      source
      theorem DomAddAct.closedEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      ClosedEmbedding ⇑DomAddAct.mk.symm
      source
      theorem DomMulAct.closedEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
      ClosedEmbedding ⇑DomMulAct.mk.symm
      source
      theorem DomAddAct.quotientMap_mk_symm {M : Type u_1} [TopologicalSpace M] :
      QuotientMap ⇑DomAddAct.mk.symm
      source
      theorem DomMulAct.quotientMap_mk_symm {M : Type u_1} [TopologicalSpace M] :
      QuotientMap ⇑DomMulAct.mk.symm
      source
      instance DomAddAct.instT0Space {M : Type u_1} [TopologicalSpace M] [T0Space M] :
      T0Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT0Space {M : Type u_1} [TopologicalSpace M] [T0Space M] :
      T0Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT1Space {M : Type u_1} [TopologicalSpace M] [T1Space M] :
      T1Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT1Space {M : Type u_1} [TopologicalSpace M] [T1Space M] :
      T1Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :
      T2Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :
      T2Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT25Space {M : Type u_1} [TopologicalSpace M] [T25Space M] :
      T25Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT25Space {M : Type u_1} [TopologicalSpace M] [T25Space M] :
      T25Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT3Space {M : Type u_1} [TopologicalSpace M] [T3Space M] :
      T3Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT3Space {M : Type u_1} [TopologicalSpace M] [T3Space M] :
      T3Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT4Space {M : Type u_1} [TopologicalSpace M] [T4Space M] :
      T4Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT4Space {M : Type u_1} [TopologicalSpace M] [T4Space M] :
      T4Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instT5Space {M : Type u_1} [TopologicalSpace M] [T5Space M] :
      T5Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instT5Space {M : Type u_1} [TopologicalSpace M] [T5Space M] :
      T5Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instR0Space {M : Type u_1} [TopologicalSpace M] [R0Space M] :
      R0Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instR0Space {M : Type u_1} [TopologicalSpace M] [R0Space M] :
      R0Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instR1Space {M : Type u_1} [TopologicalSpace M] [R1Space M] :
      R1Space Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instR1Space {M : Type u_1} [TopologicalSpace M] [R1Space M] :
      R1Space Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instRegularSpace {M : Type u_1} [TopologicalSpace M] [RegularSpace M] :
      RegularSpace Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instRegularSpace {M : Type u_1} [TopologicalSpace M] [RegularSpace M] :
      RegularSpace Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instNormalSpace {M : Type u_1} [TopologicalSpace M] [NormalSpace M] :
      NormalSpace Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instNormalSpace {M : Type u_1} [TopologicalSpace M] [NormalSpace M] :
      NormalSpace Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instCompletelyNormalSpace {M : Type u_1} [TopologicalSpace M] [CompletelyNormalSpace M] :
      CompletelyNormalSpace Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instCompletelyNormalSpace {M : Type u_1} [TopologicalSpace M] [CompletelyNormalSpace M] :
      CompletelyNormalSpace Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :
      DiscreteTopology Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :
      DiscreteTopology Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instSeparableSpace {M : Type u_1} [TopologicalSpace M] [TopologicalSpace.SeparableSpace M] :
      TopologicalSpace.SeparableSpace Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instSeparableSpace {M : Type u_1} [TopologicalSpace M] [TopologicalSpace.SeparableSpace M] :
      TopologicalSpace.SeparableSpace Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instFirstCountableTopology {M : Type u_1} [TopologicalSpace M] [FirstCountableTopology M] :
      FirstCountableTopology Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instFirstCountableTopology {M : Type u_1} [TopologicalSpace M] [FirstCountableTopology M] :
      FirstCountableTopology Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomAddAct.instSecondCountableTopology {M : Type u_1} [TopologicalSpace M] [SecondCountableTopology M] :
      SecondCountableTopology Mᵈᵃᵃ
      Equations
      • ⋯ = ⋯
      source
      instance DomMulAct.instSecondCountableTopology {M : Type u_1} [TopologicalSpace M] [SecondCountableTopology M] :
      SecondCountableTopology Mᵈᵐᵃ
      Equations
      • ⋯ = ⋯
      source
      @[simp]
      theorem DomAddAct.map_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.map (⇑DomAddAct.mk) (nhds x) = nhds (DomAddAct.mk x)
      source
      @[simp]
      theorem DomMulAct.map_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.map (⇑DomMulAct.mk) (nhds x) = nhds (DomMulAct.mk x)
      source
      @[simp]
      theorem DomAddAct.map_mk_symm_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵃᵃ) :
      Filter.map (⇑DomAddAct.mk.symm) (nhds x) = nhds (DomAddAct.mk.symm x)
      source
      @[simp]
      theorem DomMulAct.map_mk_symm_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵐᵃ) :
      Filter.map (⇑DomMulAct.mk.symm) (nhds x) = nhds (DomMulAct.mk.symm x)
      source
      @[simp]
      theorem DomAddAct.comap_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵃᵃ) :
      Filter.comap (⇑DomAddAct.mk) (nhds x) = nhds (DomAddAct.mk.symm x)
      source
      @[simp]
      theorem DomMulAct.comap_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵐᵃ) :
      Filter.comap (⇑DomMulAct.mk) (nhds x) = nhds (DomMulAct.mk.symm x)
      source
      @[simp]
      theorem DomAddAct.comap_mk.symm_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.comap (⇑DomAddAct.mk.symm) (nhds x) = nhds (DomAddAct.mk x)
      source
      @[simp]
      theorem DomMulAct.comap_mk.symm_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
      Filter.comap (⇑DomMulAct.mk.symm) (nhds x) = nhds (DomMulAct.mk x)