Theorem exists_continuous_one_zero_of_isCompact

Modification history

2023-11-07 10:06
Mathlib/Topology/UrysohnsLemma.lean
feat: Urysohn lemma in regular locally compact spaces (#8124) …
Added exists_continuous_one_zero_of_isCompactView on Github →