Documentation

Mathlib.Topology.Algebra.Constructions.DomMulAct

Topological space structure on Mᵈᵐᵃ and Mᵈᵃᵃ #

In this file we define TopologicalSpace structure on Mᵈᵐᵃ and Mᵈᵃᵃ and prove basic theorems about these topologies. The topologies on Mᵈᵐᵃ and Mᵈᵃᵃ are the same as the topology on M. Formally, they are induced by DomMulAct.mk.symm and DomAddAct.mk.symm, since the types aren't definitionally equal.

Tags #

topological space, group action, domain action

source
instance DomMulAct.instTopologicalSpace {M : Type u_1} [TopologicalSpace M] :
TopologicalSpace Mᵈᵐᵃ

Put the same topological space structure on Mᵈᵐᵃ as on the original space.

Equations
    source
    instance DomAddAct.instTopologicalSpace {M : Type u_1} [TopologicalSpace M] :
    TopologicalSpace Mᵈᵃᵃ

    Put the same topological space structure on Mᵈᵃᵃ as on the original space.

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

      DomMulAct.mk as a homeomorphism.

      Equations
        Instances For
          source
          def DomAddAct.mkHomeomorph {M : Type u_1} [TopologicalSpace M] :
          M ≃ₜ Mᵈᵃᵃ

          DomAddAct.mk as a homeomorphism.

          Equations
            Instances For
              source
              @[simp]
              theorem DomMulAct.mkHomeomorph_toEquiv {M : Type u_1} [TopologicalSpace M] :
              mkHomeomorph.toEquiv = mk
              source
              @[simp]
              theorem DomAddAct.mkHomeomorph_toEquiv {M : Type u_1} [TopologicalSpace M] :
              mkHomeomorph.toEquiv = mk
              source
              @[simp]
              theorem DomMulAct.coe_mkHomeomorph {M : Type u_1} [TopologicalSpace M] :
              ⇑mkHomeomorph = ⇑mk
              source
              @[simp]
              theorem DomAddAct.coe_mkHomeomorph {M : Type u_1} [TopologicalSpace M] :
              ⇑mkHomeomorph = ⇑mk
              source
              @[simp]
              theorem DomMulAct.coe_mkHomeomorph_symm {M : Type u_1} [TopologicalSpace M] :
              ⇑mkHomeomorph.symm = ⇑mk.symm
              source
              @[simp]
              theorem DomAddAct.coe_mkHomeomorph_symm {M : Type u_1} [TopologicalSpace M] :
              ⇑mkHomeomorph.symm = ⇑mk.symm
              source
              theorem DomMulAct.isInducing_mk {M : Type u_1} [TopologicalSpace M] :
              Topology.IsInducing ⇑mk
              source
              theorem DomAddAct.isInducing_mk {M : Type u_1} [TopologicalSpace M] :
              Topology.IsInducing ⇑mk
              source
              theorem DomMulAct.isEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
              Topology.IsEmbedding ⇑mk
              source
              theorem DomAddAct.isEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
              Topology.IsEmbedding ⇑mk
              source
              theorem DomMulAct.isOpenEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
              Topology.IsOpenEmbedding ⇑mk
              source
              theorem DomAddAct.isOpenEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
              Topology.IsOpenEmbedding ⇑mk
              source
              theorem DomMulAct.isClosedEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
              Topology.IsClosedEmbedding ⇑mk
              source
              theorem DomAddAct.isClosedEmbedding_mk {M : Type u_1} [TopologicalSpace M] :
              Topology.IsClosedEmbedding ⇑mk
              source
              theorem DomMulAct.isQuotientMap_mk {M : Type u_1} [TopologicalSpace M] :
              Topology.IsQuotientMap ⇑mk
              source
              theorem DomAddAct.isQuotientMap_mk {M : Type u_1} [TopologicalSpace M] :
              Topology.IsQuotientMap ⇑mk
              source
              theorem DomMulAct.isInducing_mk_symm {M : Type u_1} [TopologicalSpace M] :
              Topology.IsInducing ⇑mk.symm
              source
              theorem DomAddAct.isInducing_mk_symm {M : Type u_1} [TopologicalSpace M] :
              Topology.IsInducing ⇑mk.symm
              source
              theorem DomMulAct.isEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
              Topology.IsEmbedding ⇑mk.symm
              source
              theorem DomAddAct.isEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
              Topology.IsEmbedding ⇑mk.symm
              source
              theorem DomMulAct.isOpenEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
              Topology.IsOpenEmbedding ⇑mk.symm
              source
              theorem DomAddAct.isOpenEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
              Topology.IsOpenEmbedding ⇑mk.symm
              source
              theorem DomMulAct.isClosedEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
              Topology.IsClosedEmbedding ⇑mk.symm
              source
              theorem DomAddAct.isClosedEmbedding_mk_symm {M : Type u_1} [TopologicalSpace M] :
              Topology.IsClosedEmbedding ⇑mk.symm
              source
              theorem DomMulAct.isQuotientMap_mk_symm {M : Type u_1} [TopologicalSpace M] :
              Topology.IsQuotientMap ⇑mk.symm
              source
              theorem DomAddAct.isQuotientMap_mk_symm {M : Type u_1} [TopologicalSpace M] :
              Topology.IsQuotientMap ⇑mk.symm
              source
              instance DomMulAct.instT0Space {M : Type u_1} [TopologicalSpace M] [T0Space M] :
              T0Space Mᵈᵐᵃ
              source
              instance DomAddAct.instT0Space {M : Type u_1} [TopologicalSpace M] [T0Space M] :
              T0Space Mᵈᵃᵃ
              source
              instance DomMulAct.instT1Space {M : Type u_1} [TopologicalSpace M] [T1Space M] :
              T1Space Mᵈᵐᵃ
              source
              instance DomAddAct.instT1Space {M : Type u_1} [TopologicalSpace M] [T1Space M] :
              T1Space Mᵈᵃᵃ
              source
              instance DomMulAct.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :
              T2Space Mᵈᵐᵃ
              source
              instance DomAddAct.instT2Space {M : Type u_1} [TopologicalSpace M] [T2Space M] :
              T2Space Mᵈᵃᵃ
              source
              instance DomMulAct.instT25Space {M : Type u_1} [TopologicalSpace M] [T25Space M] :
              T25Space Mᵈᵐᵃ
              source
              instance DomAddAct.instT25Space {M : Type u_1} [TopologicalSpace M] [T25Space M] :
              T25Space Mᵈᵃᵃ
              source
              instance DomMulAct.instT3Space {M : Type u_1} [TopologicalSpace M] [T3Space M] :
              T3Space Mᵈᵐᵃ
              source
              instance DomAddAct.instT3Space {M : Type u_1} [TopologicalSpace M] [T3Space M] :
              T3Space Mᵈᵃᵃ
              source
              instance DomMulAct.instT4Space {M : Type u_1} [TopologicalSpace M] [T4Space M] :
              T4Space Mᵈᵐᵃ
              source
              instance DomAddAct.instT4Space {M : Type u_1} [TopologicalSpace M] [T4Space M] :
              T4Space Mᵈᵃᵃ
              source
              instance DomMulAct.instT5Space {M : Type u_1} [TopologicalSpace M] [T5Space M] :
              T5Space Mᵈᵐᵃ
              source
              instance DomAddAct.instT5Space {M : Type u_1} [TopologicalSpace M] [T5Space M] :
              T5Space Mᵈᵃᵃ
              source
              instance DomMulAct.instR0Space {M : Type u_1} [TopologicalSpace M] [R0Space M] :
              R0Space Mᵈᵐᵃ
              source
              instance DomAddAct.instR0Space {M : Type u_1} [TopologicalSpace M] [R0Space M] :
              R0Space Mᵈᵃᵃ
              source
              instance DomMulAct.instR1Space {M : Type u_1} [TopologicalSpace M] [R1Space M] :
              R1Space Mᵈᵐᵃ
              source
              instance DomAddAct.instR1Space {M : Type u_1} [TopologicalSpace M] [R1Space M] :
              R1Space Mᵈᵃᵃ
              source
              instance DomMulAct.instRegularSpace {M : Type u_1} [TopologicalSpace M] [RegularSpace M] :
              RegularSpace Mᵈᵐᵃ
              source
              instance DomAddAct.instRegularSpace {M : Type u_1} [TopologicalSpace M] [RegularSpace M] :
              RegularSpace Mᵈᵃᵃ
              source
              instance DomMulAct.instNormalSpace {M : Type u_1} [TopologicalSpace M] [NormalSpace M] :
              NormalSpace Mᵈᵐᵃ
              source
              instance DomAddAct.instNormalSpace {M : Type u_1} [TopologicalSpace M] [NormalSpace M] :
              NormalSpace Mᵈᵃᵃ
              source
              instance DomMulAct.instCompletelyNormalSpace {M : Type u_1} [TopologicalSpace M] [CompletelyNormalSpace M] :
              CompletelyNormalSpace Mᵈᵐᵃ
              source
              instance DomAddAct.instCompletelyNormalSpace {M : Type u_1} [TopologicalSpace M] [CompletelyNormalSpace M] :
              CompletelyNormalSpace Mᵈᵃᵃ
              source
              instance DomMulAct.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :
              DiscreteTopology Mᵈᵐᵃ
              source
              instance DomAddAct.instDiscreteTopology {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] :
              DiscreteTopology Mᵈᵃᵃ
              source
              instance DomMulAct.instSeparableSpace {M : Type u_1} [TopologicalSpace M] [TopologicalSpace.SeparableSpace M] :
              TopologicalSpace.SeparableSpace Mᵈᵐᵃ
              source
              instance DomAddAct.instSeparableSpace {M : Type u_1} [TopologicalSpace M] [TopologicalSpace.SeparableSpace M] :
              TopologicalSpace.SeparableSpace Mᵈᵃᵃ
              source
              instance DomMulAct.instFirstCountableTopology {M : Type u_1} [TopologicalSpace M] [FirstCountableTopology M] :
              FirstCountableTopology Mᵈᵐᵃ
              source
              instance DomAddAct.instFirstCountableTopology {M : Type u_1} [TopologicalSpace M] [FirstCountableTopology M] :
              FirstCountableTopology Mᵈᵃᵃ
              source
              instance DomMulAct.instSecondCountableTopology {M : Type u_1} [TopologicalSpace M] [SecondCountableTopology M] :
              SecondCountableTopology Mᵈᵐᵃ
              source
              instance DomAddAct.instSecondCountableTopology {M : Type u_1} [TopologicalSpace M] [SecondCountableTopology M] :
              SecondCountableTopology Mᵈᵃᵃ
              source
              instance DomMulAct.instCompactSpace {M : Type u_1} [TopologicalSpace M] [CompactSpace M] :
              CompactSpace Mᵈᵐᵃ
              source
              instance DomAddAct.instCompactSpace {M : Type u_1} [TopologicalSpace M] [CompactSpace M] :
              CompactSpace Mᵈᵃᵃ
              source
              instance DomMulAct.instLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [LocallyCompactSpace M] :
              LocallyCompactSpace Mᵈᵐᵃ
              source
              instance DomAddAct.instLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [LocallyCompactSpace M] :
              LocallyCompactSpace Mᵈᵃᵃ
              source
              instance DomMulAct.instWeaklyLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [WeaklyLocallyCompactSpace M] :
              WeaklyLocallyCompactSpace Mᵈᵐᵃ
              source
              instance DomAddAct.instWeaklyLocallyCompactSpace {M : Type u_1} [TopologicalSpace M] [WeaklyLocallyCompactSpace M] :
              WeaklyLocallyCompactSpace Mᵈᵃᵃ
              source
              @[simp]
              theorem DomMulAct.map_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
              Filter.map (⇑mk) (nhds x) = nhds (mk x)
              source
              @[simp]
              theorem DomAddAct.map_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
              Filter.map (⇑mk) (nhds x) = nhds (mk x)
              source
              @[simp]
              theorem DomMulAct.map_mk_symm_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵐᵃ) :
              Filter.map (⇑mk.symm) (nhds x) = nhds (mk.symm x)
              source
              @[simp]
              theorem DomAddAct.map_mk_symm_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵃᵃ) :
              Filter.map (⇑mk.symm) (nhds x) = nhds (mk.symm x)
              source
              @[simp]
              theorem DomMulAct.comap_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵐᵃ) :
              Filter.comap (⇑mk) (nhds x) = nhds (mk.symm x)
              source
              @[simp]
              theorem DomAddAct.comap_mk_nhds {M : Type u_1} [TopologicalSpace M] (x : Mᵈᵃᵃ) :
              Filter.comap (⇑mk) (nhds x) = nhds (mk.symm x)
              source
              @[simp]
              theorem DomMulAct.comap_mk.symm_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
              Filter.comap (⇑mk.symm) (nhds x) = nhds (mk x)
              source
              @[simp]
              theorem DomAddAct.comap_mk.symm_nhds {M : Type u_1} [TopologicalSpace M] (x : M) :
              Filter.comap (⇑mk.symm) (nhds x) = nhds (mk x)