English
The cardinality of f.pi equals the product of the cardinalities of f(i) over all i.
Русский
Кардинал f.pi равен произведению кардиналов f(i) по всем i.
LaTeX
$$card_pi (f : Π₀ i, Finset (α i)) : #f.pi = (f.prod fun i => #(f i))$$
Lean4
@[simp]
theorem card_pi (f : Π₀ i, Finset (α i)) : #f.pi = f.prod fun i ↦ #(f i) :=
by
rw [pi, card_dfinsupp]
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id]