sym_union — Mathlib

English

The nth symmetric power of the union contains the union of the nth symmetric powers: s^{(n)} ∪ t^{(n)} ⊆ (s ∪ t)^{(n)}.

Русский

Объединение симметрических мощностей удовлетворяет включению: s^{(n)} ∪ t^{(n)} ⊆ (s ∪ t)^{(n)}.

LaTeX

$$$ s^{(n)} \\cup t^{(n)} \\subseteq (s \\cup t)^{(n)} $$$

Lean4

@[simp]
theorem sym_union (s t : Finset α) (n : ℕ) : s.sym n ∪ t.sym n ⊆ (s ∪ t).sym n :=
  union_subset (sym_mono subset_union_left n) (sym_mono subset_union_right n)

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