inter_add_distrib — Mathlib

English

Let s, t, u be multisets. Then (s ∩ t) + u = (s + u) ∩ (t + u).

Русский

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

LaTeX

$$$ (s \\cap t) + u = (s + u) \\cap (t + u) $$$

Lean4

theorem inter_add_distrib (s t u : Multiset α) : s ∩ t + u = (s + u) ∩ (t + u) :=
  by
  by_contra! h
  obtain ⟨a, ha⟩ :=
    lt_iff_cons_le.1 <|
      h.lt_of_le <| le_inter (Multiset.add_le_add_right inter_le_left) (Multiset.add_le_add_right inter_le_right)
  rw [← cons_add] at ha
  exact
    (lt_cons_self (s ∩ t) a).not_ge <|
      le_inter (Multiset.le_of_add_le_add_right (ha.trans inter_le_left))
        (Multiset.le_of_add_le_add_right (ha.trans inter_le_right))

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