liminf_sub_const — Mathlib

English

For ENNReal sequences, liminf(f_i − c) = liminf f_i − c, provided c ≠ ∞.

Русский

Для ENNReal последовательностей верно liminf(f_i − c) = liminf f_i − c, при условии c ≠ ∞.

LaTeX

$$$\operatorname{liminf}(f_i - c) = \operatorname{liminf} f_i - c$ (при $c \neq \infty$)$$

Lean4

theorem liminf_sub_const (F : Filter ι) [NeBot F] (f : ι → ℝ≥0∞) (c : ℝ≥0∞) :
    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 : ℝ≥0∞) ↦ x - c)
      (fun _ _ h ↦ tsub_le_tsub_right h c) (continuous_sub_right c).continuousAt).symm

Похожие утверждения