card_Ioo — Mathlib

English

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

Русский

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

LaTeX

$$card_Ioo : #(Ioo f g) = (\prod i ∈ f.support ∪ g.support, #(Icc (f i) (g i))) - 2$$

Lean4

theorem card_Ioo : #(Ioo f g) = (∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i))) - 2 := by
  rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]

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