Theorems · Theorem · general topology

EReal.limsup_add_le

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

Defined in

Mathlib.Topology.Instances.EReal.Lemmas

Cited by

4 results in Mathlib

Foundations

Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound