Documentation

Mathlib.Topology.Algebra.Group.Basic

Topological groups #

This file defines the following typeclasses:

There is an instance deducing ContinuousSub from TopologicalGroup but we use a separate typeclass because, e.g., and ℝ≥0 have continuous subtraction but are not additive groups.

We also define Homeomorph versions of several Equivs: Homeomorph.mulLeft, Homeomorph.mulRight, Homeomorph.inv, and prove a few facts about neighbourhood filters in groups.

Tags #

topological space, group, topological group

Groups with continuous multiplication #

In this section we prove a few statements about groups with continuous (*).

theorem Homeomorph.addLeft.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
Continuous fun (x : G) => (toAddUnits a) + x
theorem Homeomorph.addLeft.proof_2 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
Continuous fun (x : G) => (-toAddUnits a) + x

Addition from the left in a topological additive group as a homeomorphism.

Equations
Instances For
    def Homeomorph.mulLeft {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
    G ≃ₜ G

    Multiplication from the left in a topological group as a homeomorphism.

    Equations
    Instances For
      @[simp]
      theorem Homeomorph.coe_addLeft {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
      (Homeomorph.addLeft a) = fun (x : G) => a + x
      @[simp]
      theorem Homeomorph.coe_mulLeft {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
      (Homeomorph.mulLeft a) = fun (x : G) => a * x
      theorem isOpenMap_add_left {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
      IsOpenMap fun (x : G) => a + x
      theorem isOpenMap_mul_left {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
      IsOpenMap fun (x : G) => a * x
      theorem IsOpen.left_addCoset {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {U : Set G} (h : IsOpen U) (x : G) :
      IsOpen (x +ᵥ U)
      theorem IsOpen.leftCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsOpen U) (x : G) :
      IsOpen (x U)
      theorem isClosedMap_add_left {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
      IsClosedMap fun (x : G) => a + x
      theorem isClosedMap_mul_left {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
      IsClosedMap fun (x : G) => a * x
      theorem IsClosed.left_addCoset {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {U : Set G} (h : IsClosed U) (x : G) :
      theorem IsClosed.leftCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsClosed U) (x : G) :
      theorem Homeomorph.addRight.proof_2 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
      Continuous fun (x : G) => id x + (-toAddUnits a)

      Addition from the right in a topological additive group as a homeomorphism.

      Equations
      Instances For
        theorem Homeomorph.addRight.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
        Continuous fun (x : G) => id x + (toAddUnits a)
        def Homeomorph.mulRight {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
        G ≃ₜ G

        Multiplication from the right in a topological group as a homeomorphism.

        Equations
        Instances For
          @[simp]
          theorem Homeomorph.coe_addRight {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
          (Homeomorph.addRight a) = fun (x : G) => x + a
          @[simp]
          theorem Homeomorph.coe_mulRight {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
          (Homeomorph.mulRight a) = fun (x : G) => x * a
          theorem isOpenMap_add_right {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
          IsOpenMap fun (x : G) => x + a
          theorem isOpenMap_mul_right {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
          IsOpenMap fun (x : G) => x * a
          theorem IsOpen.right_addCoset {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {U : Set G} (h : IsOpen U) (x : G) :
          theorem IsOpen.rightCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsOpen U) (x : G) :
          theorem isClosedMap_add_right {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
          IsClosedMap fun (x : G) => x + a
          theorem isClosedMap_mul_right {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
          IsClosedMap fun (x : G) => x * a
          theorem IsClosed.rightCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsClosed U) (x : G) :

          ContinuousInv and ContinuousNeg #

          class ContinuousNeg (G : Type u) [TopologicalSpace G] [Neg G] :

          Basic hypothesis to talk about a topological additive group. A topological additive group over M, for example, is obtained by requiring the instances AddGroup M and ContinuousAdd M and ContinuousNeg M.

          Instances
            class ContinuousInv (G : Type u) [TopologicalSpace G] [Inv G] :

            Basic hypothesis to talk about a topological group. A topological group over M, for example, is obtained by requiring the instances Group M and ContinuousMul M and ContinuousInv M.

            Instances
              theorem continuousOn_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {s : Set G} :
              ContinuousOn Neg.neg s
              theorem continuousOn_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {s : Set G} :
              ContinuousOn Inv.inv s
              theorem continuousWithinAt_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {s : Set G} {x : G} :
              ContinuousWithinAt Neg.neg s x
              theorem continuousWithinAt_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {s : Set G} {x : G} :
              ContinuousWithinAt Inv.inv s x
              theorem continuousAt_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x : G} :
              ContinuousAt Neg.neg x
              theorem continuousAt_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x : G} :
              ContinuousAt Inv.inv x
              theorem tendsto_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] (a : G) :
              Filter.Tendsto Neg.neg (nhds a) (nhds (-a))
              theorem tendsto_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] (a : G) :
              Filter.Tendsto Inv.inv (nhds a) (nhds a⁻¹)
              theorem Filter.Tendsto.neg {G : Type w} {α : Type u} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {f : αG} {l : Filter α} {y : G} (h : Filter.Tendsto f l (nhds y)) :
              Filter.Tendsto (fun (x : α) => -f x) l (nhds (-y))

              If a function converges to a value in an additive topological group, then its negation converges to the negation of this value.

              theorem Filter.Tendsto.inv {G : Type w} {α : Type u} [TopologicalSpace G] [Inv G] [ContinuousInv G] {f : αG} {l : Filter α} {y : G} (h : Filter.Tendsto f l (nhds y)) :
              Filter.Tendsto (fun (x : α) => (f x)⁻¹) l (nhds y⁻¹)

              If a function converges to a value in a multiplicative topological group, then its inverse converges to the inverse of this value. For the version in normed fields assuming additionally that the limit is nonzero, use Tendsto.inv'.

              theorem Continuous.neg {G : Type w} {α : Type u} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} (hf : Continuous f) :
              Continuous fun (x : α) => -f x
              theorem Continuous.inv {G : Type w} {α : Type u} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} (hf : Continuous f) :
              Continuous fun (x : α) => (f x)⁻¹
              theorem ContinuousAt.neg {G : Type w} {α : Type u} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} {x : α} (hf : ContinuousAt f x) :
              ContinuousAt (fun (x : α) => -f x) x
              theorem ContinuousAt.inv {G : Type w} {α : Type u} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} {x : α} (hf : ContinuousAt f x) :
              ContinuousAt (fun (x : α) => (f x)⁻¹) x
              theorem ContinuousOn.neg {G : Type w} {α : Type u} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} {s : Set α} (hf : ContinuousOn f s) :
              ContinuousOn (fun (x : α) => -f x) s
              theorem ContinuousOn.inv {G : Type w} {α : Type u} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} {s : Set α} (hf : ContinuousOn f s) :
              ContinuousOn (fun (x : α) => (f x)⁻¹) s
              theorem ContinuousWithinAt.neg {G : Type w} {α : Type u} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) :
              ContinuousWithinAt (fun (x : α) => -f x) s x
              theorem ContinuousWithinAt.inv {G : Type w} {α : Type u} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) :
              ContinuousWithinAt (fun (x : α) => (f x)⁻¹) s x
              Equations
              • =
              Equations
              • =
              instance Pi.continuousNeg {ι : Type u_1} {C : ιType u_2} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Neg (C i)] [∀ (i : ι), ContinuousNeg (C i)] :
              ContinuousNeg ((i : ι) → C i)
              Equations
              • =
              instance Pi.continuousInv {ι : Type u_1} {C : ιType u_2} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Inv (C i)] [∀ (i : ι), ContinuousInv (C i)] :
              ContinuousInv ((i : ι) → C i)
              Equations
              • =
              instance Pi.has_continuous_neg' {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {ι : Type u_1} :
              ContinuousNeg (ιG)

              A version of Pi.continuousNeg for non-dependent functions. It is needed because sometimes Lean fails to use Pi.continuousNeg for non-dependent functions.

              Equations
              • =
              instance Pi.has_continuous_inv' {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {ι : Type u_1} :
              ContinuousInv (ιG)

              A version of Pi.continuousInv for non-dependent functions. It is needed because sometimes Lean fails to use Pi.continuousInv for non-dependent functions.

              Equations
              • =
              theorem isClosed_setOf_map_neg (G₁ : Type u_2) (G₂ : Type u_3) [TopologicalSpace G₂] [T2Space G₂] [Neg G₁] [Neg G₂] [ContinuousNeg G₂] :
              IsClosed {f : G₁G₂ | ∀ (x : G₁), f (-x) = -f x}
              theorem isClosed_setOf_map_inv (G₁ : Type u_2) (G₂ : Type u_3) [TopologicalSpace G₂] [T2Space G₂] [Inv G₁] [Inv G₂] [ContinuousInv G₂] :
              IsClosed {f : G₁G₂ | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}

              Negation in a topological group as a homeomorphism.

              Equations
              Instances For

                Inversion in a topological group as a homeomorphism.

                Equations
                Instances For
                  @[simp]
                  @[simp]
                  theorem IsOpen.neg {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsOpen s) :
                  theorem IsOpen.inv {G : Type w} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsOpen s) :
                  theorem IsClosed.neg {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsClosed s) :
                  theorem continuousNeg_sInf {G : Type w} [Neg G] {ts : Set (TopologicalSpace G)} (h : tts, ContinuousNeg G) :
                  theorem continuousInv_sInf {G : Type w} [Inv G] {ts : Set (TopologicalSpace G)} (h : tts, ContinuousInv G) :
                  theorem continuousNeg_iInf {G : Type w} {ι' : Sort u_1} [Neg G] {ts' : ι'TopologicalSpace G} (h' : ∀ (i : ι'), ContinuousNeg G) :
                  theorem continuousInv_iInf {G : Type w} {ι' : Sort u_1} [Inv G] {ts' : ι'TopologicalSpace G} (h' : ∀ (i : ι'), ContinuousInv G) :
                  theorem continuousNeg_inf {G : Type w} [Neg G] {t₁ : TopologicalSpace G} {t₂ : TopologicalSpace G} (h₁ : ContinuousNeg G) (h₂ : ContinuousNeg G) :
                  theorem continuousInv_inf {G : Type w} [Inv G] {t₁ : TopologicalSpace G} {t₂ : TopologicalSpace G} (h₁ : ContinuousInv G) (h₂ : ContinuousInv G) :
                  theorem Inducing.continuousNeg {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousNeg H] {f : GH} (hf : Inducing f) (hf_inv : ∀ (x : G), f (-x) = -f x) :
                  theorem Inducing.continuousInv {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousInv H] {f : GH} (hf : Inducing f) (hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹) :

                  Topological groups #

                  A topological group is a group in which the multiplication and inversion operations are continuous. Topological additive groups are defined in the same way. Equivalently, we can require that the division operation x y ↦ x * y⁻¹ (resp., subtraction) is continuous.

                  A topological (additive) group is a group in which the addition and negation operations are continuous.

                    Instances

                      A topological group is a group in which the multiplication and inversion operations are continuous.

                      When you declare an instance that does not already have a UniformSpace instance, you should also provide an instance of UniformSpace and UniformGroup using TopologicalGroup.toUniformSpace and topologicalCommGroup_isUniform.

                        Instances
                          theorem TopologicalAddGroup.continuous_conj_sum {G : Type w} [TopologicalSpace G] [Neg G] [Add G] [ContinuousAdd G] [ContinuousNeg G] :
                          Continuous fun (g : G × G) => g.1 + g.2 + -g.1

                          Conjugation is jointly continuous on G × G when both add and neg are continuous.

                          theorem TopologicalGroup.continuous_conj_prod {G : Type w} [TopologicalSpace G] [Inv G] [Mul G] [ContinuousMul G] [ContinuousInv G] :
                          Continuous fun (g : G × G) => g.1 * g.2 * g.1⁻¹

                          Conjugation is jointly continuous on G × G when both mul and inv are continuous.

                          theorem TopologicalAddGroup.continuous_conj {G : Type w} [TopologicalSpace G] [Neg G] [Add G] [ContinuousAdd G] (g : G) :
                          Continuous fun (h : G) => g + h + -g

                          Conjugation by a fixed element is continuous when add is continuous.

                          theorem TopologicalGroup.continuous_conj {G : Type w} [TopologicalSpace G] [Inv G] [Mul G] [ContinuousMul G] (g : G) :
                          Continuous fun (h : G) => g * h * g⁻¹

                          Conjugation by a fixed element is continuous when mul is continuous.

                          theorem TopologicalAddGroup.continuous_conj' {G : Type w} [TopologicalSpace G] [Neg G] [Add G] [ContinuousAdd G] [ContinuousNeg G] (h : G) :
                          Continuous fun (g : G) => g + h + -g

                          Conjugation acting on fixed element of the additive group is continuous when both add and neg are continuous.

                          theorem TopologicalGroup.continuous_conj' {G : Type w} [TopologicalSpace G] [Inv G] [Mul G] [ContinuousMul G] [ContinuousInv G] (h : G) :
                          Continuous fun (g : G) => g * h * g⁻¹

                          Conjugation acting on fixed element of the group is continuous when both mul and inv are continuous.

                          theorem continuous_zsmul {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (z : ) :
                          Continuous fun (a : G) => z a
                          abbrev continuous_zsmul.match_1 (motive : Prop) :
                          ∀ (x : ), (∀ (n : ), motive (Int.ofNat n))(∀ (n : ), motive (Int.negSucc n))motive x
                          Equations
                          • =
                          Instances For
                            theorem continuous_zpow {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (z : ) :
                            Continuous fun (a : G) => a ^ z
                            theorem Continuous.zsmul {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace α] {f : αG} (h : Continuous f) (z : ) :
                            Continuous fun (b : α) => z f b
                            theorem Continuous.zpow {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace α] {f : αG} (h : Continuous f) (z : ) :
                            Continuous fun (b : α) => f b ^ z
                            theorem continuousOn_zsmul {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} (z : ) :
                            ContinuousOn (fun (x : G) => z x) s
                            theorem continuousOn_zpow {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} (z : ) :
                            ContinuousOn (fun (x : G) => x ^ z) s
                            theorem continuousAt_zsmul {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) (z : ) :
                            ContinuousAt (fun (x : G) => z x) x
                            theorem continuousAt_zpow {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) (z : ) :
                            ContinuousAt (fun (x : G) => x ^ z) x
                            theorem Filter.Tendsto.zsmul {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {α : Type u_1} {l : Filter α} {f : αG} {x : G} (hf : Filter.Tendsto f l (nhds x)) (z : ) :
                            Filter.Tendsto (fun (x : α) => z f x) l (nhds (z x))
                            theorem Filter.Tendsto.zpow {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {α : Type u_1} {l : Filter α} {f : αG} {x : G} (hf : Filter.Tendsto f l (nhds x)) (z : ) :
                            Filter.Tendsto (fun (x : α) => f x ^ z) l (nhds (x ^ z))
                            theorem ContinuousWithinAt.zsmul {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace α] {f : αG} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ) :
                            ContinuousWithinAt (fun (x : α) => z f x) s x
                            theorem ContinuousWithinAt.zpow {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace α] {f : αG} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ) :
                            ContinuousWithinAt (fun (x : α) => f x ^ z) s x
                            theorem ContinuousAt.zsmul {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace α] {f : αG} {x : α} (hf : ContinuousAt f x) (z : ) :
                            ContinuousAt (fun (x : α) => z f x) x
                            theorem ContinuousAt.zpow {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace α] {f : αG} {x : α} (hf : ContinuousAt f x) (z : ) :
                            ContinuousAt (fun (x : α) => f x ^ z) x
                            theorem ContinuousOn.zsmul {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace α] {f : αG} {s : Set α} (hf : ContinuousOn f s) (z : ) :
                            ContinuousOn (fun (x : α) => z f x) s
                            theorem ContinuousOn.zpow {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace α] {f : αG} {s : Set α} (hf : ContinuousOn f s) (z : ) :
                            ContinuousOn (fun (x : α) => f x ^ z) s
                            instance Pi.topologicalAddGroup {β : Type v} {C : βType u_1} [(b : β) → TopologicalSpace (C b)] [(b : β) → AddGroup (C b)] [∀ (b : β), TopologicalAddGroup (C b)] :
                            TopologicalAddGroup ((b : β) → C b)
                            Equations
                            • =
                            instance Pi.topologicalGroup {β : Type v} {C : βType u_1} [(b : β) → TopologicalSpace (C b)] [(b : β) → Group (C b)] [∀ (b : β), TopologicalGroup (C b)] :
                            TopologicalGroup ((b : β) → C b)
                            Equations
                            • =

                            If addition is continuous in α, then it also is in αᵃᵒᵖ.

                            Equations
                            • =

                            If multiplication is continuous in α, then it also is in αᵐᵒᵖ.

                            Equations
                            • =
                            theorem neg_mem_nhds_zero (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {S : Set G} (hS : S nhds 0) :
                            theorem inv_mem_nhds_one (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] {S : Set G} (hS : S nhds 1) :

                            The map (x, y) ↦ (x, x + y) as a homeomorphism. This is a shear mapping.

                            Equations
                            Instances For
                              theorem Homeomorph.shearAddRight.proof_2 (G : Type u_1) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] :
                              Continuous fun (x : G × G) => (x.1, (Equiv.addLeft ((Equiv.refl G).symm x.1)).symm x.2)

                              The map (x, y) ↦ (x, x * y) as a homeomorphism. This is a shear mapping.

                              Equations
                              Instances For
                                @[simp]
                                theorem Homeomorph.shearAddRight_coe (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] :
                                (Homeomorph.shearAddRight G) = fun (z : G × G) => (z.1, z.1 + z.2)
                                @[simp]
                                theorem Homeomorph.shearMulRight_coe (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] :
                                (Homeomorph.shearMulRight G) = fun (z : G × G) => (z.1, z.1 * z.2)
                                @[simp]
                                @[simp]
                                theorem Inducing.topologicalGroup {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] {F : Type u_1} [Group H] [TopologicalSpace H] [FunLike F H G] [MonoidHomClass F H G] (f : F) (hf : Inducing f) :
                                theorem topologicalGroup_induced {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] {F : Type u_1} [Group H] [FunLike F H G] [MonoidHomClass F H G] (f : F) :
                                theorem AddSubgroup.topologicalClosure.proof_3 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) {g : G} (hg : g { toAddSubsemigroup := { carrier := closure s, add_mem' := }, zero_mem' := }.carrier) :
                                -g { toAddSubsemigroup := { carrier := closure s, add_mem' := }, zero_mem' := }.carrier

                                The (topological-space) closure of an additive subgroup of an additive topological group is itself an additive subgroup.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem AddSubgroup.topologicalClosure.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) :
                                  ∀ {a b : G}, a (AddSubmonoid.topologicalClosure s.toAddSubmonoid).carrierb (AddSubmonoid.topologicalClosure s.toAddSubmonoid).carriera + b (AddSubmonoid.topologicalClosure s.toAddSubmonoid).carrier

                                  The (topological-space) closure of a subgroup of a topological group is itself a subgroup.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    The topological closure of a normal additive subgroup is normal.

                                    The topological closure of a normal subgroup is normal.

                                    The connected component of 0 is a subgroup of G.

                                    Equations
                                    Instances For

                                      The connected component of 1 is a subgroup of G.

                                      Equations
                                      Instances For

                                        If a subgroup of an additive topological group is commutative, then so is its topological closure.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          theorem AddSubgroup.addCommGroupTopologicalClosure.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [T2Space G] (s : AddSubgroup G) (hs : ∀ (x y : s), x + y = y + x) (a : (AddSubmonoid.topologicalClosure s.toAddSubmonoid)) (b : (AddSubmonoid.topologicalClosure s.toAddSubmonoid)) :
                                          a + b = b + a
                                          def Subgroup.commGroupTopologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] [T2Space G] (s : Subgroup G) (hs : ∀ (x y : s), x * y = y * x) :

                                          If a subgroup of a topological group is commutative, then so is its topological closure.

                                          Equations
                                          Instances For
                                            theorem exists_nhds_half_neg {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} (hs : s nhds 0) :
                                            ∃ V ∈ nhds 0, vV, wV, v - w s
                                            theorem exists_nhds_split_inv {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} (hs : s nhds 1) :
                                            ∃ V ∈ nhds 1, vV, wV, v / w s
                                            theorem nhds_translation_add_neg {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) :
                                            Filter.comap (fun (x_1 : G) => x_1 + -x) (nhds 0) = nhds x
                                            theorem nhds_translation_mul_inv {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) :
                                            Filter.comap (fun (x_1 : G) => x_1 * x⁻¹) (nhds 1) = nhds x
                                            @[simp]
                                            theorem map_add_left_nhds {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) (y : G) :
                                            Filter.map (fun (x_1 : G) => x + x_1) (nhds y) = nhds (x + y)
                                            @[simp]
                                            theorem map_mul_left_nhds {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) (y : G) :
                                            Filter.map (fun (x_1 : G) => x * x_1) (nhds y) = nhds (x * y)
                                            theorem map_add_left_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) :
                                            Filter.map (fun (x_1 : G) => x + x_1) (nhds 0) = nhds x
                                            theorem map_mul_left_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) :
                                            Filter.map (fun (x_1 : G) => x * x_1) (nhds 1) = nhds x
                                            @[simp]
                                            theorem map_add_right_nhds {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) (y : G) :
                                            Filter.map (fun (x_1 : G) => x_1 + x) (nhds y) = nhds (y + x)
                                            @[simp]
                                            theorem map_mul_right_nhds {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) (y : G) :
                                            Filter.map (fun (x_1 : G) => x_1 * x) (nhds y) = nhds (y * x)
                                            theorem map_add_right_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) :
                                            Filter.map (fun (x_1 : G) => x_1 + x) (nhds 0) = nhds x
                                            theorem map_mul_right_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) :
                                            Filter.map (fun (x_1 : G) => x_1 * x) (nhds 1) = nhds x
                                            theorem Filter.HasBasis.nhds_of_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {ι : Sort u_1} {p : ιProp} {s : ιSet G} (hb : Filter.HasBasis (nhds 0) p s) (x : G) :
                                            Filter.HasBasis (nhds x) p fun (i : ι) => {y : G | y - x s i}
                                            theorem Filter.HasBasis.nhds_of_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {ι : Sort u_1} {p : ιProp} {s : ιSet G} (hb : Filter.HasBasis (nhds 1) p s) (x : G) :
                                            Filter.HasBasis (nhds x) p fun (i : ι) => {y : G | y / x s i}
                                            theorem mem_closure_iff_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {x : G} {s : Set G} :
                                            x closure s Unhds 0, ∃ y ∈ s, y - x U
                                            theorem mem_closure_iff_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {x : G} {s : Set G} :
                                            x closure s Unhds 1, ∃ y ∈ s, y / x U
                                            theorem continuous_of_continuousAt_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {M : Type u_1} {hom : Type u_2} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] [FunLike hom G M] [AddMonoidHomClass hom G M] (f : hom) (hf : ContinuousAt (f) 0) :

                                            An additive monoid homomorphism (a bundled morphism of a type that implements AddMonoidHomClass) from an additive topological group to an additive topological monoid is continuous provided that it is continuous at zero. See also uniformContinuous_of_continuousAt_zero.

                                            theorem continuous_of_continuousAt_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {M : Type u_1} {hom : Type u_2} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] [FunLike hom G M] [MonoidHomClass hom G M] (f : hom) (hf : ContinuousAt (f) 1) :

                                            A monoid homomorphism (a bundled morphism of a type that implements MonoidHomClass) from a topological group to a topological monoid is continuous provided that it is continuous at one. See also uniformContinuous_of_continuousAt_one.

                                            theorem continuous_of_continuousAt_zero₂ {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {H : Type u_1} {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [AddGroup H] [TopologicalSpace H] [TopologicalAddGroup H] (f : G →+ H →+ M) (hf : ContinuousAt (fun (x : G × H) => (f x.1) x.2) (0, 0)) (hl : ∀ (x : G), ContinuousAt ((f x)) 0) (hr : ∀ (y : H), ContinuousAt (fun (x : G) => (f x) y) 0) :
                                            Continuous fun (x : G × H) => (f x.1) x.2
                                            abbrev continuous_of_continuousAt_zero₂.match_1 {G : Type u_1} {H : Type u_2} (motive : G × HProp) :
                                            ∀ (x : G × H), (∀ (x : G) (y : H), motive (x, y))motive x
                                            Equations
                                            • =
                                            Instances For
                                              theorem continuous_of_continuousAt_one₂ {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {H : Type u_1} {M : Type u_2} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [Group H] [TopologicalSpace H] [TopologicalGroup H] (f : G →* H →* M) (hf : ContinuousAt (fun (x : G × H) => (f x.1) x.2) (1, 1)) (hl : ∀ (x : G), ContinuousAt ((f x)) 1) (hr : ∀ (y : H), ContinuousAt (fun (x : G) => (f x) y) 1) :
                                              Continuous fun (x : G × H) => (f x.1) x.2
                                              theorem TopologicalAddGroup.ext {G : Type u_1} [AddGroup G] {t : TopologicalSpace G} {t' : TopologicalSpace G} (tg : TopologicalAddGroup G) (tg' : TopologicalAddGroup G) (h : nhds 0 = nhds 0) :
                                              t = t'
                                              theorem TopologicalGroup.ext {G : Type u_1} [Group G] {t : TopologicalSpace G} {t' : TopologicalSpace G} (tg : TopologicalGroup G) (tg' : TopologicalGroup G) (h : nhds 1 = nhds 1) :
                                              t = t'
                                              theorem TopologicalGroup.ext_iff {G : Type u_1} [Group G] {t : TopologicalSpace G} {t' : TopologicalSpace G} (tg : TopologicalGroup G) (tg' : TopologicalGroup G) :
                                              t = t' nhds 1 = nhds 1
                                              theorem ContinuousNeg.of_nhds_zero {G : Type u_1} [AddGroup G] [TopologicalSpace G] (hinv : Filter.Tendsto (fun (x : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => x₀ + x + -x₀) (nhds 0) (nhds 0)) :
                                              theorem ContinuousInv.of_nhds_one {G : Type u_1} [Group G] [TopologicalSpace G] (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) :
                                              theorem TopologicalAddGroup.of_nhds_zero' {G : Type u} [AddGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : G) => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun (x : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) (hright : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x + x₀) (nhds 0)) :
                                              theorem TopologicalGroup.of_nhds_one' {G : Type u} [Group G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : G) => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) (hright : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x * x₀) (nhds 1)) :
                                              theorem TopologicalAddGroup.of_nhds_zero {G : Type u} [AddGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : G) => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun (x : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => x₀ + x + -x₀) (nhds 0) (nhds 0)) :
                                              theorem TopologicalGroup.of_nhds_one {G : Type u} [Group G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : G) => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun (x : G) => x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) :
                                              theorem TopologicalAddGroup.of_comm_of_nhds_zero {G : Type u} [AddCommGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : G) => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun (x : G) => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ + x) (nhds 0)) :
                                              theorem TopologicalGroup.of_comm_of_nhds_one {G : Type u} [CommGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : G) => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun (x : G) => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun (x : G) => x₀ * x) (nhds 1)) :
                                              theorem QuotientAddGroup.nhds_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) (x : G) :
                                              nhds x = Filter.map QuotientAddGroup.mk (nhds x)

                                              Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.

                                              theorem QuotientGroup.nhds_eq {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (N : Subgroup G) (x : G) :
                                              nhds x = Filter.map QuotientGroup.mk (nhds x)

                                              Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.

                                              Any first countable topological additive group has an antitone neighborhood basis u : ℕ → set G for which u (n + 1) + u (n + 1) ⊆ u n. The existence of such a neighborhood basis is a key tool for QuotientAddGroup.completeSpace

                                              Any first countable topological group has an antitone neighborhood basis u : ℕ → Set G for which (u (n + 1)) ^ 2 ⊆ u n. The existence of such a neighborhood basis is a key tool for QuotientGroup.completeSpace

                                              In a first countable topological additive group G with normal additive subgroup N, 0 : G ⧸ N has a countable neighborhood basis.

                                              Equations
                                              • =

                                              In a first countable topological group G with normal subgroup N, 1 : G ⧸ N has a countable neighborhood basis.

                                              Equations
                                              • =
                                              class ContinuousSub (G : Type u_1) [TopologicalSpace G] [Sub G] :

                                              A typeclass saying that p : G × G ↦ p.1 - p.2 is a continuous function. This property automatically holds for topological additive groups but it also holds, e.g., for ℝ≥0.

                                              Instances
                                                class ContinuousDiv (G : Type u_1) [TopologicalSpace G] [Div G] :

                                                A typeclass saying that p : G × G ↦ p.1 / p.2 is a continuous function. This property automatically holds for topological groups. Lemmas using this class have primes. The unprimed version is for GroupWithZero.

                                                Instances
                                                  theorem Filter.Tendsto.sub {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] {f : αG} {g : αG} {l : Filter α} {a : G} {b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) :
                                                  Filter.Tendsto (fun (x : α) => f x - g x) l (nhds (a - b))
                                                  theorem Filter.Tendsto.div' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] {f : αG} {g : αG} {l : Filter α} {a : G} {b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) :
                                                  Filter.Tendsto (fun (x : α) => f x / g x) l (nhds (a / b))
                                                  theorem Filter.Tendsto.const_sub {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] (b : G) {c : G} {f : αG} {l : Filter α} (h : Filter.Tendsto f l (nhds c)) :
                                                  Filter.Tendsto (fun (k : α) => b - f k) l (nhds (b - c))
                                                  theorem Filter.Tendsto.const_div' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] (b : G) {c : G} {f : αG} {l : Filter α} (h : Filter.Tendsto f l (nhds c)) :
                                                  Filter.Tendsto (fun (k : α) => b / f k) l (nhds (b / c))
                                                  theorem Filter.tendsto_const_sub_iff {α : Type u} {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [ContinuousSub G] (b : G) {c : G} {f : αG} {l : Filter α} :
                                                  Filter.Tendsto (fun (k : α) => b - f k) l (nhds (b - c)) Filter.Tendsto f l (nhds c)
                                                  theorem Filter.tendsto_const_div_iff {α : Type u} {G : Type u_1} [CommGroup G] [TopologicalSpace G] [ContinuousDiv G] (b : G) {c : G} {f : αG} {l : Filter α} :
                                                  Filter.Tendsto (fun (k : α) => b / f k) l (nhds (b / c)) Filter.Tendsto f l (nhds c)
                                                  theorem Filter.Tendsto.sub_const {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] {c : G} {f : αG} {l : Filter α} (h : Filter.Tendsto f l (nhds c)) (b : G) :
                                                  Filter.Tendsto (fun (x : α) => f x - b) l (nhds (c - b))
                                                  theorem Filter.Tendsto.div_const' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] {c : G} {f : αG} {l : Filter α} (h : Filter.Tendsto f l (nhds c)) (b : G) :
                                                  Filter.Tendsto (fun (x : α) => f x / b) l (nhds (c / b))
                                                  theorem Filter.tendsto_div_const_iff {α : Type u} {G : Type u_1} [CommGroupWithZero G] [TopologicalSpace G] [ContinuousDiv G] {b : G} (hb : b 0) {c : G} {f : αG} {l : Filter α} :
                                                  Filter.Tendsto (fun (x : α) => f x / b) l (nhds (c / b)) Filter.Tendsto f l (nhds c)
                                                  theorem Filter.tendsto_sub_const_iff {α : Type u} {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [ContinuousSub G] (b : G) {c : G} {f : αG} {l : Filter α} :
                                                  Filter.Tendsto (fun (x : α) => f x - b) l (nhds (c - b)) Filter.Tendsto f l (nhds c)
                                                  theorem Continuous.sub {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] [TopologicalSpace α] {f : αG} {g : αG} (hf : Continuous f) (hg : Continuous g) :
                                                  Continuous fun (x : α) => f x - g x
                                                  theorem Continuous.div' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] [TopologicalSpace α] {f : αG} {g : αG} (hf : Continuous f) (hg : Continuous g) :
                                                  Continuous fun (x : α) => f x / g x
                                                  theorem continuous_sub_left {G : Type w} [TopologicalSpace G] [Sub G] [ContinuousSub G] (a : G) :
                                                  Continuous fun (x : G) => a - x
                                                  theorem continuous_div_left' {G : Type w} [TopologicalSpace G] [Div G] [ContinuousDiv G] (a : G) :
                                                  Continuous fun (x : G) => a / x
                                                  theorem continuous_sub_right {G : Type w} [TopologicalSpace G] [Sub G] [ContinuousSub G] (a : G) :
                                                  Continuous fun (x : G) => x - a
                                                  theorem continuous_div_right' {G : Type w} [TopologicalSpace G] [Div G] [ContinuousDiv G] (a : G) :
                                                  Continuous fun (x : G) => x / a
                                                  theorem ContinuousAt.sub {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] [TopologicalSpace α] {f : αG} {g : αG} {x : α} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
                                                  ContinuousAt (fun (x : α) => f x - g x) x
                                                  theorem ContinuousAt.div' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] [TopologicalSpace α] {f : αG} {g : αG} {x : α} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
                                                  ContinuousAt (fun (x : α) => f x / g x) x
                                                  theorem ContinuousWithinAt.sub {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] [TopologicalSpace α] {f : αG} {g : αG} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
                                                  ContinuousWithinAt (fun (x : α) => f x - g x) s x
                                                  theorem ContinuousWithinAt.div' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] [TopologicalSpace α] {f : αG} {g : αG} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
                                                  ContinuousWithinAt (fun (x : α) => f x / g x) s x
                                                  theorem ContinuousOn.sub {G : Type w} {α : Type u} [TopologicalSpace G] [Sub G] [ContinuousSub G] [TopologicalSpace α] {f : αG} {g : αG} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
                                                  ContinuousOn (fun (x : α) => f x - g x) s
                                                  theorem ContinuousOn.div' {G : Type w} {α : Type u} [TopologicalSpace G] [Div G] [ContinuousDiv G] [TopologicalSpace α] {f : αG} {g : αG} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
                                                  ContinuousOn (fun (x : α) => f x / g x) s
                                                  theorem Homeomorph.subLeft.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) :
                                                  Continuous fun (x_1 : G) => -x_1 + x
                                                  theorem Homeomorph.subLeft.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) :
                                                  Continuous fun (x_1 : G) => x - x_1

                                                  A version of Homeomorph.addLeft a (-b) that is defeq to a - b.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem Homeomorph.subLeft_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) :
                                                    @[simp]
                                                    theorem Homeomorph.divLeft_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) :

                                                    A version of Homeomorph.mulLeft a b⁻¹ that is defeq to a / b.

                                                    Equations
                                                    Instances For
                                                      theorem isOpenMap_sub_left {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) :
                                                      IsOpenMap fun (x : G) => a - x
                                                      theorem isOpenMap_div_left {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) :
                                                      IsOpenMap fun (x : G) => a / x
                                                      theorem isClosedMap_sub_left {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) :
                                                      IsClosedMap fun (x : G) => a - x
                                                      theorem isClosedMap_div_left {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) :
                                                      IsClosedMap fun (x : G) => a / x

                                                      A version of Homeomorph.addRight (-a) b that is defeq to b - a.

                                                      Equations
                                                      Instances For
                                                        theorem Homeomorph.subRight.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) :
                                                        Continuous fun (x_1 : G) => id x_1 - x
                                                        theorem Homeomorph.subRight.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) :
                                                        Continuous fun (x_1 : G) => id x_1 + x
                                                        @[simp]
                                                        theorem Homeomorph.subRight_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) :
                                                        @[simp]
                                                        theorem Homeomorph.divRight_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) :

                                                        A version of Homeomorph.mulRight a⁻¹ b that is defeq to b / a.

                                                        Equations
                                                        Instances For
                                                          theorem isOpenMap_sub_right {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) :
                                                          IsOpenMap fun (x : G) => x - a
                                                          theorem isOpenMap_div_right {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) :
                                                          IsOpenMap fun (x : G) => x / a
                                                          theorem isClosedMap_sub_right {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) :
                                                          IsClosedMap fun (x : G) => x - a
                                                          theorem isClosedMap_div_right {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) :
                                                          IsClosedMap fun (x : G) => x / a
                                                          theorem tendsto_sub_nhds_zero_iff {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {α : Type u_1} {l : Filter α} {x : G} {u : αG} :
                                                          Filter.Tendsto (fun (x_1 : α) => u x_1 - x) l (nhds 0) Filter.Tendsto u l (nhds x)
                                                          theorem tendsto_div_nhds_one_iff {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] {α : Type u_1} {l : Filter α} {x : G} {u : αG} :
                                                          Filter.Tendsto (fun (x_1 : α) => u x_1 / x) l (nhds 1) Filter.Tendsto u l (nhds x)
                                                          theorem nhds_translation_sub {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) :
                                                          Filter.comap (fun (x_1 : G) => x_1 - x) (nhds 0) = nhds x
                                                          theorem nhds_translation_div {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) :
                                                          Filter.comap (fun (x_1 : G) => x_1 / x) (nhds 1) = nhds x

                                                          Topological operations on pointwise sums and products #

                                                          A few results about interior and closure of the pointwise addition/multiplication of sets in groups with continuous addition/multiplication. See also Submonoid.top_closure_mul_self_eq in Topology.Algebra.Monoid.

                                                          theorem IsOpen.vadd_left {α : Type u} {β : Type v} [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousConstVAdd α β] {s : Set α} {t : Set β} (ht : IsOpen t) :
                                                          IsOpen (s +ᵥ t)
                                                          theorem IsOpen.smul_left {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α} {t : Set β} (ht : IsOpen t) :
                                                          IsOpen (s t)
                                                          theorem subset_interior_vadd_right {α : Type u} {β : Type v} [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousConstVAdd α β] {s : Set α} {t : Set β} :
                                                          theorem subset_interior_smul_right {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α} {t : Set β} :
                                                          theorem vadd_mem_nhds {α : Type u} {β : Type v} [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousConstVAdd α β] {t : Set β} (a : α) {x : β} (ht : t nhds x) :
                                                          a +ᵥ t nhds (a +ᵥ x)
                                                          theorem smul_mem_nhds {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {t : Set β} (a : α) {x : β} (ht : t nhds x) :
                                                          a t nhds (a x)
                                                          theorem subset_interior_vadd {α : Type u} {β : Type v} [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousConstVAdd α β] {s : Set α} {t : Set β} [TopologicalSpace α] :
                                                          theorem subset_interior_smul {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α} {t : Set β} [TopologicalSpace α] :
                                                          theorem IsClosed.vadd_left_of_isCompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousNeg α] [ContinuousVAdd α β] {s : Set α} {t : Set β} (ht : IsClosed t) (hs : IsCompact s) :
                                                          theorem IsClosed.smul_left_of_isCompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousInv α] [ContinuousSMul α β] {s : Set α} {t : Set β} (ht : IsClosed t) (hs : IsCompact s) :

                                                          One may expect a version of IsClosed.smul_left_of_isCompact where t is compact and s is closed, but such a lemma can't be true in this level of generality. For a counterexample, consider acting on by translation, and let s : Set ℚ := univ, t : set ℝ := {0}. Then s is closed and t is compact, but s +ᵥ t is the set of all rationals, which is definitely not closed in . To fix the proof, we would need to make two additional assumptions:

                                                          theorem IsOpen.add_left {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} {t : Set α} :
                                                          IsOpen tIsOpen (s + t)
                                                          theorem IsOpen.mul_left {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} {t : Set α} :
                                                          IsOpen tIsOpen (s * t)
                                                          theorem subset_interior_add_right {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} {t : Set α} :
                                                          s + interior t interior (s + t)
                                                          theorem subset_interior_mul_right {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} {t : Set α} :
                                                          s * interior t interior (s * t)
                                                          theorem subset_interior_add {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} {t : Set α} :
                                                          theorem subset_interior_mul {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} {t : Set α} :
                                                          theorem singleton_add_mem_nhds {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} (a : α) {b : α} (h : s nhds b) :
                                                          {a} + s nhds (a + b)
                                                          theorem singleton_mul_mem_nhds {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} (a : α) {b : α} (h : s nhds b) :
                                                          {a} * s nhds (a * b)
                                                          theorem singleton_add_mem_nhds_of_nhds_zero {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} (a : α) (h : s nhds 0) :
                                                          {a} + s nhds a
                                                          theorem singleton_mul_mem_nhds_of_nhds_one {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} (a : α) (h : s nhds 1) :
                                                          {a} * s nhds a
                                                          theorem IsOpen.add_right {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} {t : Set α} (hs : IsOpen s) :
                                                          IsOpen (s + t)
                                                          theorem IsOpen.mul_right {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} {t : Set α} (hs : IsOpen s) :
                                                          IsOpen (s * t)
                                                          theorem subset_interior_mul_left {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} {t : Set α} :
                                                          interior s * t interior (s * t)
                                                          theorem subset_interior_mul' {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} {t : Set α} :
                                                          theorem add_singleton_mem_nhds {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} (a : α) {b : α} (h : s nhds b) :
                                                          s + {a} nhds (b + a)
                                                          theorem mul_singleton_mem_nhds {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} (a : α) {b : α} (h : s nhds b) :
                                                          s * {a} nhds (b * a)
                                                          theorem add_singleton_mem_nhds_of_nhds_zero {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} (a : α) (h : s nhds 0) :
                                                          s + {a} nhds a
                                                          theorem mul_singleton_mem_nhds_of_nhds_one {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} (a : α) (h : s nhds 1) :
                                                          s * {a} nhds a
                                                          theorem IsOpen.sub_left {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} {t : Set G} (ht : IsOpen t) :
                                                          IsOpen (s - t)
                                                          theorem IsOpen.div_left {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} (ht : IsOpen t) :
                                                          IsOpen (s / t)
                                                          theorem IsOpen.sub_right {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} {t : Set G} (hs : IsOpen s) :
                                                          IsOpen (s - t)
                                                          theorem IsOpen.div_right {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} (hs : IsOpen s) :
                                                          IsOpen (s / t)
                                                          theorem subset_interior_div_left {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} :
                                                          interior s / t interior (s / t)
                                                          theorem subset_interior_div_right {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} :
                                                          s / interior t interior (s / t)
                                                          theorem IsOpen.add_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) :
                                                          s + closure t = s + t
                                                          theorem IsOpen.mul_closure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) :
                                                          s * closure t = s * t
                                                          theorem IsOpen.closure_add {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) :
                                                          closure s + t = s + t
                                                          theorem IsOpen.closure_mul {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) :
                                                          closure s * t = s * t
                                                          theorem IsOpen.sub_closure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) :
                                                          s - closure t = s - t
                                                          theorem IsOpen.div_closure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) :
                                                          s / closure t = s / t
                                                          theorem IsOpen.closure_sub {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) :
                                                          closure s - t = s - t
                                                          theorem IsOpen.closure_div {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) :
                                                          closure s / t = s / t
                                                          theorem IsClosed.add_left_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} {t : Set G} (ht : IsClosed t) (hs : IsCompact s) :
                                                          IsClosed (s + t)
                                                          theorem IsClosed.mul_left_of_isCompact {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} (ht : IsClosed t) (hs : IsCompact s) :
                                                          IsClosed (s * t)
                                                          theorem IsClosed.add_right_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} {t : Set G} (ht : IsClosed t) (hs : IsCompact s) :
                                                          IsClosed (t + s)
                                                          theorem IsClosed.mul_right_of_isCompact {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} {t : Set G} (ht : IsClosed t) (hs : IsCompact s) :
                                                          IsClosed (t * s)
                                                          theorem QuotientGroup.isClosedMap_coe {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {H : Subgroup G} (hH : IsCompact H) :
                                                          IsClosedMap QuotientGroup.mk
                                                          theorem subset_add_closure_zero {G : Type w} [TopologicalSpace G] [AddGroup G] (s : Set G) :
                                                          s s + closure {0}
                                                          theorem subset_mul_closure_one {G : Type w} [TopologicalSpace G] [Group G] (s : Set G) :
                                                          s s * closure {1}
                                                          theorem IsClosed.mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {F : Set G} (hF : IsClosed F) :
                                                          F * closure {1} = F
                                                          theorem compl_add_closure_zero_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {t : Set G} (ht : t + closure {0} = t) :
                                                          t + closure {0} = t
                                                          theorem compl_mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {t : Set G} (ht : t * closure {1} = t) :
                                                          t * closure {1} = t
                                                          theorem IsOpen.mul_closure_one_eq {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {U : Set G} (hU : IsOpen U) :
                                                          U * closure {1} = U
                                                          theorem group_inseparable_iff {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {x : G} {y : G} :
                                                          theorem TopologicalAddGroup.t2Space_of_zero_sep {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (H : ∀ (x : G), x 0∃ U ∈ nhds 0, xU) :
                                                          theorem TopologicalGroup.t2Space_of_one_sep {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (H : ∀ (x : G), x 1∃ U ∈ nhds 1, xU) :
                                                          theorem exists_closed_nhds_zero_neg_eq_add_subset {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {U : Set G} (hU : U nhds 0) :
                                                          ∃ V ∈ nhds 0, IsClosed V -V = V V + V U

                                                          Given a neighborhood U of the identity, one may find a neighborhood V of the identity which is closed, symmetric, and satisfies V + V ⊆ U.

                                                          theorem exists_closed_nhds_one_inv_eq_mul_subset {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {U : Set G} (hU : U nhds 1) :
                                                          ∃ V ∈ nhds 1, IsClosed V V⁻¹ = V V * V U

                                                          Given a neighborhood U of the identity, one may find a neighborhood V of the identity which is closed, symmetric, and satisfies V * V ⊆ U.

                                                          Equations
                                                          • =

                                                          A subgroup S of an additive topological group G acts on G properly discontinuously on the left, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also DiscreteTopology.

                                                          A subgroup S of a topological group G acts on G properly discontinuously on the left, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also DiscreteTopology.)

                                                          A subgroup S of an additive topological group G acts on G properly discontinuously on the right, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also DiscreteTopology.)

                                                          If G is Hausdorff, this can be combined with t2Space_of_properlyDiscontinuousVAdd_of_t2Space to show that the quotient group G ⧸ S is Hausdorff.

                                                          A subgroup S of a topological group G acts on G properly discontinuously on the right, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also DiscreteTopology.)

                                                          If G is Hausdorff, this can be combined with t2Space_of_properlyDiscontinuousSMul_of_t2Space to show that the quotient group G ⧸ S is Hausdorff.

                                                          Some results about an open set containing the product of two sets in a topological group.

                                                          theorem compact_open_separated_add_right {G : Type w} [TopologicalSpace G] [AddZeroClass G] [ContinuousAdd G] {K : Set G} {U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K U) :
                                                          ∃ V ∈ nhds 0, K + V U

                                                          Given a compact set K inside an open set U, there is an open neighborhood V of 0 such that K + V ⊆ U.

                                                          theorem compact_open_separated_mul_right {G : Type w} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {K : Set G} {U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K U) :
                                                          ∃ V ∈ nhds 1, K * V U

                                                          Given a compact set K inside an open set U, there is an open neighborhood V of 1 such that K * V ⊆ U.

                                                          theorem compact_open_separated_add_left {G : Type w} [TopologicalSpace G] [AddZeroClass G] [ContinuousAdd G] {K : Set G} {U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K U) :
                                                          ∃ V ∈ nhds 0, V + K U

                                                          Given a compact set K inside an open set U, there is an open neighborhood V of 0 such that V + K ⊆ U.

                                                          theorem compact_open_separated_mul_left {G : Type w} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {K : Set G} {U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K U) :
                                                          ∃ V ∈ nhds 1, V * K U

                                                          Given a compact set K inside an open set U, there is an open neighborhood V of 1 such that V * K ⊆ U.

                                                          theorem compact_covered_by_add_left_translates {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {K : Set G} {V : Set G} (hK : IsCompact K) (hV : Set.Nonempty (interior V)) :
                                                          ∃ (t : Finset G), K ⋃ g ∈ t, (fun (x : G) => g + x) ⁻¹' V

                                                          A compact set is covered by finitely many left additive translates of a set with non-empty interior.

                                                          theorem compact_covered_by_mul_left_translates {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {K : Set G} {V : Set G} (hK : IsCompact K) (hV : Set.Nonempty (interior V)) :
                                                          ∃ (t : Finset G), K ⋃ g ∈ t, (fun (x : G) => g * x) ⁻¹' V

                                                          A compact set is covered by finitely many left multiplicative translates of a set with non-empty interior.

                                                          Every weakly locally compact separable topological additive group is σ-compact. Note: this is not true if we drop the topological group hypothesis.

                                                          Equations
                                                          • =

                                                          Every weakly locally compact separable topological group is σ-compact. Note: this is not true if we drop the topological group hypothesis.

                                                          Equations
                                                          • =
                                                          theorem exists_disjoint_vadd_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [NoncompactSpace G] {K : Set G} {L : Set G} (hK : IsCompact K) (hL : IsCompact L) :
                                                          ∃ (g : G), Disjoint K (g +ᵥ L)

                                                          Given two compact sets in a noncompact additive topological group, there is a translate of the second one that is disjoint from the first one.

                                                          theorem exists_disjoint_smul_of_isCompact {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] [NoncompactSpace G] {K : Set G} {L : Set G} (hK : IsCompact K) (hL : IsCompact L) :
                                                          ∃ (g : G), Disjoint K (g L)

                                                          Given two compact sets in a noncompact topological group, there is a translate of the second one that is disjoint from the first one.

                                                          @[deprecated IsCompact.isCompact_isClosed_basis_nhds]

                                                          A compact neighborhood of 0 in a topological additive group admits a closed compact subset that is a neighborhood of 0.

                                                          abbrev exists_isCompact_isClosed_subset_isCompact_nhds_zero.match_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] {L : Set G} (motive : (∃ (i : Set G), (i nhds 0 IsCompact i IsClosed i) i L)Prop) :
                                                          ∀ (x : ∃ (i : Set G), (i nhds 0 IsCompact i IsClosed i) i L), (∀ (K : Set G) (hK : K nhds 0) (hK₁ : IsCompact K) (hK₂ : IsClosed K) (hKL : K L), motive )motive x
                                                          Equations
                                                          • =
                                                          Instances For
                                                            @[deprecated IsCompact.isCompact_isClosed_basis_nhds]
                                                            theorem exists_isCompact_isClosed_subset_isCompact_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {L : Set G} (Lcomp : IsCompact L) (L1 : L nhds 1) :
                                                            ∃ (K : Set G), IsCompact K IsClosed K K L K nhds 1

                                                            A compact neighborhood of 1 in a topological group admits a closed compact subset that is a neighborhood of 1.

                                                            If a point in a topological group has a compact neighborhood, then the group is locally compact.

                                                            @[deprecated WeaklyLocallyCompactSpace.locallyCompactSpace]
                                                            @[deprecated WeaklyLocallyCompactSpace.locallyCompactSpace]

                                                            A topological group which is weakly locally compact is automatically locally compact.

                                                            If a function defined on a topological additive group has a support contained in a compact set, then either the function is trivial or the group is locally compact.

                                                            If a function defined on a topological group has a support contained in a compact set, then either the function is trivial or the group is locally compact.

                                                            If a function defined on a topological additive group has compact support, then either the function is trivial or the group is locally compact.

                                                            If a function defined on a topological group has compact support, then either the function is trivial or the group is locally compact.

                                                            @[deprecated isCompact_isClosed_basis_nhds]

                                                            In a locally compact additive group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space.

                                                            @[deprecated isCompact_isClosed_basis_nhds]

                                                            In a locally compact group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space.

                                                            abbrev exists_isCompact_isClosed_nhds_zero.match_1 (G : Type u_1) [TopologicalSpace G] [AddGroup G] (motive : (∃ K ∈ nhds 0, IsCompact K IsClosed K)Prop) :
                                                            ∀ (x : ∃ K ∈ nhds 0, IsCompact K IsClosed K), (∀ (K : Set G) (hK₁ : K nhds 0) (hKcomp : IsCompact K) (hKcl : IsClosed K), motive )motive x
                                                            Equations
                                                            • =
                                                            Instances For
                                                              @[deprecated exists_mem_nhds_isCompact_isClosed]
                                                              @[deprecated exists_mem_nhds_isCompact_isClosed]

                                                              A quotient of a locally compact group is locally compact.

                                                              Equations
                                                              • =
                                                              theorem nhds_add {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) (y : G) :
                                                              nhds (x + y) = nhds x + nhds y
                                                              theorem nhds_mul {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) (y : G) :
                                                              nhds (x * y) = nhds x * nhds y

                                                              On an additive topological group, 𝓝 : G → Filter G can be promoted to an AddHom.

                                                              Equations
                                                              • nhdsAddHom = { toFun := nhds, map_add' := }
                                                              Instances For
                                                                @[simp]
                                                                theorem nhdsAddHom_apply {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) :
                                                                nhdsAddHom x = nhds x
                                                                @[simp]
                                                                theorem nhdsMulHom_apply {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) :
                                                                nhdsMulHom x = nhds x

                                                                On a topological group, 𝓝 : G → Filter G can be promoted to a MulHom.

                                                                Equations
                                                                • nhdsMulHom = { toFun := nhds, map_mul' := }
                                                                Instances For
                                                                  Equations
                                                                  • =
                                                                  theorem QuotientAddGroup.continuous_smul₁ {G : Type w} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] {Γ : AddSubgroup G} (x : G Γ) :
                                                                  Continuous fun (g : G) => g +ᵥ x
                                                                  theorem QuotientGroup.continuous_smul₁ {G : Type w} [Group G] [TopologicalSpace G] [ContinuousMul G] {Γ : Subgroup G} (x : G Γ) :
                                                                  Continuous fun (g : G) => g x

                                                                  The quotient of a second countable additive topological group by a subgroup is second countable.

                                                                  Equations
                                                                  • =

                                                                  The quotient of a second countable topological group by a subgroup is second countable.

                                                                  Equations
                                                                  • =

                                                                  If G is an additive group with topological negation, then it is homeomorphic to its additive units.

                                                                  Equations
                                                                  • toAddUnits_homeomorph = { toEquiv := toAddUnits.toEquiv, continuous_toFun := , continuous_invFun := }
                                                                  Instances For

                                                                    If G is a group with topological ⁻¹, then it is homeomorphic to its units.

                                                                    Equations
                                                                    • toUnits_homeomorph = { toEquiv := toUnits.toEquiv, continuous_toFun := , continuous_invFun := }
                                                                    Instances For
                                                                      theorem AddUnits.Homeomorph.sumAddUnits.proof_2 {α : Type u_1} {β : Type u_2} [AddMonoid α] [TopologicalSpace α] [AddMonoid β] [TopologicalSpace β] :
                                                                      Continuous AddEquiv.prodAddUnits.invFun

                                                                      The topological group isomorphism between the additive units of a product of two additive monoids, and the product of the additive units of each additive monoid.

                                                                      Equations
                                                                      • AddUnits.Homeomorph.sumAddUnits = { toEquiv := AddEquiv.prodAddUnits.toEquiv, continuous_toFun := , continuous_invFun := }
                                                                      Instances For
                                                                        def Units.Homeomorph.prodUnits {α : Type u} {β : Type v} [Monoid α] [TopologicalSpace α] [Monoid β] [TopologicalSpace β] :
                                                                        (α × β)ˣ ≃ₜ αˣ × βˣ

                                                                        The topological group isomorphism between the units of a product of two monoids, and the product of the units of each monoid.

                                                                        Equations
                                                                        • Units.Homeomorph.prodUnits = { toEquiv := MulEquiv.prodUnits.toEquiv, continuous_toFun := , continuous_invFun := }
                                                                        Instances For
                                                                          theorem topologicalGroup_sInf {G : Type w} [Group G] {ts : Set (TopologicalSpace G)} (h : tts, TopologicalGroup G) :
                                                                          theorem topologicalAddGroup_iInf {G : Type w} {ι : Sort u_1} [AddGroup G] {ts' : ιTopologicalSpace G} (h' : ∀ (i : ι), TopologicalAddGroup G) :
                                                                          theorem topologicalGroup_iInf {G : Type w} {ι : Sort u_1} [Group G] {ts' : ιTopologicalSpace G} (h' : ∀ (i : ι), TopologicalGroup G) :

                                                                          Lattice of group topologies #

                                                                          We define a type class GroupTopology α which endows a group α with a topology such that all group operations are continuous.

                                                                          Group topologies on a fixed group α are ordered, by reverse inclusion. They form a complete lattice, with the discrete topology and the indiscrete topology.

                                                                          Any function f : α → β induces coinduced f : TopologicalSpace α → GroupTopology β.

                                                                          The additive version AddGroupTopology α and corresponding results are provided as well.

                                                                          structure GroupTopology (α : Type u) [Group α] extends TopologicalSpace , TopologicalGroup :

                                                                          A group topology on a group α is a topology for which multiplication and inversion are continuous.

                                                                            Instances For

                                                                              An additive group topology on an additive group α is a topology for which addition and negation are continuous.

                                                                                Instances For
                                                                                  theorem AddGroupTopology.continuous_add' {α : Type u} [AddGroup α] (g : AddGroupTopology α) :
                                                                                  Continuous fun (p : α × α) => p.1 + p.2

                                                                                  A version of the global continuous_add suitable for dot notation.

                                                                                  theorem GroupTopology.continuous_mul' {α : Type u} [Group α] (g : GroupTopology α) :
                                                                                  Continuous fun (p : α × α) => p.1 * p.2

                                                                                  A version of the global continuous_mul suitable for dot notation.

                                                                                  A version of the global continuous_neg suitable for dot notation.

                                                                                  theorem GroupTopology.continuous_inv' {α : Type u} [Group α] (g : GroupTopology α) :
                                                                                  Continuous Inv.inv

                                                                                  A version of the global continuous_inv suitable for dot notation.

                                                                                  theorem AddGroupTopology.toTopologicalSpace_injective {α : Type u} [AddGroup α] :
                                                                                  Function.Injective AddGroupTopology.toTopologicalSpace
                                                                                  theorem GroupTopology.toTopologicalSpace_injective {α : Type u} [Group α] :
                                                                                  Function.Injective GroupTopology.toTopologicalSpace
                                                                                  theorem AddGroupTopology.ext' {α : Type u} [AddGroup α] {f : AddGroupTopology α} {g : AddGroupTopology α} (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) :
                                                                                  f = g
                                                                                  theorem GroupTopology.ext' {α : Type u} [Group α] {f : GroupTopology α} {g : GroupTopology α} (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) :
                                                                                  f = g

                                                                                  The ordering on group topologies on the group γ. t ≤ s if every set open in s is also open in t (t is finer than s).

                                                                                  Equations
                                                                                  • AddGroupTopology.instPartialOrderAddGroupTopology = PartialOrder.lift AddGroupTopology.toTopologicalSpace

                                                                                  The ordering on group topologies on the group γ. t ≤ s if every set open in s is also open in t (t is finer than s).

                                                                                  Equations
                                                                                  • GroupTopology.instPartialOrderGroupTopology = PartialOrder.lift GroupTopology.toTopologicalSpace
                                                                                  @[simp]
                                                                                  theorem AddGroupTopology.toTopologicalSpace_le {α : Type u} [AddGroup α] {x : AddGroupTopology α} {y : AddGroupTopology α} :
                                                                                  x.toTopologicalSpace y.toTopologicalSpace x y
                                                                                  @[simp]
                                                                                  theorem GroupTopology.toTopologicalSpace_le {α : Type u} [Group α] {x : GroupTopology α} {y : GroupTopology α} :
                                                                                  x.toTopologicalSpace y.toTopologicalSpace x y
                                                                                  Equations
                                                                                  • AddGroupTopology.instTopAddGroupTopology = let _t := ; { top := { toTopologicalSpace := _t, toTopologicalAddGroup := } }
                                                                                  Equations
                                                                                  • GroupTopology.instTopGroupTopology = let _t := ; { top := { toTopologicalSpace := _t, toTopologicalGroup := } }
                                                                                  @[simp]
                                                                                  theorem AddGroupTopology.toTopologicalSpace_top {α : Type u} [AddGroup α] :
                                                                                  .toTopologicalSpace =
                                                                                  @[simp]
                                                                                  theorem GroupTopology.toTopologicalSpace_top {α : Type u} [Group α] :
                                                                                  .toTopologicalSpace =
                                                                                  Equations
                                                                                  • AddGroupTopology.instBotAddGroupTopology = let _t := ; { bot := { toTopologicalSpace := _t, toTopologicalAddGroup := } }
                                                                                  Equations
                                                                                  • GroupTopology.instBotGroupTopology = let _t := ; { bot := { toTopologicalSpace := _t, toTopologicalGroup := } }
                                                                                  @[simp]
                                                                                  theorem AddGroupTopology.toTopologicalSpace_bot {α : Type u} [AddGroup α] :
                                                                                  .toTopologicalSpace =
                                                                                  @[simp]
                                                                                  theorem GroupTopology.toTopologicalSpace_bot {α : Type u} [Group α] :
                                                                                  .toTopologicalSpace =
                                                                                  Equations
                                                                                  • AddGroupTopology.instBoundedOrderAddGroupTopologyToLEToPreorderInstPartialOrderAddGroupTopology = BoundedOrder.mk
                                                                                  Equations
                                                                                  • GroupTopology.instBoundedOrderGroupTopologyToLEToPreorderInstPartialOrderGroupTopology = BoundedOrder.mk
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Equations
                                                                                  • GroupTopology.instInfGroupTopology = { inf := fun (x y : GroupTopology α) => { toTopologicalSpace := x.toTopologicalSpace y.toTopologicalSpace, toTopologicalGroup := } }
                                                                                  @[simp]
                                                                                  theorem AddGroupTopology.toTopologicalSpace_inf {α : Type u} [AddGroup α] (x : AddGroupTopology α) (y : AddGroupTopology α) :
                                                                                  (x y).toTopologicalSpace = x.toTopologicalSpace y.toTopologicalSpace
                                                                                  @[simp]
                                                                                  theorem GroupTopology.toTopologicalSpace_inf {α : Type u} [Group α] (x : GroupTopology α) (y : GroupTopology α) :
                                                                                  (x y).toTopologicalSpace = x.toTopologicalSpace y.toTopologicalSpace
                                                                                  Equations
                                                                                  Equations
                                                                                  Equations
                                                                                  • AddGroupTopology.instInhabitedAddGroupTopology = { default := }
                                                                                  Equations
                                                                                  • GroupTopology.instInhabitedGroupTopology = { default := }

                                                                                  Infimum of a collection of additive group topologies

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.

                                                                                  Infimum of a collection of group topologies.

                                                                                  Equations
                                                                                  • GroupTopology.instInfSetGroupTopology = { sInf := fun (S : Set (GroupTopology α)) => { toTopologicalSpace := sInf (GroupTopology.toTopologicalSpace '' S), toTopologicalGroup := } }
                                                                                  @[simp]
                                                                                  theorem AddGroupTopology.toTopologicalSpace_sInf {α : Type u} [AddGroup α] (s : Set (AddGroupTopology α)) :
                                                                                  (sInf s).toTopologicalSpace = sInf (AddGroupTopology.toTopologicalSpace '' s)
                                                                                  @[simp]
                                                                                  theorem GroupTopology.toTopologicalSpace_sInf {α : Type u} [Group α] (s : Set (GroupTopology α)) :
                                                                                  (sInf s).toTopologicalSpace = sInf (GroupTopology.toTopologicalSpace '' s)
                                                                                  @[simp]
                                                                                  theorem AddGroupTopology.toTopologicalSpace_iInf {α : Type u} [AddGroup α] {ι : Sort u_1} (s : ιAddGroupTopology α) :
                                                                                  (⨅ (i : ι), s i).toTopologicalSpace = ⨅ (i : ι), (s i).toTopologicalSpace
                                                                                  @[simp]
                                                                                  theorem GroupTopology.toTopologicalSpace_iInf {α : Type u} [Group α] {ι : Sort u_1} (s : ιGroupTopology α) :
                                                                                  (⨅ (i : ι), s i).toTopologicalSpace = ⨅ (i : ι), (s i).toTopologicalSpace
                                                                                  theorem AddGroupTopology.instCompleteSemilatticeInfAddGroupTopology.proof_2 {α : Type u_1} [AddGroup α] (S : Set (AddGroupTopology α)) (a : AddGroupTopology α) (hab : bS, a b) :
                                                                                  a.toTopologicalSpace sInf (AddGroupTopology.toTopologicalSpace '' S)

                                                                                  Group topologies on γ form a complete lattice, with the discrete topology and the indiscrete topology.

                                                                                  The infimum of a collection of group topologies is the topology generated by all their open sets (which is a group topology).

                                                                                  The supremum of two group topologies s and t is the infimum of the family of all group topologies contained in the intersection of s and t.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.

                                                                                  Group topologies on γ form a complete lattice, with the discrete topology and the indiscrete topology.

                                                                                  The infimum of a collection of group topologies is the topology generated by all their open sets (which is a group topology).

                                                                                  The supremum of two group topologies s and t is the infimum of the family of all group topologies contained in the intersection of s and t.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  def AddGroupTopology.coinduced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [AddGroup β] (f : αβ) :

                                                                                  Given f : α → β and a topology on α, the coinduced additive group topology on β is the finest topology such that f is continuous and β is a topological additive group.

                                                                                  Equations
                                                                                  Instances For
                                                                                    def GroupTopology.coinduced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [Group β] (f : αβ) :

                                                                                    Given f : α → β and a topology on α, the coinduced group topology on β is the finest topology such that f is continuous and β is a topological group.

                                                                                    Equations
                                                                                    Instances For
                                                                                      theorem AddGroupTopology.coinduced_continuous {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [AddGroup β] (f : αβ) :
                                                                                      theorem GroupTopology.coinduced_continuous {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [Group β] (f : αβ) :