mkMetric — Mathlib

English

The outer measure corresponding to mkMetric' m is the trimmed version of OuterMeasure.mkMetric' m.

Русский

Внешняя мера, соответствующая mkMetric' m, равна усечённой мере OuterMeasure.mkMetric' m.

LaTeX

$$$ (mkMetric' m).toOuterMeasure = (OuterMeasure.mkMetric' m).trim $$$

Lean4

/-- Given a function `m : ℝ≥0∞ → ℝ≥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 sets `s` that contain at least
two points. While each `mkMetric'.pre` is an *outer* measure, the supremum is a measure. -/
def mkMetric (m : ℝ≥0∞ → ℝ≥0∞) : Measure X :=
  (OuterMeasure.mkMetric m).toMeasure (OuterMeasure.mkMetric'_isMetric _).le_caratheodory

Похожие утверждения