mul_ciSup — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem mul_ciSup (c : Cardinal.{v}) : c * (⨆ i, f i) = ⨆ i, c * f i := by
  rw [mul_comm, Cardinal.ciSup_mul f]; simp_rw [mul_comm]

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