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

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

Equations
Instances For
    theorem Homeomorph.addLeft.proof_2 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
    Continuous fun (x : G) => (-toAddUnits a) + x
    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) :

      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)
        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)
        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
            theorem ContinuousNeg.continuous_neg {G : Type u} :
            ∀ {inst : TopologicalSpace G} {inst_1 : Neg G} [self : ContinuousNeg G], Continuous fun (a : G) => -a
            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 ContinuousInv.continuous_inv {G : Type u} :
              ∀ {inst : TopologicalSpace G} {inst_1 : Inv G} [self : ContinuousInv G], Continuous fun (a : G) => a⁻¹
              theorem ContinuousNeg.induced {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F α β] [AddGroup α] [AddGroup β] [AddMonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousNeg β] (f : F) :
              theorem ContinuousInv.induced {α : Type u_1} {β : Type u_2} {F : Type u_3} [FunLike F α β] [Group α] [Group β] [MonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousInv β] (f : F) :
              theorem Specializes.neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x : G} {y : G} (h : x y) :
              (-x) (-y)
              theorem Specializes.inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x : G} {y : G} (h : x y) :
              theorem Inseparable.neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x : G} {y : G} (h : Inseparable x y) :
              theorem Inseparable.inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x : G} {y : G} (h : Inseparable x y) :
              theorem Specializes.zsmul {G : Type u_1} [SubNegMonoid G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousNeg G] {x : G} {y : G} (h : x y) (m : ) :
              (m x) (m y)
              theorem Specializes.zpow {G : Type u_1} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x : G} {y : G} (h : x y) (m : ) :
              (x ^ m) (y ^ m)
              theorem Inseparable.zsmul {G : Type u_1} [SubNegMonoid G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousNeg G] {x : G} {y : G} (h : Inseparable x y) (m : ) :
              Inseparable (m x) (m y)
              theorem Inseparable.zpow {G : Type u_1} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x : G} {y : G} (h : Inseparable x y) (m : ) :
              Inseparable (x ^ m) (y ^ m)
              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
              • =
              @[instance 100]
              Equations
              • =
              @[instance 100]
              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 nhds_neg (G : Type w) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] (a : G) :
                  nhds (-a) = -nhds a
                  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) :
                  @[simp]
                  theorem continuous_neg_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} :
                  @[simp]
                  @[simp]
                  theorem continuousAt_neg_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} {x : α} :
                  @[simp]
                  theorem continuousAt_inv_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} {x : α} :
                  @[simp]
                  theorem continuousOn_neg_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} {s : Set α} :
                  @[simp]
                  theorem continuousOn_inv_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} {s : Set α} :
                  theorem Continuous.of_inv {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} :

                  Alias of the forward direction of continuous_inv_iff.

                  theorem Continuous.of_neg {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} :
                  theorem ContinuousAt.of_inv {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} {x : α} :

                  Alias of the forward direction of continuousAt_inv_iff.

                  theorem ContinuousAt.of_neg {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} {x : α} :
                  theorem ContinuousOn.of_inv {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} {s : Set α} :

                  Alias of the forward direction of continuousOn_inv_iff.

                  theorem ContinuousOn.of_neg {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} {s : Set α} :
                  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
                          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.symm (Equiv.addLeft ((Equiv.refl G).symm x.1))) 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]
                              theorem Homeomorph.shearAddRight_symm_coe (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] :
                              (Homeomorph.shearAddRight G).symm = fun (z : G × G) => (z.1, -z.1 + z.2)
                              @[simp]
                              theorem Homeomorph.shearMulRight_symm_coe (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] :
                              (Homeomorph.shearMulRight G).symm = fun (z : G × G) => (z.1, z.1⁻¹ * z.2)
                              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_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) :
                              ∀ {a b : G}, a s.topologicalClosure.carrierb s.topologicalClosure.carriera + b s.topologicalClosure.carrier

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

                              Equations
                              • s.topologicalClosure = { carrier := closure s, add_mem' := , zero_mem' := , neg_mem' := }
                              Instances For
                                theorem AddSubgroup.topologicalClosure.proof_3 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) {g : G} (hg : g { carrier := closure s, add_mem' := , zero_mem' := }.carrier) :
                                -g { carrier := closure s, add_mem' := , zero_mem' := }.carrier
                                theorem AddSubgroup.topologicalClosure.proof_2 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) :
                                0 s.topologicalClosure.carrier

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

                                Equations
                                • s.topologicalClosure = { carrier := closure s, mul_mem' := , one_mem' := , inv_mem' := }
                                Instances For
                                  @[simp]
                                  theorem AddSubgroup.topologicalClosure_coe {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : AddSubgroup G} :
                                  s.topologicalClosure = closure s
                                  @[simp]
                                  theorem Subgroup.topologicalClosure_coe {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Subgroup G} :
                                  s.topologicalClosure = closure s
                                  theorem Subgroup.le_topologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (s : Subgroup G) :
                                  s s.topologicalClosure
                                  theorem Subgroup.isClosed_topologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (s : Subgroup G) :
                                  IsClosed s.topologicalClosure
                                  theorem AddSubgroup.topologicalClosure_minimal {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) {t : AddSubgroup G} (h : s t) (ht : IsClosed t) :
                                  s.topologicalClosure t
                                  theorem Subgroup.topologicalClosure_minimal {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (s : Subgroup G) {t : Subgroup G} (h : s t) (ht : IsClosed t) :
                                  s.topologicalClosure t
                                  theorem DenseRange.topologicalClosure_map_addSubgroup {G : Type w} {H : Type x} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [AddGroup H] [TopologicalSpace H] [TopologicalAddGroup H] {f : G →+ H} (hf : Continuous f) (hf' : DenseRange f) {s : AddSubgroup G} (hs : s.topologicalClosure = ) :
                                  (AddSubgroup.map f s).topologicalClosure =
                                  theorem DenseRange.topologicalClosure_map_subgroup {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] [Group H] [TopologicalSpace H] [TopologicalGroup H] {f : G →* H} (hf : Continuous f) (hf' : DenseRange f) {s : Subgroup G} (hs : s.topologicalClosure = ) :
                                  (Subgroup.map f s).topologicalClosure =
                                  theorem AddSubgroup.is_normal_topologicalClosure {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] :
                                  N.topologicalClosure.Normal

                                  The topological closure of a normal additive subgroup is normal.

                                  theorem Subgroup.is_normal_topologicalClosure {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] (N : Subgroup G) [N.Normal] :
                                  N.topologicalClosure.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
                                      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 : s.topologicalClosure) (b : s.topologicalClosure) :
                                      a + b = b + a
                                      def AddSubgroup.addCommGroupTopologicalClosure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [T2Space G] (s : AddSubgroup G) (hs : ∀ (x y : s), x + y = y + x) :
                                      AddCommGroup s.topologicalClosure

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

                                      Equations
                                      Instances For
                                        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) :
                                        CommGroup s.topologicalClosure

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

                                        Equations
                                        Instances For
                                          theorem Subgroup.coe_topologicalClosure_bot (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] :
                                          .topologicalClosure = closure {1}
                                          theorem exists_nhds_half_neg {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} (hs : s nhds 0) :
                                          Vnhds 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) :
                                          Vnhds 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 : (nhds 0).HasBasis p s) (x : G) :
                                          (nhds x).HasBasis 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 : (nhds 1).HasBasis p s) (x : G) :
                                          (nhds x).HasBasis 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, ys, 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, ys, 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
                                          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 (x1 x2 : G) => x1 + x2) (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 (x1 x2 : G) => x1 * x2) (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 (x1 x2 : G) => x1 + x2) (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 (x1 x2 : G) => x1 * x2) (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 (x1 x2 : G) => x1 + x2) (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 (x1 x2 : G) => x1 * x2) (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 TopologicalAddGroup.exists_antitone_basis_nhds_zero (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [FirstCountableTopology G] :
                                          ∃ (u : Set G), (nhds 0).HasAntitoneBasis u ∀ (n : ), u (n + 1) + u (n + 1) u n

                                          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

                                          theorem TopologicalGroup.exists_antitone_basis_nhds_one (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] [FirstCountableTopology G] :
                                          ∃ (u : Set G), (nhds 1).HasAntitoneBasis u ∀ (n : ), u (n + 1) * u (n + 1) u n

                                          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

                                          Equations
                                          theorem QuotientAddGroup.quotientMap_mk {G : Type w} [TopologicalSpace G] [AddGroup G] (N : AddSubgroup G) :
                                          QuotientMap QuotientAddGroup.mk
                                          theorem QuotientGroup.quotientMap_mk {G : Type w} [TopologicalSpace G] [Group G] (N : Subgroup G) :
                                          QuotientMap QuotientGroup.mk
                                          theorem QuotientAddGroup.continuous_mk {G : Type w} [TopologicalSpace G] [AddGroup G] {N : AddSubgroup G} :
                                          Continuous QuotientAddGroup.mk
                                          theorem QuotientGroup.continuous_mk {G : Type w} [TopologicalSpace G] [Group G] {N : Subgroup G} :
                                          Continuous QuotientGroup.mk
                                          theorem QuotientGroup.isOpenMap_coe {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} :
                                          IsOpenMap QuotientGroup.mk
                                          @[simp]
                                          theorem QuotientAddGroup.dense_preimage_mk {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} {s : Set (G N)} :
                                          Dense (QuotientAddGroup.mk ⁻¹' s) Dense s
                                          @[simp]
                                          theorem QuotientGroup.dense_preimage_mk {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} {s : Set (G N)} :
                                          Dense (QuotientGroup.mk ⁻¹' s) Dense s
                                          theorem QuotientAddGroup.dense_image_mk {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} {s : Set G} :
                                          Dense (QuotientAddGroup.mk '' s) Dense (s + N)
                                          theorem QuotientGroup.dense_image_mk {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} {s : Set G} :
                                          Dense (QuotientGroup.mk '' s) Dense (s * N)
                                          Equations
                                          • =
                                          theorem QuotientAddGroup.nhds_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd 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] [ContinuousMul 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.

                                          @[deprecated]
                                          theorem QuotientAddGroup.nhds_zero_isCountablyGenerated {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (N : AddSubgroup G) [FirstCountableTopology G] [N.Normal] :
                                          (nhds 0).IsCountablyGenerated
                                          @[deprecated]
                                          theorem QuotientGroup.nhds_one_isCountablyGenerated {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (N : Subgroup G) [FirstCountableTopology G] [N.Normal] :
                                          (nhds 1).IsCountablyGenerated
                                          Equations
                                          • =
                                          @[deprecated]
                                          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
                                            theorem ContinuousSub.continuous_sub {G : Type u_1} :
                                            ∀ {inst : TopologicalSpace G} {inst_1 : Sub G} [self : ContinuousSub G], Continuous fun (p : G × G) => p.1 - p.2
                                            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 ContinuousDiv.continuous_div' {G : Type u_1} :
                                              ∀ {inst : TopologicalSpace G} {inst_1 : Div G} [self : ContinuousDiv G], Continuous fun (p : G × G) => p.1 / p.2
                                              @[instance 100]
                                              Equations
                                              • =
                                              @[instance 100]
                                              Equations
                                              • =
                                              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_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
                                                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
                                                @[simp]
                                                theorem Homeomorph.subLeft_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) :
                                                @[simp]
                                                theorem Homeomorph.subLeft_symm_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) :
                                                (Homeomorph.subLeft x).symm b = -b + x
                                                @[simp]
                                                theorem Homeomorph.divLeft_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) :
                                                @[simp]
                                                theorem Homeomorph.divLeft_symm_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) :
                                                (Homeomorph.divLeft x).symm b = b⁻¹ * x

                                                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_2 {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_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) :
                                                    Continuous fun (x_1 : G) => id x_1 - x
                                                    @[simp]
                                                    theorem Homeomorph.divRight_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) :
                                                    @[simp]
                                                    theorem Homeomorph.divRight_symm_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) :
                                                    (Homeomorph.divRight x).symm b = b * x
                                                    @[simp]
                                                    theorem Homeomorph.subRight_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) :
                                                    @[simp]
                                                    theorem Homeomorph.subRight_symm_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) :
                                                    (Homeomorph.subRight x).symm b = b + x

                                                    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 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 u_1} [AddZeroClass G] [TopologicalSpace G] (s : Set G) :
                                                      s s + closure {0}
                                                      theorem subset_mul_closure_one {G : Type u_1} [MulOneClass G] [TopologicalSpace 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
                                                      @[instance 100]
                                                      Equations
                                                      • =
                                                      @[instance 100]
                                                      Equations
                                                      • =
                                                      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 0Unhds 0, xU) :
                                                      theorem TopologicalGroup.t2Space_of_one_sep {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (H : ∀ (x : G), x 1Unhds 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) :
                                                      Vnhds 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) :
                                                      Vnhds 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.

                                                      instance AddSubgroup.t3_quotient_of_isClosed {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (S : AddSubgroup G) [S.Normal] [hS : IsClosed S] :
                                                      T3Space (G S)
                                                      Equations
                                                      • =
                                                      instance Subgroup.t3_quotient_of_isClosed {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (S : Subgroup G) [S.Normal] [hS : IsClosed S] :
                                                      T3Space (G S)
                                                      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) :
                                                      Vnhds 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) :
                                                      Vnhds 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) :
                                                      Vnhds 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) :
                                                      Vnhds 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 : (interior V).Nonempty) :
                                                      ∃ (t : Finset G), K gt, (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 : (interior V).Nonempty) :
                                                      ∃ (t : Finset G), K gt, (fun (x : G) => g * x) ⁻¹' V

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

                                                      @[instance 100]

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

                                                      Equations
                                                      • =
                                                      @[instance 100]

                                                      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.

                                                      @[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.

                                                      @[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

                                                              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
                                                                theorem AddUnits.Homeomorph.sumAddUnits.proof_2 {α : Type u_1} {β : Type u_2} [AddMonoid α] [TopologicalSpace α] [AddMonoid β] [TopologicalSpace β] :
                                                                Continuous AddEquiv.prodAddUnits.invFun
                                                                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'_iff {α : Type u} [Group α] {f : GroupTopology α} {g : GroupTopology α} :
                                                                          f = g TopologicalSpace.IsOpen = TopologicalSpace.IsOpen
                                                                          theorem AddGroupTopology.ext'_iff {α : Type u} [AddGroup α] {f : AddGroupTopology α} {g : AddGroupTopology α} :
                                                                          f = g TopologicalSpace.IsOpen = TopologicalSpace.IsOpen
                                                                          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.instPartialOrder = 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
                                                                          @[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.instTop = { top := { toTopologicalSpace := , toTopologicalAddGroup := } }
                                                                          instance GroupTopology.instTop {α : Type u} [Group α] :
                                                                          Equations
                                                                          • GroupTopology.instTop = { top := { toTopologicalSpace := , toTopologicalGroup := } }
                                                                          @[simp]
                                                                          theorem AddGroupTopology.toTopologicalSpace_top {α : Type u} [AddGroup α] :
                                                                          .toTopologicalSpace =
                                                                          @[simp]
                                                                          theorem GroupTopology.toTopologicalSpace_top {α : Type u} [Group α] :
                                                                          .toTopologicalSpace =
                                                                          Equations
                                                                          • AddGroupTopology.instBot = { bot := { toTopologicalSpace := , toTopologicalAddGroup := } }
                                                                          instance GroupTopology.instBot {α : Type u} [Group α] :
                                                                          Equations
                                                                          • GroupTopology.instBot = { bot := { toTopologicalSpace := , toTopologicalGroup := } }
                                                                          @[simp]
                                                                          theorem AddGroupTopology.toTopologicalSpace_bot {α : Type u} [AddGroup α] :
                                                                          .toTopologicalSpace =
                                                                          @[simp]
                                                                          theorem GroupTopology.toTopologicalSpace_bot {α : Type u} [Group α] :
                                                                          .toTopologicalSpace =
                                                                          theorem AddGroupTopology.instBoundedOrder.proof_1 {α : Type u_1} [AddGroup α] (x : AddGroupTopology α) :
                                                                          x.toTopologicalSpace
                                                                          Equations
                                                                          • AddGroupTopology.instBoundedOrder = BoundedOrder.mk
                                                                          theorem AddGroupTopology.instBoundedOrder.proof_2 {α : Type u_1} [AddGroup α] (x : AddGroupTopology α) :
                                                                          x.toTopologicalSpace
                                                                          Equations
                                                                          • GroupTopology.instBoundedOrder = BoundedOrder.mk
                                                                          Equations
                                                                          • AddGroupTopology.instInf = { inf := fun (x y : AddGroupTopology α) => { toTopologicalSpace := x.toTopologicalSpace y.toTopologicalSpace, toTopologicalAddGroup := } }
                                                                          instance GroupTopology.instInf {α : Type u} [Group α] :
                                                                          Equations
                                                                          • GroupTopology.instInf = { 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.instInhabited = { default := }
                                                                          Equations
                                                                          • GroupTopology.instInhabited = { default := }

                                                                          Infimum of a collection of additive group topologies

                                                                          Equations
                                                                          • AddGroupTopology.instInfSet = { sInf := fun (S : Set (AddGroupTopology α)) => { toTopologicalSpace := sInf (AddGroupTopology.toTopologicalSpace '' S), toTopologicalAddGroup := } }

                                                                          Infimum of a collection of group topologies.

                                                                          Equations
                                                                          • GroupTopology.instInfSet = { 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.instCompleteSemilatticeInf.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

                                                                          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
                                                                          Equations
                                                                          theorem AddGroupTopology.instCompleteLattice.proof_8 {α : Type u_1} [AddGroup α] (s : Set (AddGroupTopology α)) (a : AddGroupTopology α) :
                                                                          (∀ bs, b a)sSup s a
                                                                          theorem AddGroupTopology.instCompleteLattice.proof_6 {α : Type u_1} [AddGroup α] (a : AddGroupTopology α) (b : AddGroupTopology α) (c : AddGroupTopology α) :
                                                                          a ba ca b c
                                                                          theorem AddGroupTopology.instCompleteLattice.proof_10 {α : Type u_1} [AddGroup α] (s : Set (AddGroupTopology α)) (a : AddGroupTopology α) :
                                                                          (∀ bs, a b)a sInf s
                                                                          theorem AddGroupTopology.instCompleteLattice.proof_3 {α : Type u_1} [AddGroup α] (a : AddGroupTopology α) (b : AddGroupTopology α) (c : AddGroupTopology α) :
                                                                          a cb ca b c
                                                                          Equations
                                                                          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 : αβ) :