addContent_diff_of_ne_top — Mathlib

English

If s,t ∈ C, m(s) ≠ ∞, m(t) ≠ ∞ and t ⊆ s, then m(s \ t) = m(s) − m(t).

Русский

Если s,t ∈ C, m(s) и m(t) конечны и t ⊆ s, то m(s \ t) = m(s) − m(t).

LaTeX

$$m(s \ t) = m(s) - m(t)$$

Lean4

theorem addContent_diff_of_ne_top (m : AddContent C) (hC : IsSetRing C) (hm_ne_top : ∀ s ∈ C, m s ≠ ∞) {s t : Set α}
    (hs : s ∈ C) (ht : t ∈ C) (hts : t ⊆ s) : m (s \ t) = m s - m t :=
  by
  have h_union : m (t ∪ s \ t) = m t + m (s \ t) := addContent_union hC ht (hC.diff_mem hs ht) disjoint_sdiff_self_right
  simp_rw [Set.union_diff_self, Set.union_eq_right.mpr hts] at h_union
  rw [h_union, ENNReal.add_sub_cancel_left (hm_ne_top _ ht)]

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