limsup_add_le_of_le — 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 $$$

Lean4

theorem limsup_add_le_of_le {a b : EReal} (ha : limsup u f < a) (hb : limsup v f ≤ b) : limsup (u + v) f ≤ a + b :=
  by
  rcases eq_top_or_lt_top b with rfl | h
  · rw [add_top_of_ne_bot ha.ne_bot]; exact le_top
  · exact (limsup_add_le (.inr (hb.trans_lt h).ne) (.inl ha.ne_top)).trans (add_le_add ha.le hb)

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