trim_eq_trim_iff — Mathlib

English

Two outer measures have equal trims iff they agree on all measurable sets.

Русский

У двух внешних мер равны обрезки тогда и только тогда, когда они совпадают на всех измеримых множествах.

LaTeX

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

Lean4

theorem trim_eq_trim_iff {m₁ m₂ : OuterMeasure α} : m₁.trim = m₂.trim ↔ ∀ s, MeasurableSet s → m₁ s = m₂ s := by
  simp only [le_antisymm_iff, trim_le_trim_iff, forall_and]

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