card_sections — Mathlib

English

The cardinality of Sections s equals the product of the cardinalities of the elements of s.

Русский

Число секций Sections s равно произведению величин кардиналов элементов s.

LaTeX

$$$$ \\operatorname{card}(\\operatorname{Sections}(s)) = \\prod (s.map \\operatorname{card}). $$$$

Lean4

theorem card_sections {s : Multiset (Multiset α)} : card (Sections s) = prod (s.map card) :=
  Multiset.induction_on s (by simp) (by simp +contextual)

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