card_pi — Mathlib

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]

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