Theorem LightProfinite.continuous_iff_convergent

Modification history

2024-07-12 13:34
Mathlib/Topology/Category/LightProfinite/Sequence.lean
feat(LightProfinite): define `ℕ∪{∞}` as a light profinite set (#13358) …
Added LightProfinite.continuous_iff_convergentView on Github →