Countable generation of neighbourhoods passes to the separated completion #
If the neighbourhood filter of a point of a uniform space is countably generated, so is the neighbourhood filter of its image in the separated completion. Nothing is assumed of the space beyond its uniformity — no separation, no completeness, no algebraic structure.
TauCeti.Topology.Algebra.GroupCompletion specialises this to the zero of a uniform
space with a zero, which is the form typeclass resolution consumes.
Main results #
theorem
UniformSpace.Completion.isCountablyGenerated_nhds_coe
{α : Type u_1}
[UniformSpace α]
{x : α}
[(nhds x).IsCountablyGenerated]
:
(nhds ↑x).IsCountablyGenerated
Countable generation of 𝓝 x passes to the separated completion.