mkMetric' — Mathlib

English

An outer measure built from Thickened indicators is a metric outer measure.

Русский

Внешняя мера, построенная из утолщённых индикаторов, является метрической внешней мерой.

LaTeX

$$Theorem mkMetric'_isMetric$$

Lean4

/-- Given a function `m : Set X → ℝ≥0∞`, `mkMetric' m` is the supremum of `mkMetric'.pre m r`
over `r > 0`. Equivalently, it is the limit of `mkMetric'.pre m r` as `r` tends to zero from
the right. -/
def mkMetric' (m : Set X → ℝ≥0∞) : OuterMeasure X :=
  ⨆ r > 0, mkMetric'.pre m r

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