Commit 2024-07-12 13:34 31c0e2a6

View on Github →

feat(LightProfinite): define ℕ∪{∞} as a light profinite set (#13358)

depends on: #13319
depends on: #13355

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/LightProfinite/Sequence.lean

added theorem LightProfinite.closedEmbedding_natUnionInftyEmbedding

added theorem LightProfinite.continuous_iff_convergent

Modified Mathlib/Topology/Metrizable/Basic.lean