le_addContent_diff — Mathlib

English

For m on a set ring, m(s) − m(t) ≤ m(s \ t).

Русский

Для множества s, t в кольце множеств неравенство m(s) − m(t) ≤ m(s \ t).

LaTeX

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

Lean4

theorem le_addContent_diff (m : AddContent C) (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : m s - m t ≤ m (s \ t) :=
  by
  conv_lhs => rw [← inter_union_diff s t]
  rw [addContent_union hC (hC.inter_mem hs ht) (hC.diff_mem hs ht) disjoint_inf_sdiff, add_comm]
  refine add_tsub_le_assoc.trans_eq ?_
  rw [tsub_eq_zero_of_le (addContent_mono hC.isSetSemiring (hC.inter_mem hs ht) ht inter_subset_right), add_zero]

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