card_finsupp — Mathlib

English

For a finitely supported function f : ι → Finset α, the cardinality of f.pi equals the product of the cardinalities of f(i) over i ∈ s.

Русский

Для функции f : ι → Finset α с конечной опорой справедливо: |f.pi| = ∏_{i ∈ ι} |f(i)|.

LaTeX

$$$|f.pi| = \\prod_{i} |f(i)|$$$

Lean4

@[simp]
theorem card_finsupp (s : Finset ι) (t : ι → Finset α) : #(s.finsupp t) = ∏ i ∈ s, #(t i) := by
  classical exact (card_map _).trans <| card_pi _ _

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