… for locally compact T2 space (#12266)

add variations of `PartitionOfUnity` and Urysohn's lemma:
- 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`. 
- In a locally compact regular space `X`, for a compact set `t` and a closed set `s` that are disjoint, there is a continuous function `f` with compact support which is `1` on `t` and `0` on `s` and `f x Icc (0 : ℝ) 1 ` for all `x`.

The former is formalized as a partition of unity. For this purpose, I extended `PartialRefiment` to include a predicate `p` about the refined set. With this, we can require that the refined open set has a compact closure. This can be applied when `X` is locally compact and T2.
 
These variations are needed in order to prove that [rieszContentAux](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.html#rieszContentAux) is indeed a Borel measure (following Rudin "Real and complex analysis"), now in #18775.



Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>

…9166)

Two theorems that give equivalent conditions to `a ≤ b` in terms of `ε`-approximation.
- Generalize `a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε` (`le_iff_forall_one_lt_le_mul`) to monoids.
- Add `(hb : 0 ≤ b) : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε` for linearly ordered semifields.

the proofs were suggested by @fpvandoorn in [this thread](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.60le_iff_forall_pos_le_add.60.20for.20.60NNReal.60)

motivation: I will need them in the proof of regularity of `rieszContent`, that will be defined after #18775

Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>

… content is indeed a content for `NNReal` (#18775)

Prove additivity of `RieszContentAux`, completing the proof that it gives a `Content`.

Motivation: this gives the measure related with a positive linear functional `Λ` on compactly supported continuous functions. The next step is to characterise the constructed measure as the one giving `Λ` back.

In this PR, it is assumed to be `NNReal`-linear. The main steps to prove additivity have been proposed by @kkytola [here](#12290 (comment)). A different approach is taken in #12290 for `Real`-linear `Λ`.

- [x] depends on: #12266 for a variation of `PartitionOfUnity`. The new contents of this PR are contained in `MeasureTheory.Integral.linearRieszMarkovKakutani` and `Topology.ContinuousMap.CompactlySupported`.


Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>