Topological groups

This file defines the following typeclasses:

• TopologicalGroup, TopologicalAddGroup: multiplicative and additive topological groups, i.e., groups with continuous (*) and (⁻¹) / (+) and (-);

• ContinuousSub G means that G has a continuous subtraction operation.

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

def Homeomorph.addLeft {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : G ≃ₜ G

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

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.

@[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 Homeomorph.addLeft_symm {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : Homeomorph.symm (Homeomorph.addLeft a) = Homeomorph.addLeft (-a)

theorem Homeomorph.mulLeft_symm {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : Homeomorph.symm (Homeomorph.mulLeft a) = Homeomorph.mulLeft 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) : IsOpen (leftAddCoset x U)

theorem IsOpen.leftCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsOpen U) (x : G) : IsOpen (leftCoset x U)

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) : IsClosed (leftAddCoset x U)

theorem IsClosed.leftCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsClosed U) (x : G) : IsClosed (leftCoset x U)

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

def Homeomorph.addRight {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : G ≃ₜ G

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

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.

@[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 Homeomorph.addRight_symm {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (a : G) : Homeomorph.symm (Homeomorph.addRight a) = Homeomorph.addRight (-a)

theorem Homeomorph.mulRight_symm {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (a : G) : Homeomorph.symm (Homeomorph.mulRight a) = Homeomorph.mulRight 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) : IsOpen (rightAddCoset U x)

theorem IsOpen.rightCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsOpen U) (x : G) : IsOpen (rightCoset U x)

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.right_addCoset {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {U : Set G} (h : IsClosed U) (x : G) : IsClosed (rightAddCoset U x)

theorem IsClosed.rightCoset {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] {U : Set G} (h : IsClosed U) (x : G) : IsClosed (rightCoset U x)

theorem discreteTopology_of_open_singleton_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (h : IsOpen {0}) : DiscreteTopology G

theorem discreteTopology_of_open_singleton_one {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (h : IsOpen {1}) : DiscreteTopology G

theorem discreteTopology_iff_open_singleton_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] : DiscreteTopology G ↔ IsOpen {0}

theorem discreteTopology_iff_open_singleton_one {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] : DiscreteTopology G ↔ IsOpen {1}

ContinuousInv and ContinuousNeg

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

• continuous_neg : Continuous fun a => -a

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.

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

• continuous_inv : Continuous fun a => a⁻¹

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.

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

instance Prod.continuousNeg {G : Type w} {H : Type x} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace H] [Neg H] [ContinuousNeg H] : ContinuousNeg (G × H)

theorem Prod.continuousNeg.proof_1 {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [Neg G] [ContinuousNeg G] [TopologicalSpace H] [Neg H] [ContinuousNeg H] : ContinuousNeg (G × H)

instance Prod.continuousInv {G : Type w} {H : Type x} [TopologicalSpace G] [Inv G] [ContinuousInv G] [TopologicalSpace H] [Inv H] [ContinuousInv H] : ContinuousInv (G × H)

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)

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)

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.

theorem Pi.has_continuous_neg'.proof_1 {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {ι : Type u_2} : ContinuousNeg (ι → G)

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.

instance continuousNeg_of_discreteTopology {H : Type x} [TopologicalSpace H] [Neg H] [DiscreteTopology H] : ContinuousNeg H

theorem continuousNeg_of_discreteTopology.proof_1 {H : Type u_1} [TopologicalSpace H] [Neg H] [DiscreteTopology H] : ContinuousNeg H

instance continuousInv_of_discreteTopology {H : Type x} [TopologicalSpace H] [Inv H] [DiscreteTopology H] : ContinuousInv H

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)⁻¹}

instance instContinuousNegAdditiveInstTopologicalSpaceAdditiveNeg {H : Type x} [TopologicalSpace H] [Inv H] [ContinuousInv H] : ContinuousNeg (Additive H)

instance instContinuousInvMultiplicativeInstTopologicalSpaceMultiplicativeInv {H : Type x} [TopologicalSpace H] [Neg H] [ContinuousNeg H] : ContinuousInv (Multiplicative H)

