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

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Homeomorph.mulLeft {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
    G ≃ₜ G

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Homeomorph.coe_addLeft {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
      ↑(Homeomorph.addLeft a) = (fun x x_1 => x + x_1) a
      @[simp]
      theorem Homeomorph.coe_mulLeft {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
      ↑(Homeomorph.mulLeft a) = (fun x x_1 => x * x_1) a
      theorem isOpenMap_add_left {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
      IsOpenMap fun x => a + x
      theorem isOpenMap_mul_left {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
      IsOpenMap fun x => a * x
      theorem IsOpen.left_addCoset {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {U : Set G} (h : IsOpen U) (x : G) :
      theorem IsOpen.leftCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsOpen U) (x : G) :
      theorem isClosedMap_add_left {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
      IsClosedMap fun x => a + x
      theorem isClosedMap_mul_left {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
      IsClosedMap fun x => a * x
      theorem IsClosed.left_addCoset {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {U : Set G} (h : IsClosed U) (x : G) :
      theorem IsClosed.leftCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsClosed U) (x : G) :
      theorem Homeomorph.addRight.proof_2 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
      Continuous fun x => id x + ↑(-toAddUnits a)

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Homeomorph.addRight.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
        Continuous fun x => 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
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Homeomorph.coe_addRight {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
          ↑(Homeomorph.addRight a) = fun g => g + a
          @[simp]
          theorem Homeomorph.coe_mulRight {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
          ↑(Homeomorph.mulRight a) = fun g => g * a
          theorem isOpenMap_add_right {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) :
          IsOpenMap fun x => x + a
          theorem isOpenMap_mul_right {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
          IsOpenMap fun x => 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 => x + a
          theorem isClosedMap_mul_right {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) :
          IsClosedMap fun x => x * a
          theorem IsClosed.rightCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsClosed U) (x : G) :

          ContinuousInv and ContinuousNeg #

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

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

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

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

            Instances
              theorem continuousOn_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {s : Set G} :
              ContinuousOn Neg.neg s
              theorem continuousOn_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {s : Set G} :
              ContinuousOn Inv.inv s
              theorem continuousWithinAt_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {s : Set G} {x : G} :
              ContinuousWithinAt Neg.neg s x
              theorem continuousWithinAt_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {s : Set G} {x : G} :
              ContinuousWithinAt Inv.inv s x
              theorem continuousAt_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x : G} :
              ContinuousAt Neg.neg x
              theorem continuousAt_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x : G} :
              ContinuousAt Inv.inv x
              theorem tendsto_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] (a : G) :
              Filter.Tendsto Neg.neg (nhds a) (nhds (-a))
              theorem tendsto_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] (a : G) :
              Filter.Tendsto Inv.inv (nhds a) (nhds a⁻¹)
              theorem Filter.Tendsto.neg {α : Type u} {G : Type w} [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 {α : Type u} {G : Type w} [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 {α : Type u} {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} (hf : Continuous f) :
              Continuous fun x => -f x
              theorem Continuous.inv {α : Type u} {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} (hf : Continuous f) :
              Continuous fun x => (f x)⁻¹
              theorem ContinuousAt.neg {α : Type u} {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} {x : α} (hf : ContinuousAt f x) :
              ContinuousAt (fun x => -f x) x
              theorem ContinuousAt.inv {α : Type u} {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} {x : α} (hf : ContinuousAt f x) :
              ContinuousAt (fun x => (f x)⁻¹) x
              theorem ContinuousOn.neg {α : Type u} {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace α] {f : αG} {s : Set α} (hf : ContinuousOn f s) :
              ContinuousOn (fun x => -f x) s
              theorem ContinuousOn.inv {α : Type u} {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} {s : Set α} (hf : ContinuousOn f s) :
              ContinuousOn (fun x => (f x)⁻¹) s
              theorem ContinuousWithinAt.neg {α : Type u} {G : Type w} [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 {α : Type u} {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace α] {f : αG} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) :
              ContinuousWithinAt (fun x => (f x)⁻¹) s x
              theorem Pi.continuousNeg.proof_1 {ι : Type u_1} {C : ιType u_2} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Neg (C i)] [∀ (i : ι), ContinuousNeg (C i)] :
              ContinuousNeg ((i : ι) → C i)
              instance Pi.continuousNeg {ι : Type u_1} {C : ιType u_2} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Neg (C i)] [∀ (i : ι), ContinuousNeg (C i)] :
              ContinuousNeg ((i : ι) → C i)
              Equations
              instance Pi.continuousInv {ι : Type u_1} {C : ιType u_2} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Inv (C i)] [∀ (i : ι), ContinuousInv (C i)] :
              ContinuousInv ((i : ι) → C i)
              Equations
              instance Pi.has_continuous_neg' {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {ι : Type u_1} :
              ContinuousNeg (ιG)

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

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

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

              Equations
              theorem isClosed_setOf_map_neg (G₁ : Type u_2) (G₂ : Type u_3) [TopologicalSpace G₂] [T2Space G₂] [Neg G₁] [Neg G₂] [ContinuousNeg G₂] :
              IsClosed {f | ∀ (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 | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}

              Negation in a topological group as a homeomorphism.

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

                Inversion in a topological group as a homeomorphism.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem IsOpen.neg {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsOpen s) :
                  theorem IsOpen.inv {G : Type w} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsOpen s) :
                  theorem IsClosed.neg {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsClosed s) :
                  theorem continuousNeg_sInf {G : Type w} [Neg G] {ts : Set (TopologicalSpace G)} (h : ∀ (t : TopologicalSpace G), t tsContinuousNeg G) :
                  theorem continuousInv_sInf {G : Type w} [Inv G] {ts : Set (TopologicalSpace G)} (h : ∀ (t : TopologicalSpace G), t tsContinuousInv 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.fst + g.snd + -g.fst

                          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.fst * g.snd * g.fst⁻¹

                          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 + 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 * 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 + 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 * h * g⁻¹

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

                          abbrev continuous_zsmul.match_1 (motive : Prop) :
                          (x : ) → ((n : ) → motive (Int.ofNat n)) → ((n : ) → motive (Int.negSucc n)) → motive x
                          Equations
                          Instances For
                            theorem continuous_zpow {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (z : ) :
                            Continuous fun a => a ^ z
                            theorem Continuous.zsmul {α : Type u} {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace α] {f : αG} (h : Continuous f) (z : ) :
                            Continuous fun b => z f b
                            theorem Continuous.zpow {α : Type u} {G : Type w} [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 => z x) s
                            theorem continuousOn_zpow {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} (z : ) :
                            ContinuousOn (fun x => x ^ z) s
                            theorem continuousAt_zsmul {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) (z : ) :
                            ContinuousAt (fun x => z x) x
                            theorem continuousAt_zpow {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) (z : ) :
                            ContinuousAt (fun x => 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 {α : Type u} {G : Type w} [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 {α : Type u} {G : Type w} [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 {α : Type u} {G : Type w} [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 {α : Type u} {G : Type w} [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 {α : Type u} {G : Type w} [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 {α : Type u} {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace α] {f : αG} {s : Set α} (hf : ContinuousOn f s) (z : ) :
                            ContinuousOn (fun x => f x ^ z) s
                            theorem Pi.topologicalAddGroup.proof_1 {β : Type u_1} {C : βType u_2} [(b : β) → TopologicalSpace (C b)] [(b : β) → AddGroup (C b)] [∀ (b : β), TopologicalAddGroup (C b)] :
                            TopologicalAddGroup ((b : β) → C b)
                            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
                            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) :
                            theorem Homeomorph.shearAddRight.proof_1 (G : Type u_1) [AddGroup G] :
                            Function.LeftInverse (Equiv.prodShear (Equiv.refl G) Equiv.addLeft).invFun (Equiv.prodShear (Equiv.refl G) Equiv.addLeft).toFun

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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem Homeomorph.shearAddRight.proof_3 (G : Type u_1) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] :
                              Continuous fun x => (x.fst, ↑(Equiv.addLeft x.fst) x.snd)
                              theorem Homeomorph.shearAddRight.proof_4 (G : Type u_1) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] :
                              Continuous fun x => (x.fst, (Equiv.addLeft ((Equiv.refl G).symm x.fst)).symm x.snd)
                              theorem Homeomorph.shearAddRight.proof_2 (G : Type u_1) [AddGroup G] :
                              Function.RightInverse (Equiv.prodShear (Equiv.refl G) Equiv.addLeft).invFun (Equiv.prodShear (Equiv.refl G) Equiv.addLeft).toFun

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem Homeomorph.shearAddRight_coe (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] :
                                ↑(Homeomorph.shearAddRight G) = fun z => (z.fst, z.fst + z.snd)
                                @[simp]
                                theorem Homeomorph.shearMulRight_coe (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] :
                                ↑(Homeomorph.shearMulRight G) = fun z => (z.fst, z.fst * z.snd)
                                @[simp]
                                theorem Inducing.topologicalGroup {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] {F : Type u_1} [Group H] [TopologicalSpace H] [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] [MonoidHomClass F H G] (f : F) :
                                Equations
                                • One or more equations did not get rendered due to their size.
                                theorem AddSubgroup.topologicalClosure.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) :
                                ∀ {a b : G}, a (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrierb (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carriera + b (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrier

                                The (topological-space) closure of an additive subgroup of a space M with ContinuousAdd is itself an additive subgroup.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem AddSubgroup.topologicalClosure.proof_3 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) {g : G} (hg : g { toAddSubsemigroup := { carrier := closure s, add_mem' := (_ : ∀ {a b : G}, a (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrierb (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carriera + b (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrier) }, zero_mem' := (_ : 0 (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrier) }.toAddSubsemigroup.carrier) :
                                  -g { toAddSubsemigroup := { carrier := closure s, add_mem' := (_ : ∀ {a b : G}, a (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrierb (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carriera + b (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrier) }, zero_mem' := (_ : 0 (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrier) }.toAddSubsemigroup.carrier
                                  theorem AddSubgroup.topologicalClosure.proof_2 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) :
                                  0 (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrier

                                  The (topological-space) closure of a subgroup of a space M with ContinuousMul is itself a subgroup.

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

                                    The topological closure of a normal additive subgroup is normal.

                                    The topological closure of a normal subgroup is normal.

                                    The connected component of 0 is a subgroup of G.

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

                                      The connected component of 1 is a subgroup of G.

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

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

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

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

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem exists_nhds_half_neg {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : Set G} (hs : s nhds 0) :
                                            V, V nhds 0 ∀ (v : G), v V∀ (w : G), w Vv - w s
                                            theorem exists_nhds_split_inv {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Set G} (hs : s nhds 1) :
                                            V, V nhds 1 ∀ (v : G), v V∀ (w : G), w Vv / w s
                                            theorem nhds_translation_add_neg {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) :
                                            Filter.comap (fun y => y + -x) (nhds 0) = nhds x
                                            theorem nhds_translation_mul_inv {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) :
                                            Filter.comap (fun y => y * 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 x_1 => x + x_1) x) (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 x_1 => x * x_1) x) (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 x_1 => x + x_1) x) (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 x_1 => x * x_1) x) (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 z => z + 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 z => z * 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 y => y + 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 y => y * x) (nhds 1) = nhds x
                                            theorem Filter.HasBasis.nhds_of_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {ι : Sort u_1} {p : ιProp} {s : ιSet G} (hb : Filter.HasBasis (nhds 0) p s) (x : G) :
                                            Filter.HasBasis (nhds x) p fun i => {y | y - x s i}
                                            theorem Filter.HasBasis.nhds_of_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {ι : Sort u_1} {p : ιProp} {s : ιSet G} (hb : Filter.HasBasis (nhds 1) p s) (x : G) :
                                            Filter.HasBasis (nhds x) p fun i => {y | 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 ∀ (U : Set G), U nhds 0y, y s y - x U
                                            theorem mem_closure_iff_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {x : G} {s : Set G} :
                                            x closure s ∀ (U : Set G), U nhds 1y, y s y / x U
                                            theorem continuous_of_continuousAt_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {M : Type u_1} {hom : Type u_2} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] [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] [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.

                                            abbrev continuous_of_continuousAt_zero₂.match_1 {G : Type u_1} {H : Type u_2} (motive : G × HProp) :
                                            (x : G × H) → ((x : G) → (y : H) → motive (x, y)) → motive x
                                            Equations
                                            Instances For
                                              theorem continuous_of_continuousAt_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 => ↑(f x.fst) x.snd) (0, 0)) (hl : ∀ (x : G), ContinuousAt (↑(f x)) 0) (hr : ∀ (y : H), ContinuousAt (fun x => ↑(f x) y) 0) :
                                              Continuous fun x => ↑(f x.fst) x.snd
                                              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 => ↑(f x.fst) x.snd) (1, 1)) (hl : ∀ (x : G), ContinuousAt (↑(f x)) 1) (hr : ∀ (y : H), ContinuousAt (fun x => ↑(f x) y) 1) :
                                              Continuous fun x => ↑(f x.fst) x.snd
                                              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 => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => 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 => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) :
                                              theorem TopologicalAddGroup.of_nhds_zero' {G : Type u} [AddGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) (hright : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x + x₀) (nhds 0)) :
                                              theorem TopologicalGroup.of_nhds_one' {G : Type u} [Group G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) (hright : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x * x₀) (nhds 1)) :
                                              theorem TopologicalAddGroup.of_nhds_zero {G : Type u} [AddGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ + x + -x₀) (nhds 0) (nhds 0)) :
                                              theorem TopologicalGroup.of_nhds_one {G : Type u} [Group G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) (hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) :
                                              theorem TopologicalAddGroup.of_comm_of_nhds_zero {G : Type u} [AddCommGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hinv : Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) :
                                              theorem TopologicalGroup.of_comm_of_nhds_one {G : Type u} [CommGroup G] [TopologicalSpace G] (hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hinv : Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) :
                                              theorem QuotientAddGroup.nhds_eq {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) (x : G) :
                                              nhds x = Filter.map QuotientAddGroup.mk (nhds x)

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

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

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

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

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

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

                                              Equations

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

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

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

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

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

                                                Instances
                                                  theorem Filter.Tendsto.sub {α : Type u} {G : Type w} [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' {α : Type u} {G : Type w} [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 {α : Type u} {G : Type w} [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' {α : Type u} {G : Type w} [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.sub_const {α : Type u} {G : Type w} [TopologicalSpace G] [Sub G] [ContinuousSub G] {c : G} {f : αG} {l : Filter α} (h : Filter.Tendsto f l (nhds c)) (b : G) :
                                                  Filter.Tendsto (fun k => f k - b) l (nhds (c - b))
                                                  theorem Filter.Tendsto.div_const' {α : Type u} {G : Type w} [TopologicalSpace G] [Div G] [ContinuousDiv G] {c : G} {f : αG} {l : Filter α} (h : Filter.Tendsto f l (nhds c)) (b : G) :
                                                  Filter.Tendsto (fun k => f k / b) l (nhds (c / b))
                                                  theorem Continuous.sub {α : Type u} {G : Type w} [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' {α : Type u} {G : Type w} [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 b => a - b
                                                  theorem continuous_div_left' {G : Type w} [TopologicalSpace G] [Div G] [ContinuousDiv G] (a : G) :
                                                  Continuous fun b => a / b
                                                  theorem continuous_sub_right {G : Type w} [TopologicalSpace G] [Sub G] [ContinuousSub G] (a : G) :
                                                  Continuous fun b => b - a
                                                  theorem continuous_div_right' {G : Type w} [TopologicalSpace G] [Div G] [ContinuousDiv G] (a : G) :
                                                  Continuous fun b => b / a
                                                  theorem ContinuousAt.sub {α : Type u} {G : Type w} [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' {α : Type u} {G : Type w} [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 {α : Type u} {G : Type w} [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' {α : Type u} {G : Type w} [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 {α : Type u} {G : Type w} [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' {α : Type u} {G : Type w} [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

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

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem Homeomorph.divLeft_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) :
                                                    ↑(Homeomorph.divLeft x) b = x / b
                                                    @[simp]
                                                    theorem Homeomorph.subLeft_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) :
                                                    ↑(Homeomorph.subLeft x) b = x - b

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

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      theorem isOpenMap_sub_left {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) :
                                                      IsOpenMap ((fun x x_1 => x - x_1) a)
                                                      theorem isOpenMap_div_left {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) :
                                                      IsOpenMap ((fun x x_1 => x / x_1) a)
                                                      theorem isClosedMap_sub_left {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) :
                                                      IsClosedMap ((fun x x_1 => x - x_1) a)
                                                      theorem isClosedMap_div_left {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) :
                                                      IsClosedMap ((fun x x_1 => x / x_1) a)

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

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem Homeomorph.divRight_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) :
                                                        ↑(Homeomorph.divRight x) b = b / x
                                                        @[simp]
                                                        theorem Homeomorph.subRight_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) :
                                                        ↑(Homeomorph.subRight x) b = b - x
                                                        @[simp]

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

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem isOpenMap_sub_right {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) :
                                                          IsOpenMap fun x => x - a
                                                          theorem isOpenMap_div_right {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) :
                                                          IsOpenMap fun x => x / a
                                                          theorem isClosedMap_div_right {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) :
                                                          IsClosedMap fun x => 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 n => u n - 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 n => u n / 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 => x - x) (nhds 0) = nhds x
                                                          theorem nhds_translation_div {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) :
                                                          Filter.comap (fun x => x / x) (nhds 1) = nhds x

                                                          Topological operations on pointwise sums and products #

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

                                                          theorem IsOpen.vadd_left {α : Type u} {β : Type v} [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousConstVAdd α β] {s : Set α} {t : Set β} (ht : IsOpen t) :
                                                          IsOpen (s +ᵥ t)
                                                          theorem IsOpen.smul_left {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α} {t : Set β} (ht : IsOpen t) :
                                                          IsOpen (s t)
                                                          theorem subset_interior_vadd_right {α : Type u} {β : Type v} [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousConstVAdd α β] {s : Set α} {t : Set β} :
                                                          theorem subset_interior_smul_right {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α} {t : Set β} :
                                                          theorem vadd_mem_nhds {α : Type u} {β : Type v} [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousConstVAdd α β] {t : Set β} (a : α) {x : β} (ht : t nhds x) :
                                                          a +ᵥ t nhds (a +ᵥ x)
                                                          theorem smul_mem_nhds {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {t : Set β} (a : α) {x : β} (ht : t nhds x) :
                                                          a t nhds (a x)
                                                          theorem subset_interior_vadd {α : Type u} {β : Type v} [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousConstVAdd α β] {s : Set α} {t : Set β} [TopologicalSpace α] :
                                                          theorem subset_interior_smul {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α} {t : Set β} [TopologicalSpace α] :
                                                          abbrev IsClosed.vadd_left_of_isCompact.match_1 {α : Type u_2} {β : Type u_1} [AddGroup α] [AddAction α β] {s : Set α} {t : Set β} (x : β) (motive : x s +ᵥ tProp) :
                                                          (h : x s +ᵥ t) → ((g : α) → (y : β) → (hgs : g s) → (hyt : y t) → (hgyx : (fun x x_1 => x +ᵥ x_1) g y = x) → motive (_ : a b, a s b t (fun x x_1 => x +ᵥ x_1) a b = x)) → motive h
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            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 {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {s : Set α} {t : Set α} (ht : IsOpen t) :
                                                            IsOpen (s - t)
                                                            theorem IsOpen.div_left {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {s : Set α} {t : Set α} (ht : IsOpen t) :
                                                            IsOpen (s / t)
                                                            theorem IsOpen.sub_right {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {s : Set α} {t : Set α} (hs : IsOpen s) :
                                                            IsOpen (s - t)
                                                            theorem IsOpen.div_right {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {s : Set α} {t : Set α} (hs : IsOpen s) :
                                                            IsOpen (s / t)
                                                            theorem subset_interior_sub_left {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {s : Set α} {t : Set α} :
                                                            interior s - t interior (s - t)
                                                            theorem subset_interior_div_left {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {s : Set α} {t : Set α} :
                                                            interior s / t interior (s / t)
                                                            theorem subset_interior_sub_right {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {s : Set α} {t : Set α} :
                                                            s - interior t interior (s - t)
                                                            theorem subset_interior_div_right {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {s : Set α} {t : Set α} :
                                                            s / interior t interior (s / t)
                                                            theorem subset_interior_sub {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {s : Set α} {t : Set α} :
                                                            theorem subset_interior_div {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {s : Set α} {t : Set α} :
                                                            theorem IsOpen.add_closure {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {s : Set α} (hs : IsOpen s) (t : Set α) :
                                                            s + closure t = s + t
                                                            theorem IsOpen.mul_closure {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {s : Set α} (hs : IsOpen s) (t : Set α) :
                                                            s * closure t = s * t
                                                            theorem IsOpen.closure_add {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {t : Set α} (ht : IsOpen t) (s : Set α) :
                                                            closure s + t = s + t
                                                            theorem IsOpen.closure_mul {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {t : Set α} (ht : IsOpen t) (s : Set α) :
                                                            closure s * t = s * t
                                                            theorem IsOpen.sub_closure {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {s : Set α} (hs : IsOpen s) (t : Set α) :
                                                            s - closure t = s - t
                                                            theorem IsOpen.div_closure {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {s : Set α} (hs : IsOpen s) (t : Set α) :
                                                            s / closure t = s / t
                                                            theorem IsOpen.closure_sub {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {t : Set α} (ht : IsOpen t) (s : Set α) :
                                                            closure s - t = s - t
                                                            theorem IsOpen.closure_div {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {t : Set α} (ht : IsOpen t) (s : Set α) :
                                                            closure s / t = s / t
                                                            theorem IsClosed.add_left_of_isCompact {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {s : Set α} {t : Set α} (ht : IsClosed t) (hs : IsCompact s) :
                                                            IsClosed (s + t)
                                                            theorem IsClosed.mul_left_of_isCompact {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {s : Set α} {t : Set α} (ht : IsClosed t) (hs : IsCompact s) :
                                                            IsClosed (s * t)
                                                            theorem IsClosed.add_right_of_isCompact {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {s : Set α} {t : Set α} (ht : IsClosed t) (hs : IsCompact s) :
                                                            IsClosed (t + s)
                                                            theorem IsClosed.mul_right_of_isCompact {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {s : Set α} {t : Set α} (ht : IsClosed t) (hs : IsCompact s) :
                                                            IsClosed (t * s)
                                                            theorem QuotientAddGroup.isClosedMap_coe {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] {H : AddSubgroup α} (hH : IsCompact H) :
                                                            IsClosedMap QuotientAddGroup.mk
                                                            theorem QuotientGroup.isClosedMap_coe {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {H : Subgroup α} (hH : IsCompact H) :
                                                            IsClosedMap QuotientGroup.mk
                                                            theorem TopologicalAddGroup.t2Space_of_zero_sep {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (H : ∀ (x : G), x 0U, U nhds 0 ¬x U) :
                                                            theorem TopologicalGroup.t2Space_of_one_sep {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (H : ∀ (x : G), x 1U, U nhds 1 ¬x U) :

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                                            Equations

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

                                                            Equations
                                                            theorem exists_disjoint_vadd_of_isCompact {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [NoncompactSpace G] {K : Set G} {L : Set G} (hK : IsCompact K) (hL : IsCompact L) :
                                                            g, 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, 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.

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

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

                                                            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.

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

                                                            abbrev exists_isCompact_isClosed_nhds_zero.match_2 (G : Type u_1) [TopologicalSpace G] [AddGroup G] (motive : (s, IsCompact s s nhds 0) → Prop) :
                                                            (x : s, IsCompact s s nhds 0) → ((_L : Set G) → (Lcomp : IsCompact _L) → (L1 : _L nhds 0) → motive (_ : s, IsCompact s s nhds 0)) → motive x
                                                            Equations
                                                            Instances For
                                                              abbrev exists_isCompact_isClosed_nhds_zero.match_1 (G : Type u_1) [TopologicalSpace G] [AddGroup G] (_L : Set G) (motive : (K, IsCompact K IsClosed K K _L K nhds 0) → Prop) :
                                                              (x : K, IsCompact K IsClosed K K _L K nhds 0) → ((K : Set G) → (Kcl : IsCompact K) → (Kcomp : IsClosed K) → (left : K _L) → (K1 : K nhds 0) → motive (_ : K, IsCompact K IsClosed K K _L K nhds 0)) → motive x
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                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' := (_ : ∀ (x x_1 : G), nhds (x + x_1) = nhds x + nhds x_1) }
                                                                Instances For
                                                                  @[simp]
                                                                  theorem nhdsAddHom_apply {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (a : G) :
                                                                  nhdsAddHom a = nhds a
                                                                  @[simp]
                                                                  theorem nhdsMulHom_apply {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (a : G) :
                                                                  nhdsMulHom a = nhds a

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

                                                                  Equations
                                                                  • nhdsMulHom = { toFun := nhds, map_mul' := (_ : ∀ (x x_1 : G), nhds (x * x_1) = nhds x * nhds x_1) }
                                                                  Instances For
                                                                    theorem QuotientGroup.continuous_smul₁ {G : Type w} [Group G] [TopologicalSpace G] [ContinuousMul G] {Γ : Subgroup G} (x : G Γ) :
                                                                    Continuous fun g => g x
                                                                    theorem toAddUnits_homeomorph.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousNeg G] :
                                                                    Continuous toAddUnits.toEquiv.toFun

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

                                                                    Equations
                                                                    Instances For

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

                                                                      Equations
                                                                      Instances For
                                                                        theorem AddUnits.Homeomorph.sumAddUnits.proof_2 {α : Type u_1} {β : Type u_2} [AddMonoid α] [TopologicalSpace α] [AddMonoid β] [TopologicalSpace β] :
                                                                        Continuous AddEquiv.prodAddUnits.toEquiv.invFun

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

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

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

                                                                          Equations
                                                                          Instances For
                                                                            theorem topologicalGroup_sInf {G : Type w} [Group G] {ts : Set (TopologicalSpace G)} (h : ∀ (t : TopologicalSpace G), t tsTopologicalGroup 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.fst + p.snd

                                                                                    A version of the global continuous_add suitable for dot notation.

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

                                                                                    A version of the global continuous_mul suitable for dot notation.

                                                                                    A version of the global continuous_neg suitable for dot notation.

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

                                                                                    A version of the global continuous_inv suitable for dot notation.

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

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

                                                                                    Equations

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

                                                                                    Infimum of a collection of additive group topologies

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

                                                                                    Infimum of a collection of group topologies.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    @[simp]
                                                                                    theorem AddGroupTopology.toTopologicalSpace_sInf {α : Type u} [AddGroup α] (s : Set (AddGroupTopology α)) :
                                                                                    (sInf s).toTopologicalSpace = sInf (AddGroupTopology.toTopologicalSpace '' s)
                                                                                    @[simp]
                                                                                    theorem GroupTopology.toTopologicalSpace_sInf {α : Type u} [Group α] (s : Set (GroupTopology α)) :
                                                                                    (sInf s).toTopologicalSpace = sInf (GroupTopology.toTopologicalSpace '' s)
                                                                                    @[simp]
                                                                                    theorem AddGroupTopology.toTopologicalSpace_iInf {α : Type u} [AddGroup α] {ι : Sort u_1} (s : ιAddGroupTopology α) :
                                                                                    (⨅ (i : ι), s i).toTopologicalSpace = ⨅ (i : ι), (s i).toTopologicalSpace
                                                                                    @[simp]
                                                                                    theorem GroupTopology.toTopologicalSpace_iInf {α : Type u} [Group α] {ι : Sort u_1} (s : ιGroupTopology α) :
                                                                                    (⨅ (i : ι), s i).toTopologicalSpace = ⨅ (i : ι), (s i).toTopologicalSpace
                                                                                    theorem AddGroupTopology.instCompleteSemilatticeInfAddGroupTopology.proof_3 {α : Type u_1} [AddGroup α] (S : Set (AddGroupTopology α)) (a : AddGroupTopology α) (hab : ∀ (b : AddGroupTopology α), b Sa b) :
                                                                                    a.toTopologicalSpace sInf (AddGroupTopology.toTopologicalSpace '' S)

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

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

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

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

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

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

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

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

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

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

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

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