card_Iic — Mathlib

English

The cardinality of Iic f is the product over i in supp f of the cardinalities of Iic(f(i)).

Русский

Кардинал(Iic f) равен произведению кардиналов Iic(f(i)) по i из supp f.

LaTeX

$$$\\#(Iic f) = \\prod_{i \\in \\operatorname{supp} f} \\#(Iic(f(i)))$$$

Lean4

theorem card_Iic : #(Iic f) = ∏ i ∈ f.support, #(Iic (f i)) := by
  classical simp_rw [Iic_eq_Icc, card_Icc, Finsupp.bot_eq_zero, support_zero, empty_union, zero_apply, bot_eq_zero]

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