sym_inter — Mathlib

English

The nth symmetric power distributes over intersection: the nth symmetric power of s ∩ t is equal to the intersection of the nth symmetric powers.

Русский

Симметрическая мощность n-го порядка сохраняет пересечение: (s ∩ t)^{(n)} = s^{(n)} ∩ t^{(n)}.

LaTeX

$$$ (s \\cap t)^{(n)} = s^{(n)} \\cap t^{(n)} $$$

Lean4

@[simp]
theorem sym_inter (s t : Finset α) (n : ℕ) : (s ∩ t).sym n = s.sym n ∩ t.sym n :=
  by
  ext m
  simp only [mem_inter, mem_sym_iff, imp_and, forall_and]

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