English
Adding a constant to every term shifts the limsup by the same constant: limsup (f_i + c) = limsup f_i + c.
Русский
Прибавление константы ко всем членам последовательности смещает limsup на ту же константу.
LaTeX
$$$\mathrm{limsup}\ (f_i + c) = \mathrm{limsup}\ f_i + c.$$$
Lean4
/-- `liminf (c + xᵢ) = c + liminf xᵢ`. -/
theorem limsup_const_add (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R] [AddLeftMono R] (f : ι → R) (c : R)
(bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
Filter.limsup (fun i ↦ c + f i) F = c + Filter.limsup f F :=
(Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c + x) (fun _ _ h ↦ add_le_add_left h c)
(continuous_add_left c).continuousAt bdd_above cobdd).symm
