Uniform structure on topological groups #
Main results #
extension of ℤ-bilinear maps to complete groups (useful for ring completions)
QuotientGroup.completeSpaceandQuotientAddGroup.completeSpaceguarantee 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.
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
isUniformEmbedding_translate_add
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
(a : α)
:
IsUniformEmbedding fun (x : α) => x + a
theorem
isUniformEmbedding_translate_mul
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
(a : α)
:
IsUniformEmbedding fun (x : α) => x * a
@[deprecated isUniformEmbedding_translate_mul]
theorem
uniformEmbedding_translate_mul
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
(a : α)
:
IsUniformEmbedding fun (x : α) => x * a
Alias of isUniformEmbedding_translate_mul.
theorem
IsUniformInducing.uniformAddGroup
{β : Type u_2}
[AddGroup β]
{γ : Type u_3}
[AddGroup γ]
[UniformSpace γ]
[UniformAddGroup γ]
[UniformSpace β]
{F : Type u_4}
[FunLike F β γ]
[AddMonoidHomClass F β γ]
(f : F)
(hf : IsUniformInducing ⇑f)
:
theorem
IsUniformInducing.uniformGroup
{β : Type u_2}
[Group β]
{γ : Type u_3}
[Group γ]
[UniformSpace γ]
[UniformGroup γ]
[UniformSpace β]
{F : Type u_4}
[FunLike F β γ]
[MonoidHomClass F β γ]
(f : F)
(hf : IsUniformInducing ⇑f)
:
@[deprecated IsUniformInducing.uniformGroup]
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 : IsUniformInducing ⇑f)
:
Alias of IsUniformInducing.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)
:
theorem
UniformGroup.comap
{β : Type u_2}
[Group β]
{γ : Type u_3}
[Group γ]
{u : UniformSpace γ}
[UniformGroup γ]
{F : Type u_4}
[FunLike F β γ]
[MonoidHomClass F β γ]
(f : F)
:
instance
AddSubgroup.uniformAddGroup
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
(S : AddSubgroup α)
:
Equations
- ⋯ = ⋯
instance
Subgroup.uniformGroup
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
(S : Subgroup α)
:
UniformGroup ↥S
Equations
- ⋯ = ⋯
theorem
CauchySeq.add
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
{v : ι → α}
(hu : CauchySeq u)
(hv : CauchySeq v)
:
theorem
CauchySeq.mul
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
{v : ι → α}
(hu : CauchySeq u)
(hv : CauchySeq v)
:
theorem
CauchySeq.add_const
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
{x : α}
(hu : CauchySeq u)
:
theorem
CauchySeq.mul_const
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
{x : α}
(hu : CauchySeq u)
:
theorem
CauchySeq.const_add
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
{x : α}
(hu : CauchySeq u)
:
theorem
CauchySeq.const_mul
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
{x : α}
(hu : CauchySeq u)
:
theorem
CauchySeq.neg
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
(h : CauchySeq u)
:
theorem
CauchySeq.inv
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
(h : CauchySeq u)
:
theorem
totallyBounded_iff_subset_finite_iUnion_nhds_zero
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{s : Set α}
:
theorem
totallyBounded_iff_subset_finite_iUnion_nhds_one
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
{s : Set α}
:
theorem
totallyBounded_neg
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{s : Set α}
(hs : TotallyBounded s)
:
TotallyBounded (-s)
theorem
totallyBounded_inv
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
{s : Set α}
(hs : TotallyBounded s)
:
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_is_uniform_of_compactSpace
(G : Type u_1)
[AddGroup G]
[TopologicalSpace G]
[TopologicalAddGroup G]
[CompactSpace G]
:
theorem
topologicalGroup_is_uniform_of_compactSpace
(G : Type u_1)
[Group G]
[TopologicalSpace G]
[TopologicalGroup G]
[CompactSpace 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 ↥f.range)
:
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 ↥f.range)
:
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
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 ι)
:
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 ι)
:
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
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
IsDenseInducing.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]
{e : β →+ α}
(de : IsDenseInducing ⇑e)
{f : δ →+ γ}
(df : IsDenseInducing ⇑f)
{φ : β →+ δ →+ G}
(hφ : Continuous fun (p : β × δ) => (φ p.1) p.2)
[UniformAddGroup G]
[T0Space G]
[CompleteSpace G]
:
Continuous (⋯.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)
[N.Normal]
[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)
[N.Normal]
[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)
[N.Normal]
[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)
[N.Normal]
[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
- ⋯ = ⋯