trim_eq_iInf — Mathlib

English

The trim of s equals the infimum of m t over all measurable t containing s.

Русский

Обрезка множества s равна наименьшему значению m t по всем измеримым t, содержащим s.

LaTeX

$$$$ m^{\mathrm{trim}}(s) = \inf_{t \;:\; s \subseteq t,\ MeasurableSet(t)} m(t). $$$$

Lean4

theorem trim_eq_iInf (s : Set α) : m.trim s = ⨅ (t) (_ : s ⊆ t) (_ : MeasurableSet t), m t :=
  by
  simp +singlePass only [iInf_comm]
  exact
    inducedOuterMeasure_eq_iInf MeasurableSet.iUnion (fun f _ => measure_iUnion_le f) (fun _ _ _ _ h => measure_mono h)
      s

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