card_Ico — Mathlib

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]

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