trim_sup — Mathlib

English

Trim commutes with taking the supremum: (m1 ⊔ m2).trim = m1.trim ⊔ m2.trim.

Русский

Обрезка сохраняет взятие верхнего объединения: (m1 ⊔ m2).trim = m1.trim ⊔ m2.trim.

LaTeX

$$$$ (m_1 \sqcup m_2)^{\mathrm{trim}} = m_1^{\mathrm{trim}} \sqcup m_2^{\mathrm{trim}}. $$$$

Lean4

/-- `trim` sends the supremum of two outer measures to the supremum of the trimmed measures. -/
theorem trim_sup (m₁ m₂ : OuterMeasure α) : (m₁ ⊔ m₂).trim = m₁.trim ⊔ m₂.trim :=
  ext fun s => (trim_binop (sup_apply m₁ m₂) s).trans (sup_apply _ _ _).symm

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