card_filter_piFinset_const — Mathlib

English

For finite s, i, j, the filtered cardinality equals either |s|^{|ι|-1} if j ∈ s else 0.

Русский

Для конечного s, i, j кардинальность фильтра равна |s|^{|ι|-1} если j ∈ s, иначе 0.

LaTeX

$$$#({f ∈ πFinset (\\mapsto s) : f i = j}) = \\begin{cases} |s|^{(card ι) - 1}, & j \\in s \\\\\\\\ 0, & \\text{иначе} \\end{cases}$$$

Lean4

theorem card_filter_piFinset_const (s : Finset κ) (i : ι) (j : κ) :
    #({f ∈ piFinset fun _ ↦ s | f i = j}) = if j ∈ s then #s ^ (card ι - 1) else 0 :=
  (card_filter_piFinset_eq _ _ _).trans <| by rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

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