theorem IsCompact.neg {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsCompact s) : IsCompact (-s)

theorem IsCompact.inv {G : Type w} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsCompact s) : IsCompact s⁻¹

def Homeomorph.neg (G : Type u_1) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] : G ≃ₜ G

Negation in a topological group as a homeomorphism.

theorem Homeomorph.neg.proof_1 (G : Type u_1) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] : Continuous fun a => -a

def Homeomorph.inv (G : Type u_1) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : G ≃ₜ G

Inversion in a topological group as a homeomorphism.

theorem isOpenMap_neg (G : Type w) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] : IsOpenMap Neg.neg

theorem isOpenMap_inv (G : Type w) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : IsOpenMap Inv.inv

theorem isClosedMap_neg (G : Type w) [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] : IsClosedMap Neg.neg

theorem isClosedMap_inv (G : Type w) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : IsClosedMap Inv.inv

theorem IsOpen.neg {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsOpen s) : IsOpen (-s)

theorem IsOpen.inv {G : Type w} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsOpen s) : IsOpen s⁻¹

theorem IsClosed.neg {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {s : Set G} (hs : IsClosed s) : IsClosed (-s)

theorem IsClosed.inv {G : Type w} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsClosed s) : IsClosed s⁻¹

theorem neg_closure {G : Type w} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] (s : Set G) : -closure s = closure (-s)

theorem inv_closure {G : Type w} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] (s : Set G) : (closure s)⁻¹ = closure s⁻¹

theorem continuousNeg_sInf {G : Type w} [Neg G] {ts : Set (TopologicalSpace G)} (h : ∀ (t : TopologicalSpace G), t ∈ ts → ContinuousNeg G) : ContinuousNeg G

theorem continuousInv_sInf {G : Type w} [Inv G] {ts : Set (TopologicalSpace G)} (h : ∀ (t : TopologicalSpace G), t ∈ ts → ContinuousInv G) : ContinuousInv G

theorem continuousNeg_iInf {G : Type w} {ι' : Sort u_1} [Neg G] {ts' : ι' → TopologicalSpace G} (h' : ∀ (i : ι'), ContinuousNeg G) : ContinuousNeg G

theorem continuousInv_iInf {G : Type w} {ι' : Sort u_1} [Inv G] {ts' : ι' → TopologicalSpace G} (h' : ∀ (i : ι'), ContinuousInv G) : ContinuousInv G

theorem continuousNeg_inf {G : Type w} [Neg G] {t₁ : TopologicalSpace G} {t₂ : TopologicalSpace G} (h₁ : ContinuousNeg G) (h₂ : ContinuousNeg G) : ContinuousNeg G

theorem continuousInv_inf {G : Type w} [Inv G] {t₁ : TopologicalSpace G} {t₂ : TopologicalSpace G} (h₁ : ContinuousInv G) (h₂ : ContinuousInv G) : ContinuousInv G

theorem Inducing.continuousNeg {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousNeg H] {f : G → H} (hf : Inducing f) (hf_inv : ∀ (x : G), f (-x) = -f x) : ContinuousNeg G

theorem Inducing.continuousInv {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousInv H] {f : G → H} (hf : Inducing f) (hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹) : ContinuousInv G

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.

class TopologicalAddGroup (G : Type u) [TopologicalSpace G] [AddGroup G] extends ContinuousAdd , ContinuousNeg : Prop

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

class TopologicalGroup (G : Type u_1) [TopologicalSpace G] [Group G] extends ContinuousMul , ContinuousInv : Prop

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.

instance ConjAct.units_continuousConstSMul {M : Type u_1} [Monoid M] [TopologicalSpace M] [ContinuousMul M] : ContinuousConstSMul (ConjAct Mˣ) M

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.

theorem continuous_zsmul {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (z : ℤ) : Continuous fun a => z • a

abbrev continuous_zsmul.match_1 (motive : ℤ → Prop) : (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x

theorem continuous_zpow {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (z : ℤ) : Continuous fun a => a ^ z

instance AddGroup.continuousConstSMul_int {A : Type u_1} [AddGroup A] [TopologicalSpace A] [TopologicalAddGroup A] : ContinuousConstSMul ℤ A

instance AddGroup.continuousSMul_int {A : Type u_1} [AddGroup A] [TopologicalSpace A] [TopologicalAddGroup A] : ContinuousSMul ℤ A

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 tendsto_neg_nhdsWithin_Ioi {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Ioi a)) (nhdsWithin (-a) (Set.Iio (-a)))

theorem tendsto_inv_nhdsWithin_Ioi {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Ioi a)) (nhdsWithin a⁻¹ (Set.Iio a⁻¹))

theorem tendsto_neg_nhdsWithin_Iio {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Iio a)) (nhdsWithin (-a) (Set.Ioi (-a)))

theorem tendsto_inv_nhdsWithin_Iio {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Iio a)) (nhdsWithin a⁻¹ (Set.Ioi a⁻¹))

theorem tendsto_neg_nhdsWithin_Ioi_neg {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Ioi (-a))) (nhdsWithin a (Set.Iio a))

theorem tendsto_inv_nhdsWithin_Ioi_inv {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Ioi a⁻¹)) (nhdsWithin a (Set.Iio a))

theorem tendsto_neg_nhdsWithin_Iio_neg {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Iio (-a))) (nhdsWithin a (Set.Ioi a))

