Theorem exists_continuousMap_one_of_isCompact_subset_isOpen

Modification history

2025-12-05 13:19
Mathlib/Topology/UrysohnsLemma.lean
feat: generalize urysohns lemma (#32337) …
Modified exists_continuousMap_one_of_isCompact_subset_isOpenView on Github →
2025-11-04 23:41
Mathlib/Topology/UrysohnsLemma.lean
feat: uniqueness of measures in the Riesz–Markov–Kakutani representation theorem (#28061) …
Added exists_continuousMap_one_of_isCompact_subset_isOpenView on Github →