Documentation

Mathlib.Order.Filter.ENNReal

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 : Filter α} [CountableInterFilter f] (u : αENNReal) :
∀ᶠ (y : α) in f, u y Filter.limsup u f
theorem ENNReal.limsup_eq_zero_iff {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : αENNReal} :
theorem ENNReal.limsup_const_mul_of_ne_top {α : Type u_1} {f : Filter α} {u : αENNReal} {a : ENNReal} (ha_top : a ) :
Filter.limsup (fun (x : α) => a * u x) f = a * Filter.limsup u f
theorem ENNReal.limsup_const_mul {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : αENNReal} {a : ENNReal} :
Filter.limsup (fun (x : α) => a * u x) f = a * Filter.limsup u f
theorem ENNReal.limsup_mul_le {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u : αENNReal) (v : αENNReal) :
theorem ENNReal.limsup_add_le {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u : αENNReal) (v : αENNReal) :
theorem ENNReal.limsup_liminf_le_liminf_limsup {α : Type u_1} {β : Type u_2} [Countable β] {f : Filter α} [CountableInterFilter f] {g : Filter β} (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