Theorem LightProfinite.closedEmbedding_natUnionInftyEmbedding

Modification history

2024-10-20 13:29
Mathlib/Topology/Category/LightProfinite/Sequence.lean
chore: Rename `ClosedEmbedding` to `IsClosedEmbedding` (#17937) …
Deleted LightProfinite.closedEmbedding_natUnionInftyEmbeddingView on Github →
2024-07-12 13:34
Mathlib/Topology/Category/LightProfinite/Sequence.lean
feat(LightProfinite): define `ℕ∪{∞}` as a light profinite set (#13358) …
Added LightProfinite.closedEmbedding_natUnionInftyEmbeddingView on Github →