add_eq_union_iff_disjoint — Mathlib

English

Let s,t,u be multisets. Then s + t = s ∪ t iff Disjoint s t.

Русский

Пусть s,t,u — мультисеты. Тогда s + t = s ∪ t эквивале Disjoint s t.

LaTeX

$$$s + t = s \\cup t \\iff Disjoint s t$$$

Lean4

theorem add_eq_union_iff_disjoint [DecidableEq α] {s t : Multiset α} : s + t = s ∪ t ↔ Disjoint s t := by
  simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero, Nat.min_eq_zero_iff,
    Nat.add_eq_max_iff]

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