Uniform structure on topological groups

This file defines uniform groups and its additive counterpart. These typeclasses should be preferred over using [TopologicalSpace α] [TopologicalGroup α] since every topological group naturally induces a uniform structure.

Main declarations

• UniformGroup and UniformAddGroup: Multiplicative and additive uniform groups, that i.e., groups with uniformly continuous (*) and (⁻¹) / (+) and (-).

Main results

• TopologicalAddGroup.toUniformSpace and comm_topologicalAddGroup_is_uniform can be used to construct a canonical uniformity for a topological add group.

• extension of ℤ-bilinear maps to complete groups (useful for ring completions)

• QuotientGroup.completeSpace and QuotientAddGroup.completeSpace guarantee that quotients of first countable topological groups by normal subgroups are themselves complete. In particular, the quotient of a Banach space by a subspace is complete.

class UniformGroup (α : Type u_3) [UniformSpace α] [Group α] : Prop

A uniform group is a group in which multiplication and inversion are uniformly continuous.

• uniformContinuous_div : UniformContinuous fun (p : α × α) => p.1 / p.2

class UniformAddGroup (α : Type u_3) [UniformSpace α] [AddGroup α] : Prop

A uniform additive group is an additive group in which addition and negation are uniformly continuous.

• uniformContinuous_sub : UniformContinuous fun (p : α × α) => p.1 - p.2

theorem UniformAddGroup.mk' {α : Type u_3} [UniformSpace α] [AddGroup α] (h₁ : UniformContinuous fun (p : α × α) => p.1 + p.2) (h₂ : UniformContinuous fun (p : α) => -p) : UniformAddGroup α

theorem UniformGroup.mk' {α : Type u_3} [UniformSpace α] [Group α] (h₁ : UniformContinuous fun (p : α × α) => p.1 * p.2) (h₂ : UniformContinuous fun (p : α) => p⁻¹) : UniformGroup α

theorem uniformContinuous_sub {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] : UniformContinuous fun (p : α × α) => p.1 - p.2

theorem uniformContinuous_div {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] : UniformContinuous fun (p : α × α) => p.1 / p.2

theorem UniformContinuous.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun (x : β) => f x - g x

theorem UniformContinuous.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun (x : β) => f x / g x

theorem UniformContinuous.neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) : UniformContinuous fun (x : β) => -f x

theorem UniformContinuous.inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) : UniformContinuous fun (x : β) => (f x)⁻¹

theorem uniformContinuous_neg {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] : UniformContinuous fun (x : α) => -x

theorem uniformContinuous_inv {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] : UniformContinuous fun (x : α) => x⁻¹

theorem UniformContinuous.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun (x : β) => f x + g x

theorem UniformContinuous.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun (x : β) => f x * g x

theorem uniformContinuous_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] : UniformContinuous fun (p : α × α) => p.1 + p.2

theorem uniformContinuous_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] : UniformContinuous fun (p : α × α) => p.1 * p.2

