extend_mono — Mathlib

English

If s1 ⊆ s2 and s1 is measurable, then the extension is monotone: extend m s1 ≤ extend m s2.

Русский

Если s1 ⊆ s2 и s1 измеримо, то расширение монотонно: extend m s1 ≤ extend m s2.

LaTeX

$$$\\text{MeasurableSet}(s_1) \\land s_1 \\subseteq s_2 \\Rightarrow \\mathrm{extend}\\ m\\ s_1 \\le \\mathrm{extend}\\ m\\ s_2$$$

Lean4

theorem extend_mono {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (hs : s₁ ⊆ s₂) : extend m s₁ ≤ extend m s₂ :=
  by
  refine le_iInf ?_; intro h₂
  have := extend_union MeasurableSet.empty m0 MeasurableSet.iUnion mU disjoint_sdiff_self_right h₁ (h₂.diff h₁)
  rw [union_diff_cancel hs] at this
  rw [← extend_eq m]
  exact le_iff_exists_add.2 ⟨_, this⟩

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