feat(Topology/UrysohnsLemma): add variations of Urysohn's lemma

[yoh-tanimoto]

add variations of Urysohn's lemma:

• In a normal space X, for a closed set t and an 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.
• In a locally compact T2 space X, for a compact set t and a finite family of open sets {s i} such that t ⊆ ⋃ i, s i, there is a family of continuous function {f i} supported in s i, ∑ i, f i x = 1 on t and 0 ≤ f x ≤ 1.

These variations are needed in order to prove that rieszContentAux is indeed a Borel measure (following Rudin "Real and complex analysis").

---

• [x] depends on: #12459

The part using prod_mem is suggested by @eric-wieser.