addContent_union_le — Mathlib

English

For s,t ∈ C, m(s ∪ t) ≤ m(s) + m(t).

Русский

Для s,t ∈ C верно m(s ∪ t) ≤ m(s) + m(t).

LaTeX

$$m(s ∪ t) ≤ m(s) + m(t)$$

Lean4

theorem addContent_union_le (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : m (s ∪ t) ≤ m s + m t :=
  by
  rw [← union_diff_self, addContent_union hC hs (hC.diff_mem ht hs)]
  · exact add_le_add le_rfl (addContent_mono hC.isSetSemiring (hC.diff_mem ht hs) ht diff_subset)
  · rw [Set.disjoint_iff_inter_eq_empty, inter_diff_self]

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