theorem tendsto_inv_nhdsWithin_Iio_inv {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Iio a⁻¹)) (nhdsWithin a (Set.Ioi a))

theorem tendsto_neg_nhdsWithin_Ici {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Ici a)) (nhdsWithin (-a) (Set.Iic (-a)))

theorem tendsto_inv_nhdsWithin_Ici {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Ici a)) (nhdsWithin a⁻¹ (Set.Iic a⁻¹))

theorem tendsto_neg_nhdsWithin_Iic {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Iic a)) (nhdsWithin (-a) (Set.Ici (-a)))

theorem tendsto_inv_nhdsWithin_Iic {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Iic a)) (nhdsWithin a⁻¹ (Set.Ici a⁻¹))

theorem tendsto_neg_nhdsWithin_Ici_neg {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Ici (-a))) (nhdsWithin a (Set.Iic a))

theorem tendsto_inv_nhdsWithin_Ici_inv {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Ici a⁻¹)) (nhdsWithin a (Set.Iic a))

theorem tendsto_neg_nhdsWithin_Iic_neg {H : Type x} [TopologicalSpace H] [OrderedAddCommGroup H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Iic (-a))) (nhdsWithin a (Set.Ici a))

theorem tendsto_inv_nhdsWithin_Iic_inv {H : Type x} [TopologicalSpace H] [OrderedCommGroup H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Iic a⁻¹)) (nhdsWithin a (Set.Ici a))

theorem instTopologicalAddGroupSumInstTopologicalSpaceSumInstAddGroup.proof_1 {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace H] [AddGroup H] [TopologicalAddGroup H] : TopologicalAddGroup (G × H)

instance instTopologicalAddGroupSumInstTopologicalSpaceSumInstAddGroup {G : Type w} {H : Type x} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace H] [AddGroup H] [TopologicalAddGroup H] : TopologicalAddGroup (G × H)

instance instTopologicalGroupProdInstTopologicalSpaceProdInstGroup {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace H] [Group H] [TopologicalGroup H] : TopologicalGroup (G × H)

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)

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)

theorem instContinuousNegAddOppositeInstTopologicalSpaceAddOppositeNeg.proof_1 {α : Type u_1} [TopologicalSpace α] [Neg α] [ContinuousNeg α] : ContinuousNeg αᵃᵒᵖ

instance instContinuousNegAddOppositeInstTopologicalSpaceAddOppositeNeg {α : Type u} [TopologicalSpace α] [Neg α] [ContinuousNeg α] : ContinuousNeg αᵃᵒᵖ

