Commit 2024-08-26 13:16 5d1d19d6

feat(Topology/UrysohnsLemma): add a variation of Urysohn's lemma for T2Space (#12459) prove a version of Urysohn's lemma and separation lemmas needed for them.

• In a T2Space X, for a closed set t and a relatively compact open set s such that t ⊆ s, there is a continuous function f supported in s, f x = 1 on t and 0 ≤ f x ≤ 1. Motivation: this will be used in #12290.