union_add_inter — Mathlib

English

Let s, t be multisets. Then s ∪ t + s ∩ t = s + t.

Русский

Пусть s, t — мультимножества. Тогда s ∪ t + s ∩ t = s + t.

LaTeX

$$$ s \\cup t + s \\cap t = s + t $$$

Lean4

theorem union_add_inter (s t : Multiset α) : s ∪ t + s ∩ t = s + t :=
  by
  apply _root_.le_antisymm
  · rw [union_add_distrib]
    refine union_le (Multiset.add_le_add_left inter_le_right) ?_
    rw [Multiset.add_comm]
    exact Multiset.add_le_add_right inter_le_left
  · rw [Multiset.add_comm, add_inter_distrib]
    refine le_inter (Multiset.add_le_add_right le_union_right) ?_
    rw [Multiset.add_comm]
    exact Multiset.add_le_add_right le_union_left

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