le_limsup_add — Mathlib

English

If limsup u f < a and limsup v f ≤ b, then limsup (u+v) f ≤ a+b.

Русский

Если limsup u f < a и limsup v f ≤ b, то limsup(u+v) f ≤ a+b.

LaTeX

$$$ (\text{ha}) \,(hb) :\; \limsup (u+v) f ≤ a+b $ where \ ha : \limsup u f < a, \ hb : \limsup v f ≤ b $$$

Lean4

theorem le_limsup_add : (limsup u f) + (liminf v f) ≤ limsup (u + v) f :=
  add_le_of_forall_lt fun _ a_u _ b_v ↦
    (le_limsup_iff).2 fun _ c_ab ↦
      (((frequently_lt_of_lt_limsup) a_u).and_eventually ((eventually_lt_of_lt_liminf) b_v)).mono fun _ ab_x ↦
        c_ab.trans (add_lt_add ab_x.1 ab_x.2)

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