theorem UniformContinuous.const_nsmul {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (n : ℕ) : UniformContinuous fun (x : β) => n • f x

abbrev UniformContinuous.const_nsmul.match_1 (motive : ℕ → Prop) : ∀ (x : ℕ), (Unit → motive 0) → (∀ (n : ℕ), motive (Nat.succ n)) → motive x

Equations

• ⋯ = ⋯

theorem UniformContinuous.pow_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (n : ℕ) : UniformContinuous fun (x : β) => f x ^ n

theorem uniformContinuous_const_nsmul {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (n : ℕ) : UniformContinuous fun (x : α) => n • x

theorem uniformContinuous_pow_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (n : ℕ) : UniformContinuous fun (x : α) => x ^ n

abbrev UniformContinuous.const_zsmul.match_1 (motive : ℤ → Prop) : ∀ (x : ℤ), (∀ (n : ℕ), motive (Int.ofNat n)) → (∀ (n : ℕ), motive (Int.negSucc n)) → motive x

Equations

• ⋯ = ⋯

theorem UniformContinuous.const_zsmul {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (n : ℤ) : UniformContinuous fun (x : β) => n • f x

theorem UniformContinuous.zpow_const {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (n : ℤ) : UniformContinuous fun (x : β) => f x ^ n

theorem uniformContinuous_const_zsmul {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (n : ℤ) : UniformContinuous fun (x : α) => n • x

theorem uniformContinuous_zpow_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (n : ℤ) : UniformContinuous fun (x : α) => x ^ n

instance UniformAddGroup.to_topologicalAddGroup {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] : TopologicalAddGroup α

Equations

• ⋯ = ⋯

instance UniformGroup.to_topologicalGroup {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] : TopologicalGroup α

Equations

• ⋯ = ⋯

instance instUniformAddGroupSumInstUniformSpaceSumInstAddGroup {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] : UniformAddGroup (α × β)

Equations

• ⋯ = ⋯

instance instUniformGroupProdInstUniformSpaceProdInstGroup {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] [Group β] [UniformGroup β] : UniformGroup (α × β)

Equations

• ⋯ = ⋯

instance Pi.instUniformAddGroup {ι : Type u_3} {G : ι → Type u_4} [(i : ι) → UniformSpace (G i)] [(i : ι) → AddGroup (G i)] [∀ (i : ι), UniformAddGroup (G i)] : UniformAddGroup ((i : ι) → G i)

Equations

• ⋯ = ⋯

instance Pi.instUniformGroup {ι : Type u_3} {G : ι → Type u_4} [(i : ι) → UniformSpace (G i)] [(i : ι) → Group (G i)] [∀ (i : ι), UniformGroup (G i)] : UniformGroup ((i : ι) → G i)

Equations

• ⋯ = ⋯

theorem uniformity_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) : Filter.map (fun (x : α × α) => (x.1 + a, x.2 + a)) (uniformity α) = uniformity α

theorem uniformity_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) : Filter.map (fun (x : α × α) => (x.1 * a, x.2 * a)) (uniformity α) = uniformity α

theorem uniformEmbedding_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) : UniformEmbedding fun (x : α) => x + a

theorem uniformEmbedding_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) : UniformEmbedding fun (x : α) => x * a

instance AddOpposite.instUniformAddGroupAddOppositeInstUniformSpaceAddOppositeInstAddGroup {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] : UniformAddGroup αᵃᵒᵖ

Equations

• ⋯ = ⋯

instance MulOpposite.instUniformGroupMulOppositeInstUniformSpaceMulOppositeInstGroup {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] : UniformGroup αᵐᵒᵖ

Equations

• ⋯ = ⋯

theorem uniformAddGroup_sInf {β : Type u_2} [AddGroup β] {us : Set (UniformSpace β)} (h : ∀ u ∈ us, UniformAddGroup β) : UniformAddGroup β

theorem uniformGroup_sInf {β : Type u_2} [Group β] {us : Set (UniformSpace β)} (h : ∀ u ∈ us, UniformGroup β) : UniformGroup β

theorem uniformAddGroup_iInf {β : Type u_2} [AddGroup β] {ι : Sort u_3} {us' : ι → UniformSpace β} (h' : ∀ (i : ι), UniformAddGroup β) : UniformAddGroup β

theorem uniformGroup_iInf {β : Type u_2} [Group β] {ι : Sort u_3} {us' : ι → UniformSpace β} (h' : ∀ (i : ι), UniformGroup β) : UniformGroup β

theorem uniformAddGroup_inf {β : Type u_2} [AddGroup β] {u₁ : UniformSpace β} {u₂ : UniformSpace β} (h₁ : UniformAddGroup β) (h₂ : UniformAddGroup β) : UniformAddGroup β

theorem uniformGroup_inf {β : Type u_2} [Group β] {u₁ : UniformSpace β} {u₂ : UniformSpace β} (h₁ : UniformGroup β) (h₂ : UniformGroup β) : UniformGroup β

theorem UniformInducing.uniformAddGroup {β : Type u_2} [AddGroup β] {γ : Type u_3} [AddGroup γ] [UniformSpace γ] [UniformAddGroup γ] [UniformSpace β] {F : Type u_4} [FunLike F β γ] [AddMonoidHomClass F β γ] (f : F) (hf : UniformInducing ⇑f) : UniformAddGroup β

theorem UniformInducing.uniformGroup {β : Type u_2} [Group β] {γ : Type u_3} [Group γ] [UniformSpace γ] [UniformGroup γ] [UniformSpace β] {F : Type u_4} [FunLike F β γ] [MonoidHomClass F β γ] (f : F) (hf : UniformInducing ⇑f) : UniformGroup β

theorem UniformAddGroup.comap {β : Type u_2} [AddGroup β] {γ : Type u_3} [AddGroup γ] {u : UniformSpace γ} [UniformAddGroup γ] {F : Type u_4} [FunLike F β γ] [AddMonoidHomClass F β γ] (f : F) : UniformAddGroup β

theorem UniformGroup.comap {β : Type u_2} [Group β] {γ : Type u_3} [Group γ] {u : UniformSpace γ} [UniformGroup γ] {F : Type u_4} [FunLike F β γ] [MonoidHomClass F β γ] (f : F) : UniformGroup β

instance AddSubgroup.uniformAddGroup {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (S : AddSubgroup α) : UniformAddGroup ↥S

Equations

• ⋯ = ⋯

instance Subgroup.uniformGroup {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (S : Subgroup α) : UniformGroup ↥S

Equations

• ⋯ = ⋯

theorem uniformity_eq_comap_nhds_zero (α : Type u_1) [UniformSpace α] [AddGroup α] [UniformAddGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.2 - x.1) (nhds 0)

theorem uniformity_eq_comap_nhds_one (α : Type u_1) [UniformSpace α] [Group α] [UniformGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.2 / x.1) (nhds 1)

theorem uniformity_eq_comap_nhds_zero_swapped (α : Type u_1) [UniformSpace α] [AddGroup α] [UniformAddGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.1 - x.2) (nhds 0)

theorem uniformity_eq_comap_nhds_one_swapped (α : Type u_1) [UniformSpace α] [Group α] [UniformGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.1 / x.2) (nhds 1)

theorem UniformAddGroup.ext {G : Type u_3} [AddGroup G] {u : UniformSpace G} {v : UniformSpace G} (hu : UniformAddGroup G) (hv : UniformAddGroup G) (h : nhds 0 = nhds 0) : u = v

theorem UniformGroup.ext {G : Type u_3} [Group G] {u : UniformSpace G} {v : UniformSpace G} (hu : UniformGroup G) (hv : UniformGroup G) (h : nhds 1 = nhds 1) : u = v

theorem UniformAddGroup.ext_iff {G : Type u_3} [AddGroup G] {u : UniformSpace G} {v : UniformSpace G} (hu : UniformAddGroup G) (hv : UniformAddGroup G) : u = v ↔ nhds 0 = nhds 0

theorem UniformGroup.ext_iff {G : Type u_3} [Group G] {u : UniformSpace G} {v : UniformSpace G} (hu : UniformGroup G) (hv : UniformGroup G) : u = v ↔ nhds 1 = nhds 1

theorem UniformAddGroup.uniformity_countably_generated {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [Filter.IsCountablyGenerated (nhds 0)] : Filter.IsCountablyGenerated (uniformity α)

theorem UniformGroup.uniformity_countably_generated {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] [Filter.IsCountablyGenerated (nhds 1)] : Filter.IsCountablyGenerated (uniformity α)

theorem uniformity_eq_comap_neg_add_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] : uniformity α = Filter.comap (fun (x : α × α) => -x.1 + x.2) (nhds 0)

theorem uniformity_eq_comap_inv_mul_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.1⁻¹ * x.2) (nhds 1)

theorem uniformity_eq_comap_neg_add_nhds_zero_swapped {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] : uniformity α = Filter.comap (fun (x : α × α) => -x.2 + x.1) (nhds 0)

theorem uniformity_eq_comap_inv_mul_nhds_one_swapped {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] : uniformity α = Filter.comap (fun (x : α × α) => x.2⁻¹ * x.1) (nhds 1)

theorem Filter.HasBasis.uniformity_of_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : Filter.HasBasis (nhds 0) p U) : Filter.HasBasis (uniformity α) p fun (i : ι) => {x : α × α | x.2 - x.1 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : Filter.HasBasis (nhds 1) p U) : Filter.HasBasis (uniformity α) p fun (i : ι) => {x : α × α | x.2 / x.1 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_zero_neg_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : Filter.HasBasis (nhds 0) p U) : Filter.HasBasis (uniformity α) p fun (i : ι) => {x : α × α | -x.1 + x.2 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : Filter.HasBasis (nhds 1) p U) : Filter.HasBasis (uniformity α) p fun (i : ι) => {x : α × α | x.1⁻¹ * x.2 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_zero_swapped {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : Filter.HasBasis (nhds 0) p U) : Filter.HasBasis (uniformity α) p fun (i : ι) => {x : α × α | x.1 - x.2 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_one_swapped {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : Filter.HasBasis (nhds 1) p U) : Filter.HasBasis (uniformity α) p fun (i : ι) => {x : α × α | x.1 / x.2 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_zero_neg_add_swapped {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : Filter.HasBasis (nhds 0) p U) : Filter.HasBasis (uniformity α) p fun (i : ι) => {x : α × α | -x.2 + x.1 ∈ U i}

theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul_swapped {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Sort u_3} {p : ι → Prop} {U : ι → Set α} (h : Filter.HasBasis (nhds 1) p U) : Filter.HasBasis (uniformity α) p fun (i : ι) => {x : α × α | x.2⁻¹ * x.1 ∈ U i}

theorem uniformContinuous_of_tendsto_zero {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [UniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] {f : hom} (h : Filter.Tendsto (⇑f) (nhds 0) (nhds 0)) : UniformContinuous ⇑f

theorem uniformContinuous_of_tendsto_one {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {hom : Type u_3} [UniformSpace β] [Group β] [UniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Filter.Tendsto (⇑f) (nhds 1) (nhds 1)) : UniformContinuous ⇑f

theorem uniformContinuous_of_continuousAt_zero {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [UniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] (f : hom) (hf : ContinuousAt (⇑f) 0) : UniformContinuous ⇑f

An additive group homomorphism (a bundled morphism of a type that implements AddMonoidHomClass) between two uniform additive groups is uniformly continuous provided that it is continuous at zero. See also continuous_of_continuousAt_zero.

theorem uniformContinuous_of_continuousAt_one {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {hom : Type u_3} [UniformSpace β] [Group β] [UniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] (f : hom) (hf : ContinuousAt (⇑f) 1) : UniformContinuous ⇑f

A group homomorphism (a bundled morphism of a type that implements MonoidHomClass) between two uniform groups is uniformly continuous provided that it is continuous at one. See also continuous_of_continuousAt_one.

theorem AddMonoidHom.uniformContinuous_of_continuousAt_zero {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] (f : α →+ β) (hf : ContinuousAt (⇑f) 0) : UniformContinuous ⇑f

theorem MonoidHom.uniformContinuous_of_continuousAt_one {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] [Group β] [UniformGroup β] (f : α →* β) (hf : ContinuousAt (⇑f) 1) : UniformContinuous ⇑f

theorem UniformAddGroup.uniformContinuous_iff_open_ker {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {hom : Type u_3} [UniformSpace β] [DiscreteTopology β] [AddGroup β] [UniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] {f : hom} : UniformContinuous ⇑f ↔ IsOpen ↑(AddMonoidHom.ker ↑f)

A homomorphism from a uniform additive group to a discrete uniform additive group is continuous if and only if its kernel is open.

theorem UniformGroup.uniformContinuous_iff_open_ker {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {hom : Type u_3} [UniformSpace β] [DiscreteTopology β] [Group β] [UniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} : UniformContinuous ⇑f ↔ IsOpen ↑(MonoidHom.ker ↑f)

A homomorphism from a uniform group to a discrete uniform group is continuous if and only if its kernel is open.

theorem uniformContinuous_addMonoidHom_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [UniformAddGroup β] [FunLike hom α β] [AddMonoidHomClass hom α β] {f : hom} (h : Continuous ⇑f) : UniformContinuous ⇑f

theorem uniformContinuous_monoidHom_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {hom : Type u_3} [UniformSpace β] [Group β] [UniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Continuous ⇑f) : UniformContinuous ⇑f

theorem CauchySeq.add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} {v : ι → α} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq (u + v)

theorem CauchySeq.mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} {v : ι → α} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq (u * v)

theorem CauchySeq.add_const {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) : CauchySeq fun (n : ι) => u n + x

theorem CauchySeq.mul_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) : CauchySeq fun (n : ι) => u n * x

theorem CauchySeq.const_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) : CauchySeq fun (n : ι) => x + u n

theorem CauchySeq.const_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) : CauchySeq fun (n : ι) => x * u n

theorem CauchySeq.neg {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} (h : CauchySeq u) : CauchySeq (-u)

theorem CauchySeq.inv {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} (h : CauchySeq u) : CauchySeq u⁻¹

theorem totallyBounded_iff_subset_finite_iUnion_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {s : Set α} : TotallyBounded s ↔ ∀ U ∈ nhds 0, ∃ (t : Set α), Set.Finite t ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U

theorem totallyBounded_iff_subset_finite_iUnion_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {s : Set α} : TotallyBounded s ↔ ∀ U ∈ nhds 1, ∃ (t : Set α), Set.Finite t ∧ s ⊆ ⋃ y ∈ t, y • U

theorem TendstoUniformlyOnFilter.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (f + f') (g + g') l l'

theorem TendstoUniformlyOnFilter.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (f * f') (g * g') l l'

theorem TendstoUniformlyOnFilter.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (f - f') (g - g') l l'

theorem TendstoUniformlyOnFilter.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (f / f') (g / g') l l'

theorem TendstoUniformlyOn.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f + f') (g + g') l s

theorem TendstoUniformlyOn.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f * f') (g * g') l s

theorem TendstoUniformlyOn.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f - f') (g - g') l s

theorem TendstoUniformlyOn.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f / f') (g / g') l s

theorem TendstoUniformly.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (f + f') (g + g') l

theorem TendstoUniformly.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (f * f') (g * g') l

theorem TendstoUniformly.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (f - f') (g - g') l

theorem TendstoUniformly.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {g : β → α} {g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (f / f') (g / g') l

theorem UniformCauchySeqOn.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (f + f') l s

theorem UniformCauchySeqOn.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (f * f') l s

theorem UniformCauchySeqOn.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (f - f') l s

theorem UniformCauchySeqOn.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (f / f') l s

theorem TopologicalAddGroup.toUniformSpace.proof_3 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] : ∀ (x : G), nhds x = Filter.comap (Prod.mk x) (Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0))

theorem TopologicalAddGroup.toUniformSpace.proof_1 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] : Filter.Tendsto Prod.swap (Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)) (Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0))

theorem TopologicalAddGroup.toUniformSpace.proof_2 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] : (Filter.lift' (Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)) fun (s : Set (G × G)) => compRel s s) ≤ Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)

def TopologicalAddGroup.toUniformSpace (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] : UniformSpace G

The right uniformity on a topological additive group (as opposed to the left uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a UniformAddGroup structure. Two important special cases where they do coincide are for commutative additive groups (see comm_topologicalAddGroup_is_uniform) and for compact additive groups (see topologicalAddGroup_is_uniform_of_compactSpace).

Equations

• TopologicalAddGroup.toUniformSpace G = UniformSpace.mk (Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)) ⋯ ⋯ ⋯

def TopologicalGroup.toUniformSpace (G : Type u_1) [Group G] [TopologicalSpace G] [TopologicalGroup G] : UniformSpace G

The right uniformity on a topological group (as opposed to the left uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a UniformGroup structure. Two important special cases where they do coincide are for commutative groups (see comm_topologicalGroup_is_uniform) and for compact groups (see topologicalGroup_is_uniform_of_compactSpace).

Equations

• TopologicalGroup.toUniformSpace G = UniformSpace.mk (Filter.comap (fun (p : G × G) => p.2 / p.1) (nhds 1)) ⋯ ⋯ ⋯

theorem uniformity_eq_comap_nhds_zero' (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] : uniformity G = Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)

theorem uniformity_eq_comap_nhds_one' (G : Type u_1) [Group G] [TopologicalSpace G] [TopologicalGroup G] : uniformity G = Filter.comap (fun (p : G × G) => p.2 / p.1) (nhds 1)

theorem topologicalAddGroup_is_uniform_of_compactSpace (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [CompactSpace G] : UniformAddGroup G

theorem topologicalGroup_is_uniform_of_compactSpace (G : Type u_1) [Group G] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] : UniformGroup G

instance AddSubgroup.isClosed_of_discrete {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {H : AddSubgroup G} [DiscreteTopology ↥H] : IsClosed ↑H

Equations

• ⋯ = ⋯

instance Subgroup.isClosed_of_discrete {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] {H : Subgroup G} [DiscreteTopology ↥H] : IsClosed ↑H

Equations

• ⋯ = ⋯

theorem AddSubgroup.tendsto_coe_cofinite_of_discrete {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] (H : AddSubgroup G) [DiscreteTopology ↥H] : Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact G)

theorem Subgroup.tendsto_coe_cofinite_of_discrete {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] (H : Subgroup G) [DiscreteTopology ↥H] : Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact G)

theorem AddMonoidHom.tendsto_coe_cofinite_of_discrete {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {H : Type u_2} [AddGroup H] {f : H →+ G} (hf : Function.Injective ⇑f) (hf' : DiscreteTopology ↥(AddMonoidHom.range f)) : Filter.Tendsto (⇑f) Filter.cofinite (Filter.cocompact G)

theorem MonoidHom.tendsto_coe_cofinite_of_discrete {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] {H : Type u_2} [Group H] {f : H →* G} (hf : Function.Injective ⇑f) (hf' : DiscreteTopology ↥(MonoidHom.range f)) : Filter.Tendsto (⇑f) Filter.cofinite (Filter.cocompact G)

theorem TopologicalAddGroup.tendstoUniformly_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {ι : Type u_2} {α : Type u_3} (F : ι → α → G) (f : α → G) (p : Filter ι) : TendstoUniformly F f p ↔ ∀ u ∈ nhds 0, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a - f a ∈ u

abbrev TopologicalAddGroup.tendstoUniformly_iff.match_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] : ∀ (x : Set (G × G)) (motive : x ∈ uniformity G → Prop) (x_1 : x ∈ uniformity G), (∀ (u : Set G) (hu : u ∈ nhds 0) (hv : (fun (p : G × G) => p.2 - p.1) ⁻¹' u ⊆ x), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem TopologicalGroup.tendstoUniformly_iff {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {ι : Type u_2} {α : Type u_3} (F : ι → α → G) (f : α → G) (p : Filter ι) : TendstoUniformly F f p ↔ ∀ u ∈ nhds 1, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a ∈ u

theorem TopologicalAddGroup.tendstoUniformlyOn_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {ι : Type u_2} {α : Type u_3} (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) : TendstoUniformlyOn F f p s ↔ ∀ u ∈ nhds 0, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a - f a ∈ u

theorem TopologicalGroup.tendstoUniformlyOn_iff {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {ι : Type u_2} {α : Type u_3} (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) : TendstoUniformlyOn F f p s ↔ ∀ u ∈ nhds 1, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a / f a ∈ u

theorem TopologicalAddGroup.tendstoLocallyUniformly_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {ι : Type u_2} {α : Type u_3} [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) : TendstoLocallyUniformly F f p ↔ ∀ u ∈ nhds 0, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u

abbrev TopologicalAddGroup.tendstoLocallyUniformly_iff.match_1 {G : Type u_3} [AddGroup G] {ι : Type u_2} {α : Type u_1} [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (x : α) (u : Set G) : ∀ (x_1 : Set α) (motive : (x_1 ∈ nhds x ∧ ∀ᶠ (i : ι) in p, ∀ a ∈ x_1, F i a - f a ∈ u) → Prop) (x_2 : x_1 ∈ nhds x ∧ ∀ᶠ (i : ι) in p, ∀ a ∈ x_1, F i a - f a ∈ u), (∀ (h : x_1 ∈ nhds x) (hp : ∀ᶠ (i : ι) in p, ∀ a ∈ x_1, F i a - f a ∈ u), motive ⋯) → motive x_2

Equations

• ⋯ = ⋯

theorem TopologicalGroup.tendstoLocallyUniformly_iff {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {ι : Type u_2} {α : Type u_3} [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) : TendstoLocallyUniformly F f p ↔ ∀ u ∈ nhds 1, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u

theorem TopologicalAddGroup.tendstoLocallyUniformlyOn_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {ι : Type u_2} {α : Type u_3} [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) : TendstoLocallyUniformlyOn F f p s ↔ ∀ u ∈ nhds 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u

abbrev TopologicalAddGroup.tendstoLocallyUniformlyOn_iff.match_1 {G : Type u_3} [AddGroup G] {ι : Type u_2} {α : Type u_1} [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (x : α) (u : Set G) : ∀ (x_1 : Set α) (motive : (x_1 ∈ nhdsWithin x s ∧ ∀ᶠ (i : ι) in p, ∀ a ∈ x_1, F i a - f a ∈ u) → Prop) (x_2 : x_1 ∈ nhdsWithin x s ∧ ∀ᶠ (i : ι) in p, ∀ a ∈ x_1, F i a - f a ∈ u), (∀ (h : x_1 ∈ nhdsWithin x s) (hp : ∀ᶠ (i : ι) in p, ∀ a ∈ x_1, F i a - f a ∈ u), motive ⋯) → motive x_2

Equations

• ⋯ = ⋯

theorem TopologicalGroup.tendstoLocallyUniformlyOn_iff {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] {ι : Type u_2} {α : Type u_3} [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) : TendstoLocallyUniformlyOn F f p s ↔ ∀ u ∈ nhds 1, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u

theorem comm_topologicalAddGroup_is_uniform {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] : UniformAddGroup G

theorem comm_topologicalGroup_is_uniform {G : Type u_1} [CommGroup G] [TopologicalSpace G] [TopologicalGroup G] : UniformGroup G

theorem UniformAddGroup.toUniformSpace_eq {G : Type u_2} [u : UniformSpace G] [AddGroup G] [UniformAddGroup G] : TopologicalAddGroup.toUniformSpace G = u

theorem UniformGroup.toUniformSpace_eq {G : Type u_2} [u : UniformSpace G] [Group G] [UniformGroup G] : TopologicalGroup.toUniformSpace G = u

theorem tendsto_sub_comap_self {α : Type u_1} {β : Type u_2} {hom : Type u_3} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] [TopologicalSpace β] [AddGroup β] [FunLike hom β α] [AddMonoidHomClass hom β α] {e : hom} (de : DenseInducing ⇑e) (x₀ : α) : Filter.Tendsto (fun (t : β × β) => t.2 - t.1) (Filter.comap (fun (p : β × β) => (e p.1, e p.2)) (nhds (x₀, x₀))) (nhds 0)

theorem tendsto_div_comap_self {α : Type u_1} {β : Type u_2} {hom : Type u_3} [TopologicalSpace α] [Group α] [TopologicalGroup α] [TopologicalSpace β] [Group β] [FunLike hom β α] [MonoidHomClass hom β α] {e : hom} (de : DenseInducing ⇑e) (x₀ : α) : Filter.Tendsto (fun (t : β × β) => t.2 / t.1) (Filter.comap (fun (p : β × β) => (e p.1, e p.2)) (nhds (x₀, x₀))) (nhds 1)

theorem DenseInducing.extend_Z_bilin {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {G : Type u_5} [TopologicalSpace α] [AddCommGroup α] [TopologicalAddGroup α] [TopologicalSpace β] [AddCommGroup β] [TopologicalSpace γ] [AddCommGroup γ] [TopologicalAddGroup γ] [TopologicalSpace δ] [AddCommGroup δ] [UniformSpace G] [AddCommGroup G] [UniformAddGroup G] [T0Space G] [CompleteSpace G] {e : β →+ α} (de : DenseInducing ⇑e) {f : δ →+ γ} (df : DenseInducing ⇑f) {φ : β →+ δ →+ G} (hφ : Continuous fun (p : β × δ) => (φ p.1) p.2) : Continuous (DenseInducing.extend ⋯ fun (p : β × δ) => (φ p.1) p.2)

Bourbaki GT III.6.5 Theorem I: ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity. Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary.

instance QuotientAddGroup.completeSpace' (G : Type u) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [AddSubgroup.Normal N] [CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable topological additive group G by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by subspaces are complete. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Because an additive topological group is not equipped with a UniformSpace instance by default, we must explicitly provide it in order to consider completeness. See QuotientAddGroup.completeSpace for a version in which G is already equipped with a uniform structure.

Equations

• ⋯ = ⋯

instance QuotientGroup.completeSpace' (G : Type u) [Group G] [TopologicalSpace G] [TopologicalGroup G] [FirstCountableTopology G] (N : Subgroup G) [Subgroup.Normal N] [CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable topological group G by a normal subgroup is itself complete. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Because a topological group is not equipped with a UniformSpace instance by default, we must explicitly provide it in order to consider completeness. See QuotientGroup.completeSpace for a version in which G is already equipped with a uniform structure.

Equations

• ⋯ = ⋯

instance QuotientAddGroup.completeSpace (G : Type u) [AddGroup G] [us : UniformSpace G] [UniformAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [AddSubgroup.Normal N] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable uniform additive group G by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by subspaces are complete. In contrast to QuotientAddGroup.completeSpace', in this version G is already equipped with a uniform structure. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Even though G is equipped with a uniform structure, the quotient G ⧸ N does not inherit a uniform structure, so it is still provided manually via TopologicalAddGroup.toUniformSpace. In the most common use case ─ quotients of normed additive commutative groups by subgroups ─ significant care was taken so that the uniform structure inherent in that setting coincides (definitionally) with the uniform structure provided here.

Equations

• ⋯ = ⋯

instance QuotientGroup.completeSpace (G : Type u) [Group G] [us : UniformSpace G] [UniformGroup G] [FirstCountableTopology G] (N : Subgroup G) [Subgroup.Normal N] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable uniform group G by a normal subgroup is itself complete. In contrast to QuotientGroup.completeSpace', in this version G is already equipped with a uniform structure. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Even though G is equipped with a uniform structure, the quotient G ⧸ N does not inherit a uniform structure, so it is still provided manually via TopologicalGroup.toUniformSpace. In the most common use cases, this coincides (definitionally) with the uniform structure on the quotient obtained via other means.

Equations

• ⋯ = ⋯