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.

[github-actions[bot]]

PR summary 646d9d61d7

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.UrysohnsLemma	1328	1336	+8 (+0.60%)

Import changes for all files

Files	Import difference
22 files Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Light.Explicit Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Condensed.Discrete.Module Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Limits Mathlib.Condensed.Discrete.Colimit Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.Module Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Condensed.Light.Functors	5
Mathlib.MeasureTheory.Measure.EverywherePos	7
36 files Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Condensed.Limits Mathlib.Condensed.TopComparison Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Condensed.Explicit Mathlib.Condensed.Module Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.CompletelyRegular Mathlib.Condensed.Basic Mathlib.Condensed.Solid Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.CompHaus.Limits Mathlib.Condensed.TopCatAdjunction Mathlib.Topology.UrysohnsLemma Mathlib.Topology.Category.CompactlyGenerated Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.Profinite.Extend Mathlib.Condensed.CartesianClosed Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Locale Mathlib.Order.Category.Frm Mathlib.Condensed.Epi Mathlib.Condensed.Functors Mathlib.Condensed.Equivalence Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.Category.Stonean.Limits	8

---

Declarations diff

+ exists_continuous_sum_one_of_isOpen_isCompact + exists_continuous_zero_one_of_isCompact' + exists_gt_t2space + exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space + exists_isSubordinate_of_locallyFinite_of_prop_t2space + exists_isSubordinate_of_locallyFinite_t2space + exists_subset_iUnion_closure_subset_t2space + exists_subset_iUnion_compact_subset_t2space + toFun_eq_coe

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[j-loreaux]

This PR looks mostly fine, but there are still some places where it needs some work. Are you planning to continue working on this PR? Would you like some help from others, or do you want to hand it over completely? (In the latter case, please label it with please-adopt.)

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#18827~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[jcommelin]

bors d+

[mathlib-bors[bot]]

:v: yoh-tanimoto can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[yoh-tanimoto]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style