limsup_const_sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem limsup_const_sub (F : Filter ι) (f : ι → ℝ≥0∞) {c : ℝ≥0∞} (c_ne_top : c ≠ ∞) :
    Filter.limsup (fun i ↦ c - f i) F = c - Filter.liminf f F :=
  by
  rcases F.eq_or_neBot with rfl | _
  · simp only [limsup_bot, bot_eq_zero', liminf_bot, le_top, tsub_eq_zero_of_le]
  ·
    exact
      (Antitone.map_limsInf_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

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