limsup_add_bot_of_ne_top — Mathlib

English

If limsup u f = ⊥ and limsup v f ≠ ⊤, then limsup(u+v) f = ⊥.

Русский

Если limsup u f = ⊥ и limsup v f ≠ ⊤, то limsup(u+v) f = ⊥.

LaTeX

$$$ \text{limsup}(u+v) f = ⊥ \quad\text{when } \text{limsup }u f = ⊥ \text{ and } \text{limsup }v f \neq ⊤ $$$

Lean4

theorem limsup_add_bot_of_ne_top (h : limsup u f = ⊥) (h' : limsup v f ≠ ⊤) : limsup (u + v) f = ⊥ :=
  by
  apply le_bot_iff.1 ((limsup_add_le (.inr h') _).trans _)
  · rw [h]; exact .inl bot_ne_top
  · rw [h, bot_add]

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