Documentation

Mathlib.Topology.Algebra.Group.Basic

Topological groups #

This file defines the following typeclasses:

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

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

Tags #

topological space, group, topological group

Groups with continuous multiplication #

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

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

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

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

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

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

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

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

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

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

          ContinuousInv and ContinuousNeg #

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

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

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

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

            Instances
              theorem Specializes.neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x : G} {y : G} (h : x y) :
              (-x) (-y)
              theorem Specializes.inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x : G} {y : G} (h : x y) :
              theorem Inseparable.neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x : G} {y : G} (h : Inseparable x y) :
              theorem Inseparable.inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x : G} {y : G} (h : Inseparable x y) :
              theorem Specializes.zsmul {G : Type u_1} [SubNegMonoid G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousNeg G] {x : G} {y : G} (h : x y) (m : ) :
              (m x) (m y)
              abbrev Specializes.zsmul.match_1 (motive : Prop) :
              ∀ (x : ), (∀ (n : ), motive (Int.ofNat n))(∀ (n : ), motive (Int.negSucc n))motive x
              Equations
              • =
              Instances For
                theorem Specializes.zpow {G : Type u_1} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x : G} {y : G} (h : x y) (m : ) :
                (x ^ m) (y ^ m)
                theorem Inseparable.zsmul {G : Type u_1} [SubNegMonoid G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousNeg G] {x : G} {y : G} (h : Inseparable x y) (m : ) :
                Inseparable (m x) (m y)
                theorem Inseparable.zpow {G : Type u_1} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x : G} {y : G} (h : Inseparable x y) (m : ) :
                Inseparable (x ^ m) (y ^ m)
                theorem continuousOn_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {s : Set G} :
                ContinuousOn Neg.neg s
                theorem continuousOn_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {s : Set G} :
                ContinuousOn Inv.inv s
                theorem continuousWithinAt_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {s : Set G} {x : G} :
                ContinuousWithinAt Neg.neg s x
                theorem continuousWithinAt_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {s : Set G} {x : G} :
                ContinuousWithinAt Inv.inv s x
                theorem continuousAt_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x : G} :
                ContinuousAt Neg.neg x
                theorem continuousAt_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x : G} :
                ContinuousAt Inv.inv x
                theorem tendsto_neg {G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] (a : G) :
                Filter.Tendsto Neg.neg (nhds a) (nhds (-a))
                theorem tendsto_inv {G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] (a : G) :
                Filter.Tendsto Inv.inv (nhds a) (nhds a⁻¹)
                theorem Filter.Tendsto.neg {G : Type w} {α : Type u} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {f : αG} {l : Filter α} {y : G} (h : Filter.Tendsto f l (nhds y)) :
                Filter.Tendsto (fun (x : α) => -f x) l (nhds (-y))

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

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

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

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

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

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

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

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

                Negation in a topological group as a homeomorphism.

                Equations
                Instances For

                  Inversion in a topological group as a homeomorphism.

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

                    Topological groups #

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

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

                      Instances

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                            Equations
                            • =

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

                            Equations
                            • =
                            theorem neg_mem_nhds_zero (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {S : Set G} (hS : S nhds 0) :
                            theorem inv_mem_nhds_one (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] {S : Set G} (hS : S nhds 1) :
                            theorem Homeomorph.shearAddRight.proof_2 (G : Type u_1) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] :
                            Continuous fun (x : G × G) => (x.1, (Equiv.addLeft ((Equiv.refl G).symm x.1)).symm x.2)

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

                            Equations
                            Instances For

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

                              Equations
                              Instances For
                                @[simp]
                                theorem Homeomorph.shearAddRight_coe (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] :
                                (Homeomorph.shearAddRight G) = fun (z : G × G) => (z.1, z.1 + z.2)
                                @[simp]
                                theorem Homeomorph.shearMulRight_coe (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] :
                                (Homeomorph.shearMulRight G) = fun (z : G × G) => (z.1, z.1 * z.2)
                                @[simp]
                                @[simp]
                                theorem Inducing.topologicalGroup {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] {F : Type u_1} [Group H] [TopologicalSpace H] [FunLike F H G] [MonoidHomClass F H G] (f : F) (hf : Inducing f) :
                                theorem topologicalGroup_induced {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] {F : Type u_1} [Group H] [FunLike F H G] [MonoidHomClass F H G] (f : F) :
                                theorem AddSubgroup.topologicalClosure.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) :
                                ∀ {a b : G}, a (AddSubmonoid.topologicalClosure s.toAddSubmonoid).carrierb (AddSubmonoid.topologicalClosure s.toAddSubmonoid).carriera + b (AddSubmonoid.topologicalClosure s.toAddSubmonoid).carrier

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

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

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

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

                                    The topological closure of a normal additive subgroup is normal.

                                    The topological closure of a normal subgroup is normal.

                                    The connected component of 0 is a subgroup of G.

                                    Equations
                                    Instances For

                                      The connected component of 1 is a subgroup of G.

                                      Equations
                                      Instances For

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                              Equations
                                              • =

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

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

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

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

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

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

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

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

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

                                                    Equations
                                                    Instances For
                                                      theorem isOpenMap_sub_left {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) :
                                                      IsOpenMap fun (x : G) => a - x
                                                      theorem isOpenMap_div_left {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) :
                                                      IsOpenMap fun (x : G) => a / x
                                                      theorem isClosedMap_sub_left {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) :
                                                      IsClosedMap fun (x : G) => a - x
                                                      theorem isClosedMap_div_left {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (a : G) :
                                                      IsClosedMap fun (x : G) => a / x
                                                      theorem Homeomorph.subRight.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) :
                                                      Continuous fun (x_1 : G) => id x_1 - x
                                                      theorem Homeomorph.subRight.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) :
                                                      Continuous fun (x_1 : G) => id x_1 + x

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

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

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

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

                                                          Topological operations on pointwise sums and products #

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

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

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

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