disjUnion_comm — Mathlib

English

Swapping the order in disjUnion yields the same result up to symmetry: disjUnion s t h = disjUnion t s h.symm.

Русский

Поменяв порядок в disjUnion, получаем то же множество; равенство держится при симметрии.

LaTeX

$$$\\operatorname{disjUnion}(s,t,h) = \\operatorname{disjUnion}(t,s,h^{\\mathrm{symm}})$$$

Lean4

theorem disjUnion_comm (s t : Finset α) (h : Disjoint s t) : disjUnion s t h = disjUnion t s h.symm :=
  eq_of_veq <| Multiset.add_comm _ _

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