card_Ioc — Mathlib

English

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

Русский

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

LaTeX

$$$\\#(Ioc f g) = \\prod_{i \\in \\operatorname{supp} f \\cup \\operatorname{supp} g} \\#(Icc(f(i), g(i))) - 1$$$

Lean4

theorem card_Ioc : #(Ioc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1 := by
  rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]

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