Theorems · Theorem · general topology

EReal.liminf_add_le

∀ {α : 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

Defined in

Mathlib.Topology.Instances.EReal.Lemmas

Cited by

2 results in Mathlib

Foundations

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