union_add_distrib — Mathlib

English

Another expression of the distributive property: s ∪ t + u = s + u ∪ (t + u).

Русский

Ещё одно выражение дистрибутивности: s ∪ t + u = s + u ∪ (t + u).

LaTeX

$$$\\forall s,t,u \\in \\mathrm{Multiset}(\\alpha),\\ (s \\cup t) + u = s + u \\cup (t + u).$$$

Lean4

theorem union_add_distrib (s t u : Multiset α) : s ∪ t + u = s + u ∪ (t + u) := by
  simpa [(· ∪ ·), union, eq_comm, Multiset.add_assoc, Multiset.add_left_inj] using
    show s + u - (t + u) = s - t by rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right]

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