ciSup_add_ciSup — Mathlib

English

For a family f_i of cardinals indexed by I and any cardinal c, (sup_i f_i) · c = sup_i (f_i · c).

Русский

Для семейства f_i кардиналов, индексируемого I, и любого кардинала c, выполняется (sup_i f_i) · c = sup_i (f_i · c).

LaTeX

$$$(\sup_i f_i) \cdot c = \sup_i (f_i \cdot c)$$$

Lean4

protected theorem ciSup_add_ciSup (hf : BddAbove (range f)) (g : ι' → Cardinal.{v}) (hg : BddAbove (range g)) :
    (⨆ i, f i) + (⨆ j, g j) = ⨆ (i) (j), f i + g j := by simp_rw [Cardinal.ciSup_add f hf, Cardinal.add_ciSup g hg]

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