English
mkMetric' m is defined as the supremum of μ r where μ r is the maximal outer measure with μ r(s) ≤ m(s) for all s, and the supremum yields a measure.
Русский
mkMetric' m определяется как супремум по μ r, где μ r — максимальная внешняя мера с μ r(s) ≤ m(s) для всех s; переход к мере даёт карнатаевскую меру.
LaTeX
$$$ mkMetric' (m) = (OuterMeasure.mkMetric' (m)).toMeasure (OuterMeasure.mkMetric'_isMetric _).le_caratheodory $$$
Lean4
/-- Given a function `m : Set X → ℝ≥0∞`, `mkMetric' m` is the supremum of `μ r`
over `r > 0`, where `μ r` is the maximal outer measure `μ` such that `μ s ≤ m s`
for all `s`. While each `μ r` is an *outer* measure, the supremum is a measure. -/
def mkMetric' (m : Set X → ℝ≥0∞) : Measure X :=
(OuterMeasure.mkMetric' m).toMeasure (OuterMeasure.mkMetric'_isMetric _).le_caratheodory
