sub_add_inter — Mathlib

English

For multisets s, t, s - t + s ∩ t = s.

Русский

Для мультимножеств s, t выполняется s - t + s ∩ t = s.

LaTeX

$$$ s - t + s \\cap t = s $$$

Lean4

theorem sub_add_inter (s t : Multiset α) : s - t + s ∩ t = s :=
  by
  rw [inter_comm]
  revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_
  by_cases h : a ∈ s
  · rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]
  · rw [cons_inter_of_neg _ h, sub_cons, erase_of_notMem h, IH]

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