ciSup_mul_ciSup — Mathlib

English

For f:I→Cardinal and g:J→Cardinal, (sup_i f_i) × (sup_j g_j) = sup_{i} sup_{j} (f_i × g_j).

Русский

Для двух семейств f_i и g_j кардиналов, индексов I и J, выполняется (sup_i f_i) × (sup_j g_j) = sup_i sup_j (f_i × g_j).

LaTeX

$$$\bigl(\sup_i f_i\bigr) \times \bigl(\sup_j g_j\bigr) = \sup_{i} \sup_{j} (f_i \times g_j)$$$

Lean4

protected theorem ciSup_mul_ciSup (g : ι' → Cardinal.{v}) : (⨆ i, f i) * (⨆ j, g j) = ⨆ (i) (j), f i * g j := by
  simp_rw [Cardinal.ciSup_mul f, Cardinal.mul_ciSup g]

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