union_val_nd — Mathlib

English

Let S and T be finite sets. The underlying multiset of their union equals the nondistinct union of their underlying multisets: (S ∪ T).1 = ndunion S.1 T.1.

Русский

Пусть S и T — конечные множества. Очередная мультисета объединения равна ndunion оригинальных мультисетов: (S ∪ T).1 = ndunion(S.1, T.1).

LaTeX

$$$ (s \cup t).1 = ndunion\,s.1\,t.1 $$$

Lean4

theorem union_val_nd (s t : Finset α) : (s ∪ t).1 = ndunion s.1 t.1 :=
  rfl

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