Theorems · Definition · combinatorics

Finset.symInsertEquiv

{α : Type u_1} →
  {s : Finset α} →
    {a : α} → [inst : DecidableEq α] → {n : ℕ} → a ∉ s → ↥((insert a s).sym n) ≃ (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))

If a does not belong to the finset s, then the nth symmetric power of {a} ∪ s is in 1-1 correspondence with the disjoint union of the n - ith symmetric powers of s, for 0 ≤ i ≤ n.

Defined in

Mathlib.Data.Finset.Sym

Cited by

6 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq