English
For finite families s i and i ∈ univ, the number of functions f with f i = a is the product over j ≠ i of card(s j).
Русский
Количество функций f с условием f i = a равно произведению по j ≠ i от card(s j).
LaTeX
$$$\\#\\{ f \\in \\pi\\mathrm{Finset}\\, s \\mid f(i)=a \\} = \\prod_{j \\in \\mathrm{univ}\\setminus \\{i\\}} \\#(s(j))$$$
Lean4
/-- The number of dependent maps `f : Π j, s j` for which the `i` component is `a` is the product
over all `j ≠ i` of `#(s j)`.
Note that this is just a composition of easier lemmas, but there's some glue missing to make that
smooth enough not to need this lemma. -/
theorem card_filter_piFinset_eq_of_mem [∀ i, DecidableEq (α i)] (s : ∀ i, Finset (α i)) (i : ι) {a : α i}
(ha : a ∈ s i) : #({f ∈ piFinset s | f i = a}) = ∏ j ∈ univ.erase i, #(s j) := by
calc
_ = ∏ j, #(Function.update s i { a } j) := by
rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]
_ = ∏ j, Function.update (fun j ↦ #(s j)) i 1 j :=
(Fintype.prod_congr _ _ fun j ↦ by obtain rfl | hji := eq_or_ne j i <;> simp [*])
_ = _ := by simp [prod_update_of_mem, erase_eq]
