mkMetric_toOuterMeasure — Mathlib

English

The mkMetric construction on measures corresponds to taking the outer measure mkMetric m as a measure via toOuterMeasure.

Русский

Конструкция mkMetric при работе с мерами соответствует внешней мере mkMetric m через toOuterMeasure.

LaTeX

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

Lean4

@[simp]
theorem mkMetric_toOuterMeasure (m : ℝ≥0∞ → ℝ≥0∞) : (mkMetric m : Measure X).toOuterMeasure = OuterMeasure.mkMetric m :=
  OuterMeasure.trim_mkMetric m

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