card_Ioo — Mathlib

English

The cardinality of Ioo f g equals the product of per-coordinate Icc cards minus 2, for i in supp f ∪ supp g.

Русский

Кардинал(Ioo f g) равен произведению кардиналов Icc(f(i), g(i)) минус 2 по координатам.

LaTeX

$$$\\#(Ioo f g) = \\prod_{i \\in \\operatorname{supp} f \\cup \\operatorname{supp} g} \\#(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]

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