English
Subtraction of a constant from every term shifts the liminf to the left by that constant: liminf (f_i - c) = liminf f_i - c.
Русский
Вычитание константы из каждого элемента сдвигает liminf влево на ту константу.
LaTeX
$$$\mathrm{liminf}\ (f_i - c) = \mathrm{liminf}\ f_i - c.$$$
Lean4
/-- `liminf (c - xᵢ) = c - limsup xᵢ`. -/
theorem liminf_const_sub (F : Filter ι) [NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R]
[AddLeftMono R] (f : ι → R) (c : R) (bdd_above : F.IsBoundedUnder (· ≤ ·) f)
(cobdd : F.IsCoboundedUnder (· ≤ ·) f) : Filter.liminf (fun i ↦ c - f i) F = c - Filter.limsup f F :=
(Antitone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c - x) (fun _ _ h ↦ tsub_le_tsub_left h c)
(continuous_sub_left c).continuousAt bdd_above cobdd).symm
