Theorem exists_tsupport_one_of_isOpen_isClosed

Modification history

2024-08-26 13:16
Mathlib/Topology/UrysohnsLemma.lean
feat(Topology/UrysohnsLemma): add a variation of Urysohn's lemma for T2Space (#12459) …
Added exists_tsupport_one_of_isOpen_isClosedView on Github →