∀ {α : Type u_3} {f : Filter α} {u v : α → EReal},
  Filter.limsup u f ≠ ⊥ ∨ Filter.liminf v f ≠ ⊤ →
    Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ ⊥ → Filter.liminf (u + v) f ≤ Filter.limsup u f + Filter.liminf v f