English
Shifting by a constant on the left side adds the constant to the limsup: limsup (c + f_i) = c + limsup f_i.
Русский
Смещение слева константой добавляет ту же константу к limsup.
LaTeX
$$$\mathrm{limsup}\ (c + f_i) = c + \mathrm{limsup}\ f_i.$$$
Lean4
/-- `limsup (xᵢ + c) = (limsup xᵢ) + c`. -/
theorem limsup_add_const (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R] [AddRightMono R] (f : ι → R) (c : R)
(bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
Filter.limsup (fun i ↦ f i + c) F = Filter.limsup f F + c :=
(Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x + c) (fun _ _ h ↦ add_le_add_right h c)
(continuous_add_right c).continuousAt bdd_above cobdd).symm
