English
The cardinality of Ico f g equals the product of per-coordinate Icc cards minus 1, taken over supp f ∪ supp g.
Русский
Кардинал(Ico f g) равен произведению по i из supp f ∪ supp g кардиналов Icc(f(i), g(i)) минус 1.
LaTeX
$$$\\#(Ico f g) = \\prod_{i \\in \\operatorname{supp} f \\cup \\operatorname{supp} g} \\#(Icc(f(i), g(i))) - 1$$$
Lean4
theorem card_Ico : #(Ico f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1 := by
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]