Commit 2025-12-05 13:19 d2fb7e03

View on Github →

feat: generalize urysohns lemma (#32337) Generalize some of the theorems in the Urysohn's lemma file.

Estimated changes

Modified Mathlib/Topology/UrysohnsLemma.lean

modified theorem exists_continuousMap_one_of_isCompact_subset_isOpen

modified theorem exists_tsupport_one_of_isOpen_isClosed