card_sigma — Mathlib

English

The cardinality of a sigma-type equals the sum of the cardinalities of the fibers: |s.sigma t| = Σ_{a ∈ s} |t(a)|.

Русский

Мощность сигма-типа равна сумме мощностей волокон: |s.sigma t| = ∑_{a ∈ s} |t(a)|.

LaTeX

$$$$\\#(s.\\sigma t) = \\sum_{a \\in s} \\#(t(a)). $$$$

Lean4

@[simp]
theorem card_sigma {σ : α → Type*} (s : Finset α) (t : ∀ a, Finset (σ a)) : #(s.sigma t) = ∑ a ∈ s, #(t a) :=
  Multiset.card_sigma _ _

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