trim_eq — Mathlib

English

For measurable s, trim does not change the value: m.trim(s) = m(s).

Русский

Для измеримого s обрезка не изменяет значение: m.trim(s) = m(s).

LaTeX

$$$$ \forall s\ (MeasurableSet(s) \Rightarrow m^{\mathrm{trim}}(s) = m(s)). $$$$

Lean4

@[simp]
theorem trim_eq {s : Set α} (hs : MeasurableSet s) : m.trim s = m s :=
  inducedOuterMeasure_eq' MeasurableSet.iUnion (fun f _hf => measure_iUnion_le f) (fun _ _ _ _ h => measure_mono h) hs

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