card_pi — Mathlib

English

Cardinality of pi m t equals the product of the cardinals of t(a) over a in m.

Русский

Кардинальность pi m t равна произведению кардинальностей t(a) по всем a ∈ m.

LaTeX

$$$\\operatorname{card}(\\pi m t) = \\prod_{a\\in m} \\operatorname{card}(t a).$$$

Lean4

theorem card_pi (m : Multiset α) (t : ∀ a, Multiset (β a)) : card (pi m t) = prod (m.map fun a => card (t a)) :=
  Multiset.induction_on m (by simp) (by simp +contextual)

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