# Order properties of extended non-negative reals #

This file compiles filter-related results about ℝ≥0∞ (see Data/Real/ENNReal.lean).

theorem ENNReal.eventually_le_limsup {α : Type u_1} {f : } (u : αENNReal) :
∀ᶠ (y : α) in f, u y
theorem ENNReal.limsup_eq_zero_iff {α : Type u_1} {f : } {u : αENNReal} :
= 0 f.EventuallyEq u 0
theorem ENNReal.limsup_const_mul_of_ne_top {α : Type u_1} {f : } {u : αENNReal} {a : ENNReal} (ha_top : a ) :
Filter.limsup (fun (x : α) => a * u x) f = a *
theorem ENNReal.limsup_const_mul {α : Type u_1} {f : } {u : αENNReal} {a : ENNReal} :
Filter.limsup (fun (x : α) => a * u x) f = a *
theorem ENNReal.limsup_mul_le {α : Type u_1} {f : } (u : αENNReal) (v : αENNReal) :
Filter.limsup (u * v) f *
theorem ENNReal.limsup_add_le {α : Type u_1} {f : } (u : αENNReal) (v : αENNReal) :
Filter.limsup (u + v) f +
theorem ENNReal.limsup_liminf_le_liminf_limsup {α : Type u_1} {β : Type u_2} [] {f : } {g : } (u : αβENNReal) :
Filter.limsup (fun (a : α) => Filter.liminf (fun (b : β) => u a b) g) f Filter.liminf (fun (b : β) => Filter.limsup (fun (a : α) => u a b) f) g