card_uIcc — Mathlib

English

The cardinal of the product's uIcc equals the product of the coordinatewise uIcc cards: #(uIcc a b) = ∏ i #(uIcc(a i)(b i)).

Русский

Кардинал uIcc произведения равен произведению координатно-векторных кардиналов uIcc: #(uIcc a b) = ∏ i #(uIcc(a_i, b_i)).

LaTeX

$$$$ #(uIcc(a,b)) = \\prod_{i} #(uIcc(a_i, b_i)) $$$$

Lean4

theorem card_uIcc : #(uIcc a b) = ∏ i, #(uIcc (a i) (b i)) :=
  card_Icc _ _

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