Countable generation of 𝓝 0 passes to the separated completion #
The zero-point form of UniformSpace.Completion.isCountablyGenerated_nhds_coe, registered as an
instance. Only a zero and a uniformity are needed; no group structure, no separation, no
completeness.
It exists because results in the Huber development carry [(𝓝 (0 : A)).IsCountablyGenerated] and
are applied with A a completion — in particular to A⟨X₁,…,Xₖ⟩, the completion of the
restricted-series subring, where
TauCeti.Huber.isCountablyGenerated_nhds_zero_weightedRestrictedSubring supplies the property
downstairs and this carries it up.
Main results #
Countable generation of 𝓝 0 passes to the separated completion.
An instance rather than a theorem because it is consumed by typeclass resolution, whereas the general statement it specialises is about an arbitrary point and cannot be.