inter_add_sub_of_add_eq_add — Mathlib

English

If M + N = P + Q for multisets, then (N ∩ Q) + (P - M) = N.

Русский

Если выполняется M + N = P + Q для мультимножств, то (N ∩ Q) + (P - M) = N.

LaTeX

$$$ (N \\cap Q) + (P - M) = N $$$

Lean4

theorem inter_add_sub_of_add_eq_add [DecidableEq α] {M N P Q : Multiset α} (h : M + N = P + Q) :
    (N ∩ Q) + (P - M) = N := by
  ext x
  rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]
  have h0 : M.count x + N.count x = P.count x + Q.count x :=
    by
    rw [Multiset.ext] at h
    simp_all only [Multiset.count_add]
  omega

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