English
If f_i is a family of cardinals bounded above, then (sup_i f_i) + c = sup_i (f_i + c) for any cardinal c.
Русский
Если f_i — семейство кардиналов, ограниченное сверху, то для любого кардинала c выполняется (sup_i f_i) + c = sup_i (f_i + c).
LaTeX
$$$\text{BddAbove}(\mathrm{range}(f)) \Rightarrow \forall c\,\bigl( (\sup_i f_i) + c = \sup_i (f_i + c) \bigr)$$$
Lean4
protected theorem ciSup_add (hf : BddAbove (range f)) (c : Cardinal.{v}) : (⨆ i, f i) + c = ⨆ i, f i + c :=
by
have : ∀ i, f i + c ≤ (⨆ i, f i) + c := fun i ↦ add_le_add_right (le_ciSup hf i) c
refine le_antisymm ?_ (ciSup_le' this)
have bdd : BddAbove (range (f · + c)) := ⟨_, forall_mem_range.mpr this⟩
obtain hs | hs := lt_or_ge (⨆ i, f i) ℵ₀
· obtain ⟨i, hi⟩ := exists_eq_of_iSup_eq_of_not_isSuccLimit f hf (not_isSuccLimit_of_lt_aleph0 hs) rfl
exact hi ▸ le_ciSup bdd i
rw [add_eq_max hs, max_le_iff]
exact
⟨ciSup_mono bdd fun i ↦ self_le_add_right _ c, (self_le_add_left _ _).trans (le_ciSup bdd <| Classical.arbitrary ι)⟩
