English
Adding a constant to every term shifts the liminf by the same constant: liminf (f_i + c) = liminf f_i + c.
Русский
Прибавление константы к каждому члену последовательности сдвигает liminf на ту же константу.
LaTeX
$$$\mathrm{liminf}\ (f_i + c) = \mathrm{liminf}\ f_i + c.$$$
Lean4
/-- `liminf (xᵢ + c) = (liminf xᵢ) + c`. -/
theorem liminf_add_const (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R] [AddRightMono R] (f : ι → R) (c : R)
(cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
Filter.liminf (fun i ↦ f i + c) F = Filter.liminf f F + c :=
(Monotone.map_limsInf_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 cobdd bdd_below).symm
