card_pi — Mathlib

English

For f : ι →₀ Finset α, the cardinality of f.pi equals the product of the cardinalities of f(i) over i.

Русский

Для f : ι →₀ Finset α, кардинал f.pi равен произведению кардиналов f(i).

LaTeX

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

Lean4

@[simp]
theorem card_pi (f : ι →₀ Finset α) : #f.pi = f.prod fun i ↦ #(f i) :=
  by
  rw [pi, card_finsupp]
  exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id]

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