trim_mkMetric — Mathlib

English

For mkMetric m, trimming yields the same outer measure: (mkMetric m).trim = mkMetric m.

Русский

Усечение mkMetric m не меняет внешнюю меру: (mkMetric m).trim = mkMetric m.

LaTeX

$$$ (mkMetric m).trim = mkMetric m $$$

Lean4

theorem trim_mkMetric [MeasurableSpace X] [BorelSpace X] (m : ℝ≥0∞ → ℝ≥0∞) :
    (mkMetric m : OuterMeasure X).trim = mkMetric m :=
  by
  simp only [mkMetric, mkMetric'.eq_iSup_nat, trim_iSup]
  congr 1 with n : 1
  refine mkMetric'.trim_pre _ (fun s => ?_) _
  simp

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