card_sigma — Mathlib

English

The cardinality of the dependent sum Σ i, α(i) equals the sum over i of the cardinality of α(i).

Русский

Кардинальность зависимого суммирования Σ i, α(i) равна сумме по i кардинальностей α(i).

LaTeX

$$$\\operatorname{card}(\\Sigma i, \\alpha(i)) = \\sum_{i} \\operatorname{card}(\\alpha(i))$$$

Lean4

@[simp]
nonrec theorem card_sigma {ι} {α : ι → Type*} [Fintype ι] [∀ i, Fintype (α i)] : card (Sigma α) = ∑ i, card (α i) :=
  card_sigma _ _

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