trim_le_trim_iff — Mathlib

English

For outer measures m1,m2, m1.trim ≤ m2.trim iff ∀ measurable s, m1 s ≤ m2 s.

Русский

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

LaTeX

$$$m_1.\\text{trim} \\le m_2.\\text{trim} \\iff \\forall s, \\ MeasurableSet(s) \\to m_1 s \\le m_2 s$$$

Lean4

theorem trim_le_trim_iff {m₁ m₂ : OuterMeasure α} : m₁.trim ≤ m₂.trim ↔ ∀ s, MeasurableSet s → m₁ s ≤ m₂ s :=
  le_trim_iff.trans <| forall₂_congr fun s hs => by rw [trim_eq _ hs]

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