English
Adding a constant on the left shifts the liminf by the same amount: liminf (c + f_i) = c + liminf f_i.
Русский
Смещение слева константой добавляет ту же константу к liminf.
LaTeX
$$$\mathrm{liminf}\ (c + f_i) = c + \mathrm{liminf}\ f_i.$$$
Lean4
/-- `liminf (c + xᵢ) = c + liminf xᵢ`. -/
theorem liminf_const_add (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R] [AddLeftMono R] (f : ι → R) (c : R)
(cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
Filter.liminf (fun i ↦ c + f i) F = c + Filter.liminf f F :=
(Monotone.map_limsInf_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 cobdd bdd_below).symm
