card_sigma — Mathlib

English

If α is finite and each β(a) is finite, then Nat.card (Sigma β) = ∑ a, Nat.card (β(a)).

Русский

Если α конечно, и каждая β(a) конечно, то Nat.card(Sigma β) = сумма по a Nat.card(β(a)).

LaTeX

$$$$ Nat.card(\Sigma \beta) = \sum_{a} Nat.card(\beta(a)) $$$$

Lean4

theorem card_sigma {β : α → Type*} [Fintype α] [∀ a, Finite (β a)] : Nat.card (Sigma β) = ∑ a, Nat.card (β a) :=
  by
  letI _ (a : α) : Fintype (β a) := Fintype.ofFinite (β a)
  simp_rw [Nat.card_eq_fintype_card, Fintype.card_sigma]

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