le_trim_iff — Mathlib

English

The trim operation can be compared with the original order by testing all measurable sets: m1 ≤ m2.trim if and only if for every measurable s, m1(s) ≤ m2(s).

Русский

Обрезка (trim) сохраняет упорядочение: m1 ≤ m2.trim тогда и только тогда, когда для каждого измеримого s выполняется m1(s) ≤ m2(s).

LaTeX

$$$$ m_1 \le m_2^{\mathrm{trim}} \;\Longleftrightarrow\; \forall s,\ MeasurableSet(s) \Rightarrow m_1(s) \le m_2(s). $$$$

Lean4

theorem le_trim_iff {m₁ m₂ : OuterMeasure α} : m₁ ≤ m₂.trim ↔ ∀ s, MeasurableSet s → m₁ s ≤ m₂ s :=
  le_inducedOuterMeasure

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