card_uIcc — Mathlib

English

The cardinality of uIcc f g equals the product of uIcc cards coordinatewise over the union of supports.

Русский

Кардинал uIcc f g равен произведению кардиналов uIcc по координатам над объединением поддержек.

LaTeX

$$card_uIcc : #(uIcc f g) = ∏ i ∈ f.support ∪ g.support, #(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 _ _

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