card_Ico — Mathlib

English

The cardinality of Ico f g equals the product of Icc cards minus 1, over the union of supports.

Русский

Кардинал Ico f g равен произведению кардиналов Icc по всем i из объединения поддержек, минус 1.

LaTeX

$$card_Ico : #(Ico f g) = (\prod i ∈ f.support ∪ g.support, #(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]

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