Commit 2025-10-28 20:18 6c373552

View on Github →

feat(Topology): infinite T2 spaces (#30661)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/NatEmbedding.lean

added theorem exists_infinite_discreteTopology

added theorem exists_seq_infinite_isOpen_pairwise_disjoint

added theorem exists_topology_isEmbedding_nat