card_filter_piFinset_eq — Mathlib

English

For a, i, with a ∈ s i, the filtered cardinality equals the product over j ∈ univ.erase i of card(s j); otherwise 0.

Русский

Если a ∈ s i, то кардинальность фильтра равна произведению по j ∈ univ.erase i от card(s j); иначе 0.

LaTeX

$$$#({f ∈ πFinset s : f i = a}) = \\begin{cases} \\prod_{j \\in \\mathrm{univ}.erase(i)} #(s j), & a \\in s i \\\\\\\\ 0, & \\text{иначе} \\end{cases}$$$

Lean4

theorem card_filter_piFinset_eq [∀ i, DecidableEq (α i)] (s : ∀ i, Finset (α i)) (i : ι) (a : α i) :
    #({f ∈ piFinset s | f i = a}) = if a ∈ s i then ∏ b ∈ univ.erase i, #(s b) else 0 :=
  by
  split_ifs with h
  · rw [card_filter_piFinset_eq_of_mem _ _ h]
  · rw [filter_piFinset_of_notMem _ _ _ h, Finset.card_empty]

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