Theorem SeparatedNhds.of_finite

Modification history

2026-05-17 12:59
Mathlib/Topology/Separation/Hausdorff.lean
feat(Topology): subspace of a perfectly normal space is perfectly normal (#38533) …
Added SeparatedNhds.of_finiteView on Github →