card_dfinsupp — Mathlib

English

The cardinality of the finitely supported product dfinsupp (s, t) equals the product of the cardinalities of each t(i) over i ∈ s.

Русский

Кардинал множества dfinsupp(s, t) равен произведению кардиналов множеств t(i) по i∈s.

LaTeX

$$$|s.dfinsupp t| = \prod_{i \in s} |t(i)|$$$

Lean4

@[simp]
theorem card_dfinsupp (s : Finset ι) (t : ∀ i, Finset (α i)) : #(s.dfinsupp t) = ∏ i ∈ s, #(t i) :=
  (card_map _).trans <| card_pi _ _

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