add_iSup — Mathlib

English

If ι is nonempty, then (iSup f) + a = iSup (f i + a).

Русский

Если ι ненулевое, то (iSup f) + a = iSup (f i + a).

LaTeX

$$$ (\text{Nonempty } ι) \rightarrow \left( \left( \bigcup_i f_i \right) + a = \bigcup_i (f_i + a) \right) $$$

Lean4

theorem add_iSup [Nonempty ι] (f : ι → ℕ∞) : a + ⨆ i, f i = ⨆ i, a + f i :=
  by
  obtain rfl | ha := eq_or_ne a ⊤
  · simp
  refine le_antisymm ?_ <| iSup_le fun i ↦ add_le_add_left (le_iSup ..) _
  refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_
  exact iSup_le fun i ↦ ENat.le_sub_of_add_le_left ha <| le_iSup (a + f ·) i

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