card_Icc — Mathlib

English

The cardinality of Icc f g equals the product, over i in supp f ∪ supp g, of the cardinalities of Icc(f(i), g(i)).

Русский

Кардинал(Icc f g) равен произведению по i из supp f ∪ supp g от кардинала Icc(f(i), g(i)).

LaTeX

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

Lean4

theorem card_Icc : #(Icc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) := by
  simp_rw [Icc_eq, card_finsupp, coe_rangeIcc]

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