card_uIcc — Mathlib

English

The cardinality of uIcc f g equals the product of per-coordinate uIcc cards over i in supp f ∪ supp g.

Русский

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

LaTeX

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

Lean4

theorem card_uIcc : #(uIcc f g) = ∏ i ∈ f.support ∪ g.support, #(uIcc (f i) (g i)) := by
  rw [← support_inf_union_support_sup]; exact card_Icc (_ : ι →₀ α) _

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