liminf_const_sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem liminf_const_sub (F : Filter ι) [NeBot F] (f : ι → ℝ≥0∞) {c : ℝ≥0∞} (c_ne_top : c ≠ ∞) :
    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 : ℝ≥0∞) ↦ c - x) (fun _ _ h ↦ tsub_le_tsub_left h c)
      (continuous_sub_left c_ne_top).continuousAt).symm

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