Commit 2025-04-21 11:07 71121dc6

feat: modify Urysohn's lemma to let P depend on U (#24179) Modifies Urysohn's lemma to let P, the additional property satisfied by the closed set, to also depend on the open set. This is needed for #24096, where it is used to prove that uniform spaces are completely regular, and P says that some entourage in the uniformity, when composed with the closed set on both sides, is smaller than the open set.