trim_congr — Mathlib

English

If two outer measures agree on every measurable set, their trims are equal.

Русский

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

LaTeX

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

Lean4

theorem trim_congr {m₁ m₂ : OuterMeasure α} (H : ∀ {s : Set α}, MeasurableSet s → m₁ s = m₂ s) : m₁.trim = m₂.trim := by
  simp +contextual only [trim, H]

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