instance instContinuousInvMulOppositeInstTopologicalSpaceMulOppositeInv {α : Type u} [TopologicalSpace α] [Inv α] [ContinuousInv α] : ContinuousInv αᵐᵒᵖ

theorem instTopologicalAddGroupAddOppositeInstTopologicalSpaceAddOppositeAddGroup.proof_1 {α : Type u_1} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] : TopologicalAddGroup αᵃᵒᵖ

instance instTopologicalAddGroupAddOppositeInstTopologicalSpaceAddOppositeAddGroup {α : Type u} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] : TopologicalAddGroup αᵃᵒᵖ

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

instance instTopologicalGroupMulOppositeInstTopologicalSpaceMulOppositeGroup {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] : TopologicalGroup αᵐᵒᵖ

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

theorem nhds_zero_symm (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : Filter.comap Neg.neg (nhds 0) = nhds 0

theorem nhds_one_symm (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : Filter.comap Inv.inv (nhds 1) = nhds 1

theorem nhds_zero_symm' (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : Filter.map Neg.neg (nhds 0) = nhds 0

theorem nhds_one_symm' (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : Filter.map Inv.inv (nhds 1) = nhds 1

theorem neg_mem_nhds_zero (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {S : Set G} (hS : S ∈ nhds 0) : -S ∈ nhds 0

theorem inv_mem_nhds_one (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] {S : Set G} (hS : S ∈ nhds 1) : 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

def Homeomorph.shearAddRight (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : G × G ≃ₜ G × G

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

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

def Homeomorph.shearMulRight (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : G × G ≃ₜ G × G

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

@[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 Homeomorph.shearAddRight_symm_coe (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : ↑(Homeomorph.symm (Homeomorph.shearAddRight G)) = fun z => (z.fst, -z.fst + z.snd)

@[simp]

theorem Homeomorph.shearMulRight_symm_coe (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : ↑(Homeomorph.symm (Homeomorph.shearMulRight G)) = fun z => (z.fst, z.fst⁻¹ * z.snd)

theorem Inducing.topologicalAddGroup {G : Type w} {H : Type x} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {F : Type u_1} [AddGroup H] [TopologicalSpace H] [AddMonoidHomClass F H G] (f : F) (hf : Inducing ↑f) : TopologicalAddGroup H

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) : TopologicalGroup H

theorem topologicalAddGroup_induced {G : Type w} {H : Type x} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {F : Type u_1} [AddGroup H] [AddMonoidHomClass F H G] (f : F) : TopologicalAddGroup H

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) : TopologicalGroup H

theorem AddSubgroup.instTopologicalAddGroupSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupInstTopologicalSpaceSubtypeToAddGroup.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (S : AddSubgroup G) : TopologicalAddGroup { x // x ∈ S }

instance AddSubgroup.instTopologicalAddGroupSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupInstTopologicalSpaceSubtypeToAddGroup {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (S : AddSubgroup G) : TopologicalAddGroup { x // x ∈ S }

instance Subgroup.instTopologicalGroupSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupInstTopologicalSpaceSubtypeToGroup {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (S : Subgroup G) : TopologicalGroup { x // x ∈ S }

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.carrier → b ∈ (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrier → a + b ∈ (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrier

def AddSubgroup.topologicalClosure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) : AddSubgroup G

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

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.carrier → b ∈ (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrier → a + 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.carrier → b ∈ (AddSubmonoid.topologicalClosure s.toAddSubmonoid).toAddSubsemigroup.carrier → a + 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

def Subgroup.topologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (s : Subgroup G) : Subgroup G

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

@[simp]

theorem AddSubgroup.topologicalClosure_coe {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {s : AddSubgroup G} : ↑(AddSubgroup.topologicalClosure s) = closure ↑s

@[simp]

theorem Subgroup.topologicalClosure_coe {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {s : Subgroup G} : ↑(Subgroup.topologicalClosure s) = closure ↑s

theorem AddSubgroup.le_topologicalClosure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) : s ≤ AddSubgroup.topologicalClosure s

theorem Subgroup.le_topologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (s : Subgroup G) : s ≤ Subgroup.topologicalClosure s

theorem AddSubgroup.isClosed_topologicalClosure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) : IsClosed ↑(AddSubgroup.topologicalClosure s)

theorem Subgroup.isClosed_topologicalClosure {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (s : Subgroup G) : IsClosed ↑(Subgroup.topologicalClosure s)

theorem AddSubgroup.topologicalClosure_minimal {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) {t : AddSubgroup G} (h : s ≤ t) (ht : IsClosed ↑t) : AddSubgroup.topologicalClosure s ≤ t

theorem Subgroup.topologicalClosure_minimal {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (s : Subgroup G) {t : Subgroup G} (h : s ≤ t) (ht : IsClosed ↑t) : Subgroup.topologicalClosure s ≤ t

theorem DenseRange.topologicalClosure_map_addSubgroup {G : Type w} {H : Type x} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [AddGroup H] [TopologicalSpace H] [TopologicalAddGroup H] {f : G →+ H} (hf : Continuous ↑f) (hf' : DenseRange ↑f) {s : AddSubgroup G} (hs : AddSubgroup.topologicalClosure s = ⊤) : AddSubgroup.topologicalClosure (AddSubgroup.map f s) = ⊤

theorem DenseRange.topologicalClosure_map_subgroup {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [TopologicalGroup G] [Group H] [TopologicalSpace H] [TopologicalGroup H] {f : G →* H} (hf : Continuous ↑f) (hf' : DenseRange ↑f) {s : Subgroup G} (hs : Subgroup.topologicalClosure s = ⊤) : Subgroup.topologicalClosure (Subgroup.map f s) = ⊤

theorem AddSubgroup.is_normal_topologicalClosure {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) [AddSubgroup.Normal N] : AddSubgroup.Normal (AddSubgroup.topologicalClosure N)

The topological closure of a normal additive subgroup is normal.

theorem Subgroup.is_normal_topologicalClosure {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] (N : Subgroup G) [Subgroup.Normal N] : Subgroup.Normal (Subgroup.topologicalClosure N)

The topological closure of a normal subgroup is normal.

theorem add_mem_connectedComponent_zero {G : Type u_1} [TopologicalSpace G] [AddZeroClass G] [ContinuousAdd G] {g : G} {h : G} (hg : g ∈ connectedComponent 0) (hh : h ∈ connectedComponent 0) : g + h ∈ connectedComponent 0

theorem mul_mem_connectedComponent_one {G : Type u_1} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {g : G} {h : G} (hg : g ∈ connectedComponent 1) (hh : h ∈ connectedComponent 1) : g * h ∈ connectedComponent 1

theorem neg_mem_connectedComponent_zero {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {g : G} (hg : g ∈ connectedComponent 0) : -g ∈ connectedComponent 0

theorem inv_mem_connectedComponent_one {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] {g : G} (hg : g ∈ connectedComponent 1) : g⁻¹ ∈ connectedComponent 1

theorem AddSubgroup.connectedComponentOfZero.proof_1 (G : Type u_1) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : ∀ {a b : G}, a ∈ connectedComponent 0 → b ∈ connectedComponent 0 → a + b ∈ connectedComponent 0

def AddSubgroup.connectedComponentOfZero (G : Type u_1) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : AddSubgroup G

The connected component of 0 is a subgroup of G.

theorem AddSubgroup.connectedComponentOfZero.proof_2 (G : Type u_1) [TopologicalSpace G] [AddGroup G] : 0 ∈ connectedComponent 0

def Subgroup.connectedComponentOfOne (G : Type u_1) [TopologicalSpace G] [Group G] [TopologicalGroup G] : Subgroup G

The connected component of 1 is a subgroup of G.

def AddSubgroup.addCommGroupTopologicalClosure {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [T2Space G] (s : AddSubgroup G) (hs : ∀ (x y : { x // x ∈ s }), x + y = y + x) : AddCommGroup { x // x ∈ AddSubgroup.topologicalClosure s }

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

theorem AddSubgroup.addCommGroupTopologicalClosure.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (s : AddSubgroup G) (a : { x // x ∈ AddSubgroup.topologicalClosure s }) : -a + a = 0

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) : CommGroup { x // x ∈ Subgroup.topologicalClosure s }

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

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 ∈ V → 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, V ∈ nhds 1 ∧ ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v / 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 0 → ∃ y, 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 1 → ∃ y, 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) : Continuous ↑f

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) : Continuous ↑f

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 × H → Prop) : (x : G × H) → ((x : G) → (y : H) → motive (x, y)) → motive x

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 TopologicalAddGroup.ext_iff {G : Type u_1} [AddGroup G] {t : TopologicalSpace G} {t' : TopologicalSpace G} (tg : TopologicalAddGroup G) (tg' : TopologicalAddGroup G) : t = t' ↔ nhds 0 = nhds 0

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)) : ContinuousNeg G

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)) : ContinuousInv G

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)) : TopologicalAddGroup G

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)) : TopologicalGroup G

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)) : TopologicalAddGroup G

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)) : TopologicalGroup G

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)) : TopologicalAddGroup G

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)) : TopologicalGroup G

instance QuotientAddGroup.Quotient.topologicalSpace {G : Type u_1} [AddGroup G] [TopologicalSpace G] (N : AddSubgroup G) : TopologicalSpace (G ⧸ N)

instance QuotientGroup.Quotient.topologicalSpace {G : Type u_1} [Group G] [TopologicalSpace G] (N : Subgroup G) : TopologicalSpace (G ⧸ N)

theorem QuotientAddGroup.isOpenMap_coe {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) : IsOpenMap QuotientAddGroup.mk

theorem QuotientGroup.isOpenMap_coe {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (N : Subgroup G) : IsOpenMap QuotientGroup.mk

instance topologicalAddGroup_quotient {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) [AddSubgroup.Normal N] : TopologicalAddGroup (G ⧸ N)

theorem topologicalAddGroup_quotient.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) [AddSubgroup.Normal N] : TopologicalAddGroup (G ⧸ N)

instance topologicalGroup_quotient {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (N : Subgroup G) [Subgroup.Normal N] : TopologicalGroup (G ⧸ N)

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.

theorem TopologicalAddGroup.exists_antitone_basis_nhds_zero (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace.FirstCountableTopology G] : ∃ u, Filter.HasAntitoneBasis (nhds 0) u ∧ ∀ (n : ℕ), u (n + 1) + u (n + 1) ⊆ u n

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

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

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

theorem QuotientAddGroup.nhds_zero_isCountablyGenerated.proof_1 (G : Type u_1) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) (n : AddSubgroup.Normal N) [TopologicalSpace.FirstCountableTopology G] : Filter.IsCountablyGenerated (nhds ↑0)

instance QuotientAddGroup.nhds_zero_isCountablyGenerated (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) (n : AddSubgroup.Normal N) [TopologicalSpace.FirstCountableTopology G] : Filter.IsCountablyGenerated (nhds 0)

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

instance QuotientGroup.nhds_one_isCountablyGenerated (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] (N : Subgroup G) (n : Subgroup.Normal N) [TopologicalSpace.FirstCountableTopology G] : Filter.IsCountablyGenerated (nhds 1)

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

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

• continuous_sub : Continuous fun p => p.fst - p.snd

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.

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

• continuous_div' : Continuous fun p => p.fst / p.snd

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.

theorem TopologicalAddGroup.to_continuousSub.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : ContinuousSub G

instance TopologicalAddGroup.to_continuousSub {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : ContinuousSub G

instance TopologicalGroup.to_continuousDiv {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] : ContinuousDiv G

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

theorem Homeomorph.subLeft.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : Continuous fun x => x - x

theorem Homeomorph.subLeft.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : Continuous fun x => -x + x

def Homeomorph.subLeft {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : G ≃ₜ G

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

@[simp]

theorem Homeomorph.divLeft_symm_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) : ↑(Homeomorph.symm (Homeomorph.divLeft x)) b = b⁻¹ * x

@[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_symm_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) : ↑(Homeomorph.symm (Homeomorph.subLeft x)) b = -b + x

@[simp]

theorem Homeomorph.subLeft_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) : ↑(Homeomorph.subLeft x) b = x - b

def Homeomorph.divLeft {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) : G ≃ₜ G

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

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)

theorem Homeomorph.subRight.proof_2 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : Continuous fun x => id x + x

def Homeomorph.subRight {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : G ≃ₜ G

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

theorem Homeomorph.subRight.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) : Continuous fun x => id x - x

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

theorem Homeomorph.divRight_symm_apply {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) (b : G) : ↑(Homeomorph.symm (Homeomorph.divRight x)) b = b * x

@[simp]

theorem Homeomorph.subRight_symm_apply {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (x : G) (b : G) : ↑(Homeomorph.symm (Homeomorph.subRight x)) b = b + x

def Homeomorph.divRight {G : Type w} [Group G] [TopologicalSpace G] [TopologicalGroup G] (x : G) : G ≃ₜ G

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

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_sub_right {G : Type w} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (a : G) : IsClosedMap 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 β} : s +ᵥ interior t ⊆ interior (s +ᵥ t)

theorem subset_interior_smul_right {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α} {t : Set β} : s • interior t ⊆ interior (s • t)

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 α] : interior s +ᵥ interior t ⊆ interior (s +ᵥ t)

theorem subset_interior_smul {α : Type u} {β : Type v} [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α} {t : Set β} [TopologicalSpace α] : interior s • interior t ⊆ interior (s • t)

abbrev IsClosed.vadd_left_of_isCompact.match_1 {α : Type u_2} {β : Type u_1} [AddGroup α] [AddAction α β] {s : Set α} {t : Set β} (x : β) (motive : x ∈ s +ᵥ t → Prop) : (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

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) : IsClosed (s +ᵥ t)

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) : IsClosed (s • t)

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:

• for any x ∈ t, s • {x} is closed
• for any x ∈ t, there is a continuous function g : s • {x} → s such that, for all y ∈ s • {x}, we have y = (g y) • x These are fairly specific hypotheses so we don't state this version of the lemmas, but an interesting fact is that these two assumptions are verified in the case of a NormedAddTorsor (or really, any AddTorsor with continuous -ᵥ). We prove this special case in IsClosed.vadd_right_of_isCompact.

theorem AddAction.isClosedMap_quotient {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [AddGroup α] [AddAction α β] [ContinuousNeg α] [ContinuousVAdd α β] [CompactSpace α] : IsClosedMap Quotient.mk'

theorem MulAction.isClosedMap_quotient {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousInv α] [ContinuousSMul α β] [CompactSpace α] : IsClosedMap Quotient.mk'

theorem IsOpen.add_left {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd α α] {s : Set α} {t : Set α} : IsOpen t → IsOpen (s + t)

theorem IsOpen.mul_left {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} {t : Set α} : IsOpen t → IsOpen (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 α} : interior s + interior t ⊆ interior (s + t)

theorem subset_interior_mul {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul α α] {s : Set α} {t : Set α} : interior s * interior t ⊆ interior (s * t)

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_add_left {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} {t : Set α} : interior s + t ⊆ interior (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_add' {α : Type u} [TopologicalSpace α] [AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} {t : Set α} : interior s + interior t ⊆ interior (s + t)

theorem subset_interior_mul' {α : Type u} [TopologicalSpace α] [Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} {t : Set α} : interior s * interior t ⊆ interior (s * t)

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 α} : interior s - interior t ⊆ interior (s - t)

theorem subset_interior_div {α : Type u} [TopologicalSpace α] [Group α] [TopologicalGroup α] {s : Set α} {t : Set α} : interior s / interior t ⊆ interior (s / t)

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.t1Space (G : Type w) [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (h : IsClosed {0}) : T1Space G

theorem TopologicalGroup.t1Space (G : Type w) [TopologicalSpace G] [Group G] [ContinuousMul G] (h : IsClosed {1}) : T1Space G

instance TopologicalAddGroup.regularSpace (G : Type w) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : RegularSpace G

theorem TopologicalAddGroup.regularSpace.proof_1 (G : Type u_1) [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : RegularSpace G

instance TopologicalGroup.regularSpace (G : Type w) [TopologicalSpace G] [Group G] [TopologicalGroup G] : RegularSpace G

theorem TopologicalAddGroup.t2Space_iff_zero_closed {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : T2Space G ↔ IsClosed {0}

theorem TopologicalGroup.t2Space_iff_one_closed {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] : T2Space G ↔ IsClosed {1}

theorem TopologicalAddGroup.t2Space_of_zero_sep {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (H : ∀ (x : G), x ≠ 0 → ∃ U, U ∈ nhds 0 ∧ ¬x ∈ U) : T2Space G

theorem TopologicalGroup.t2Space_of_one_sep {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ nhds 1 ∧ ¬x ∈ U) : T2Space G

instance AddSubgroup.t3_quotient_of_isClosed {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (S : AddSubgroup G) [AddSubgroup.Normal S] [hS : IsClosed ↑S] : T3Space (G ⧸ S)

theorem AddSubgroup.t3_quotient_of_isClosed.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (S : AddSubgroup G) [AddSubgroup.Normal S] [hS : IsClosed ↑S] : T3Space (G ⧸ S)

instance Subgroup.t3_quotient_of_isClosed {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (S : Subgroup G) [Subgroup.Normal S] [hS : IsClosed ↑S] : T3Space (G ⧸ S)

theorem AddSubgroup.properlyDiscontinuousVAdd_of_tendsto_cofinite {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (S : AddSubgroup G) (hS : Filter.Tendsto (↑(AddSubgroup.subtype S)) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousVAdd { x // x ∈ S } G

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.

theorem Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (S : Subgroup G) (hS : Filter.Tendsto (↑(Subgroup.subtype S)) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousSMul { x // x ∈ S } G

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.)

theorem AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (S : AddSubgroup G) (hS : Filter.Tendsto (↑(AddSubgroup.subtype S)) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousVAdd { x // x ∈ ↑AddSubgroup.opposite S } G

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.

theorem Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] (S : Subgroup G) (hS : Filter.Tendsto (↑(Subgroup.subtype S)) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousSMul { x // x ∈ ↑Subgroup.opposite S } G

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.

theorem SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace.SeparableSpace G] [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G

instance SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [TopologicalSpace.SeparableSpace G] [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G

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

instance SeparableWeaklyLocallyCompactGroup.sigmaCompactSpace {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] [TopologicalSpace.SeparableSpace G] [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G

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

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.

theorem exists_isCompact_isClosed_subset_isCompact_nhds_zero {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {L : Set G} (Lcomp : IsCompact L) (L1 : L ∈ nhds 0) : ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ L ∧ K ∈ nhds 0

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

theorem exists_isCompact_isClosed_subset_isCompact_nhds_one {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] {L : Set G} (Lcomp : IsCompact L) (L1 : L ∈ nhds 1) : ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ L ∧ K ∈ nhds 1

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

theorem local_isCompact_isClosed_nhds_of_addGroup {G : Type w} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [LocallyCompactSpace G] {U : Set G} (hU : U ∈ nhds 0) : ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 0 ∈ interior K

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.

theorem local_isCompact_isClosed_nhds_of_group {G : Type w} [TopologicalSpace G] [Group G] [TopologicalGroup G] [LocallyCompactSpace G] {U : Set G} (hU : U ∈ nhds 1) : ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 1 ∈ interior K

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

theorem exists_isCompact_isClosed_nhds_zero