Theorems · Theorem · combinatorics

Finset.sym_filterNe_mem

∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] {n : ℕ} {m : Sym α n} (a : α),
  m ∈ s.sym n → (Sym.filterNe a m).snd ∈ (s.erase a).sym (n - ↑(Sym.filterNe a m).fst)

Defined in

Mathlib.Data.Finset.Sym

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEq