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.

source

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

Prop

uniformContinuous_div : UniformContinuous fun p => p.fst / p.snd

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

Instances

source

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

Prop

uniformContinuous_sub : UniformContinuous fun p => p.fst - p.snd

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

Instances

source

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

UniformAddGroup α

source

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

UniformGroup α

source

theorem uniformContinuous_sub {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :

UniformContinuous fun p => p.fst - p.snd

source

theorem uniformContinuous_div {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :

UniformContinuous fun p => p.fst / p.snd

source

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

source

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

source

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

UniformContinuous fun x => -f x

source

theorem UniformContinuous.inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) :

UniformContinuous fun x => (f x)⁻¹

source

theorem uniformContinuous_neg {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :

UniformContinuous fun x => -x

source

theorem uniformContinuous_inv {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :

UniformContinuous fun x => x⁻¹

source

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

source

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

source

theorem uniformContinuous_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :

UniformContinuous fun p => p.fst + p.snd

source

theorem uniformContinuous_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :

UniformContinuous fun p => p.fst * p.snd

source

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

source

abbrev UniformContinuous.const_nsmul.match_1 (motive : ℕ → Prop) :

(x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive (Nat.succ n)) → motive x

Instances For

source

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

source

theorem uniformContinuous_const_nsmul {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (n : ℕ) :

UniformContinuous fun x => n • x

source

theorem uniformContinuous_pow_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (n : ℕ) :

UniformContinuous fun x => x ^ n

source

abbrev UniformContinuous.const_zsmul.match_1 (motive : ℤ → Prop) :

(x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x

Instances For

source

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

source

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

source

theorem uniformContinuous_const_zsmul {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (n : ℤ) :

UniformContinuous fun x => n • x

source

theorem uniformContinuous_zpow_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (n : ℤ) :

UniformContinuous fun x => x ^ n

source

theorem UniformAddGroup.to_topologicalAddGroup.proof_1 {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :

TopologicalAddGroup α

source

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

TopologicalAddGroup α

source

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

TopologicalGroup α

source

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

UniformAddGroup (α × β)

source

theorem instUniformAddGroupSumInstUniformSpaceSumInstAddGroup.proof_1 {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] :

UniformAddGroup (α × β)

source

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

UniformGroup (α × β)

source

theorem uniformity_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :

Filter.map (fun x => (x.fst + a, x.snd + a)) (uniformity α) = uniformity α

source

theorem uniformity_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :

Filter.map (fun x => (x.fst * a, x.snd * a)) (uniformity α) = uniformity α

source

theorem uniformEmbedding_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :

UniformEmbedding fun x => x + a

source

theorem uniformEmbedding_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (a : α) :

UniformEmbedding fun x => x * a

source

theorem AddOpposite.instUniformAddGroupAddOppositeInstUniformSpaceAddOppositeAddGroup.proof_1 {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :

UniformAddGroup αᵃᵒᵖ

source

instance AddOpposite.instUniformAddGroupAddOppositeInstUniformSpaceAddOppositeAddGroup {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :

UniformAddGroup αᵃᵒᵖ

source

instance MulOpposite.instUniformGroupMulOppositeInstUniformSpaceMulOppositeGroup {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :

UniformGroup αᵐᵒᵖ

source

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

UniformAddGroup { x // x ∈ S }

source

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

UniformAddGroup { x // x ∈ S }

source

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

UniformGroup { x // x ∈ S }

source

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

UniformAddGroup β

source

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

UniformGroup β

source

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

UniformAddGroup β

source

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

UniformGroup β

source

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

UniformAddGroup β

source

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

UniformGroup β

source

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

UniformAddGroup β

source

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

UniformGroup β

source

theorem uniformity_eq_comap_nhds_zero (α : Type u_1) [UniformSpace α] [AddGroup α] [UniformAddGroup α] :

uniformity α = Filter.comap (fun x => x.snd - x.fst) (nhds 0)

source

theorem uniformity_eq_comap_nhds_one (α : Type u_1) [UniformSpace α] [Group α] [UniformGroup α] :

uniformity α = Filter.comap (fun x => x.snd / x.fst) (nhds 1)

source

theorem uniformity_eq_comap_nhds_zero_swapped (α : Type u_1) [UniformSpace α] [AddGroup α] [UniformAddGroup α] :

uniformity α = Filter.comap (fun x => x.fst - x.snd) (nhds 0)

source

theorem uniformity_eq_comap_nhds_one_swapped (α : Type u_1) [UniformSpace α] [Group α] [UniformGroup α] :

uniformity α = Filter.comap (fun x => x.fst / x.snd) (nhds 1)

source

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

source

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

source

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

source

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

source

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

Filter.IsCountablyGenerated (uniformity α)

source

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

Filter.IsCountablyGenerated (uniformity α)

source

theorem uniformity_eq_comap_neg_add_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :

uniformity α = Filter.comap (fun x => -x.fst + x.snd) (nhds 0)

source

theorem uniformity_eq_comap_inv_mul_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :

uniformity α = Filter.comap (fun x => x.fst⁻¹ * x.snd) (nhds 1)

source

theorem uniformity_eq_comap_neg_add_nhds_zero_swapped {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :

uniformity α = Filter.comap (fun x => -x.snd + x.fst) (nhds 0)

source

theorem uniformity_eq_comap_inv_mul_nhds_one_swapped {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] :

uniformity α = Filter.comap (fun x => x.snd⁻¹ * x.fst) (nhds 1)

source

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.snd - x.fst ∈ U i}

source

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.snd / x.fst ∈ U i}

source

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.fst + x.snd ∈ U i}

source

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.fst⁻¹ * x.snd ∈ U i}

source

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.fst - x.snd ∈ U i}

source

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.fst / x.snd ∈ U i}

source

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.snd + x.fst ∈ U i}

source

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.snd⁻¹ * x.fst ∈ U i}

source

theorem addGroup_separationRel {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (x : α) (y : α) :

(x, y) ∈ separationRel α ↔ x - y ∈ closure {0}

source

theorem group_separationRel {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] (x : α) (y : α) :

(x, y) ∈ separationRel α ↔ x / y ∈ closure {1}

source

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

UniformContinuous ↑f

source

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

UniformContinuous ↑f

source

theorem uniformContinuous_of_continuousAt_zero {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {hom : Type u_3} [UniformSpace β] [AddGroup β] [UniformAddGroup β] [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.

source

theorem uniformContinuous_of_continuousAt_one {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {hom : Type u_3} [UniformSpace β] [Group β] [UniformGroup β] [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.

source

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

source

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

source

theorem UniformAddGroup.uniformContinuous_iff_open_ker {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {hom : Type u_3} [UniformSpace β] [DiscreteTopology β] [AddGroup β] [UniformAddGroup β] [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.

source

theorem UniformGroup.uniformContinuous_iff_open_ker {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [UniformGroup α] {hom : Type u_3} [UniformSpace β] [DiscreteTopology β] [Group β] [UniformGroup β] [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.

source

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

UniformContinuous ↑f

source

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

UniformContinuous ↑f

source

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

CauchySeq (u + v)

source

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

CauchySeq (u * v)

source

theorem CauchySeq.add_const {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ι → α} {x : α} (hu : CauchySeq u) :

CauchySeq fun n => u n + x

source

theorem CauchySeq.mul_const {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ι → α} {x : α} (hu : CauchySeq u) :

CauchySeq fun n => u n * x

source

theorem CauchySeq.const_add {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ι → α} {x : α} (hu : CauchySeq u) :

CauchySeq fun n => x + u n

source

theorem CauchySeq.const_mul {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {ι : Type u_3} [SemilatticeSup ι] {u : ι → α} {x : α} (hu : CauchySeq u) :

CauchySeq fun n => x * u n

source

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

CauchySeq (-u)

source

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

CauchySeq u⁻¹

source

theorem totallyBounded_iff_subset_finite_iUnion_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {s : Set α} :

TotallyBounded s ↔ ∀ (U : Set α), U ∈ nhds 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), y +ᵥ U

source

theorem totallyBounded_iff_subset_finite_iUnion_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [UniformGroup α] {s : Set α} :

TotallyBounded s ↔ ∀ (U : Set α), U ∈ nhds 1 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), y • U

source

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'

source

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'

source

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'

source

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'

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

theorem TopologicalAddGroup.toUniformSpace.proof_3 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] :

(Filter.lift' (Filter.comap (fun p => p.snd - p.fst) (nhds 0)) fun s => compRel s s) ≤ Filter.comap (fun p => p.snd - p.fst) (nhds 0)

source

theorem TopologicalAddGroup.toUniformSpace.proof_4 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] (S : Set G) :

IsOpen S ↔ ∀ (a : G), a ∈ S → {p | p.fst = a → p.snd ∈ S} ∈ Filter.comap (fun p => p.snd - p.fst) (nhds 0)

source

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

Filter.principal idRel ≤ Filter.comap (fun p => p.snd - p.fst) (nhds 0)

source

theorem TopologicalAddGroup.toUniformSpace.proof_2 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] :

Filter.Tendsto Prod.swap (Filter.comap (fun p => p.snd - p.fst) (nhds 0)) (Filter.comap (fun p => p.snd - p.fst) (nhds 0))

source

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

Instances For

source

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

Instances For

source

theorem uniformity_eq_comap_nhds_zero' (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] :

uniformity G = Filter.comap (fun p => p.snd - p.fst) (nhds 0)

source

theorem uniformity_eq_comap_nhds_one' (G : Type u_1) [Group G] [TopologicalSpace G] [TopologicalGroup G] :

uniformity G = Filter.comap (fun p => p.snd / p.fst) (nhds 1)

source

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

UniformAddGroup G

source

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

UniformGroup G

source

theorem AddSubgroup.isClosed_of_discrete.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {H : AddSubgroup G} [DiscreteTopology { x // x ∈ H }] :

IsClosed ↑H

source

instance AddSubgroup.isClosed_of_discrete {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {H : AddSubgroup G} [DiscreteTopology { x // x ∈ H }] :

IsClosed ↑H

source

instance Subgroup.isClosed_of_discrete {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] {H : Subgroup G} [DiscreteTopology { x // x ∈ H }] :

IsClosed ↑H

source

theorem AddSubgroup.tendsto_coe_cofinite_of_discrete {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] (H : AddSubgroup G) [DiscreteTopology { x // x ∈ H }] :

Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact G)

source

theorem Subgroup.tendsto_coe_cofinite_of_discrete {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] (H : Subgroup G) [DiscreteTopology { x // x ∈ H }] :

Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact G)

source

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 { x // x ∈ AddMonoidHom.range f }) :

Filter.Tendsto (↑f) Filter.cofinite (Filter.cocompact G)

source

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 { x // x ∈ MonoidHom.range f }) :

Filter.Tendsto (↑f) Filter.cofinite (Filter.cocompact G)

source

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 => p.snd - p.fst) ⁻¹' u ⊆ x), motive (_ : ∃ t, t ∈ nhds 0 ∧ (fun p => p.snd - p.fst) ⁻¹' t ⊆ x)) → motive x_1

Instances For

source

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 : Set G), u ∈ nhds 0 → ∀ᶠ (i : ι) in p, ∀ (a : α), F i a - f a ∈ u

source

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 : Set G), u ∈ nhds 1 → ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a ∈ u

source

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 : Set G), u ∈ nhds 0 → ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ s → F i a - f a ∈ u

source

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 : Set G), u ∈ nhds 1 → ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ s → F i a / f a ∈ u

source

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 : Set α) (motive : (x ∈ nhds x ∧ ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ x → F i a - f a ∈ u) → Prop) (x_1 : x ∈ nhds x ∧ ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ x → F i a - f a ∈ u), (∀ (h : x ∈ nhds x) (hp : ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ x → F i a - f a ∈ u), motive (_ : x ∈ nhds x ∧ ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ x → F i a - f a ∈ u)) → motive x_1

Instances For

source

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 : Set G), u ∈ nhds 0 → ∀ (x : α), ∃ t, t ∈ nhds x ∧ ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ t → F i a - f a ∈ u

source

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 : Set G), u ∈ nhds 1 → ∀ (x : α), ∃ t, t ∈ nhds x ∧ ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ t → F i a / f a ∈ u

source

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 : Set α) (motive : (x ∈ nhdsWithin x s ∧ ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ x → F i a - f a ∈ u) → Prop) (x_1 : x ∈ nhdsWithin x s ∧ ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ x → F i a - f a ∈ u), (∀ (h : x ∈ nhdsWithin x s) (hp : ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ x → F i a - f a ∈ u), motive (_ : x ∈ nhdsWithin x s ∧ ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ x → F i a - f a ∈ u)) → motive x_1

Instances For

source

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 : Set G), u ∈ nhds 0 → ∀ (x : α), x ∈ s → ∃ t, t ∈ nhdsWithin x s ∧ ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ t → F i a - f a ∈ u

source

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 : Set G), u ∈ nhds 1 → ∀ (x : α), x ∈ s → ∃ t, t ∈ nhdsWithin x s ∧ ∀ᶠ (i : ι) in p, ∀ (a : α), a ∈ t → F i a / f a ∈ u

source

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

UniformAddGroup G

source

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

UniformGroup G

source

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

TopologicalAddGroup.toUniformSpace G = u

source

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

TopologicalGroup.toUniformSpace G = u

source

theorem tendsto_sub_comap_self {α : Type u_1} {β : Type u_2} {hom : Type u_3} [TopologicalSpace α] [AddGroup α] [TopologicalAddGroup α] [TopologicalSpace β] [AddGroup β] [AddMonoidHomClass hom β α] {e : hom} (de : DenseInducing ↑e) (x₀ : α) :

Filter.Tendsto (fun t => t.snd - t.fst) (Filter.comap (fun p => (↑e p.fst, ↑e p.snd)) (nhds (x₀, x₀))) (nhds 0)

source

theorem tendsto_div_comap_self {α : Type u_1} {β : Type u_2} {hom : Type u_3} [TopologicalSpace α] [Group α] [TopologicalGroup α] [TopologicalSpace β] [Group β] [MonoidHomClass hom β α] {e : hom} (de : DenseInducing ↑e) (x₀ : α) :

Filter.Tendsto (fun t => t.snd / t.fst) (Filter.comap (fun p => (↑e p.fst, ↑e p.snd)) (nhds (x₀, x₀))) (nhds 1)

source

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] [SeparatedSpace G] [CompleteSpace G] {e : β →+ α} (de : DenseInducing ↑e) {f : δ →+ γ} (df : DenseInducing ↑f) {φ : β →+ δ →+ G} (hφ : Continuous fun p => ↑(↑φ p.fst) p.snd) :

Continuous (DenseInducing.extend (_ : DenseInducing fun p => (↑e p.fst, ↑f p.snd)) fun p => ↑(↑φ p.fst) p.snd)

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.

source

instance QuotientAddGroup.completeSpace' (G : Type u) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [TopologicalSpace.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.

source

theorem QuotientAddGroup.completeSpace'.proof_1 (G : Type u_1) [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [TopologicalSpace.FirstCountableTopology G] (N : AddSubgroup G) [AddSubgroup.Normal N] [CompleteSpace G] :

CompleteSpace (G ⧸ N)

source

instance QuotientGroup.completeSpace' (G : Type u) [Group G] [TopologicalSpace G] [TopologicalGroup G] [TopologicalSpace.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.

source

theorem QuotientAddGroup.completeSpace.proof_1 (G : Type u_1) [AddGroup G] [us : UniformSpace G] [UniformAddGroup G] [TopologicalSpace.FirstCountableTopology G] (N : AddSubgroup G) [AddSubgroup.Normal N] [hG : CompleteSpace G] :

CompleteSpace (G ⧸ N)

source

instance QuotientAddGroup.completeSpace (G : Type u) [AddGroup G] [us : UniformSpace G] [UniformAddGroup G] [TopologicalSpace.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.

source

instance QuotientGroup.completeSpace (G : Type u) [Group G] [us : UniformSpace G] [UniformGroup G] [TopologicalSpace.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.