card_filter_piFinset_const_eq_of_mem

English

For finite s, index i, j ∈ κ, the filtered cardinality equals |s|^{|ι|-1}.

Русский

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

LaTeX

$$$#\\{f ∈ πFinset(\\!\\mapsto s) : f(i)=j\\} = #s^{(card ι) - 1}$$$

Lean4

theorem card_filter_piFinset_const_eq_of_mem (s : Finset κ) (i : ι) {x : κ} (hx : x ∈ s) :
    #({f ∈ piFinset fun _ ↦ s | f i = x}) = #s ^ (card ι - 1) :=
  (card_filter_piFinset_eq_of_mem _ _ hx).trans <| by rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

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