# mathlibdocumentation

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 α} (u : α → ennreal) :
∀ᶠ (y : α) in f, u y f.limsup u
theorem ennreal.limsup_eq_zero_iff {α : Type u_1} {f : filter α} {u : α → ennreal} :
f.limsup u = 0 u =ᶠ[f] 0
theorem ennreal.limsup_const_mul_of_ne_top {α : Type u_1} {f : filter α} {u : α → ennreal} {a : ennreal} (ha_top : a ) :
f.limsup (λ (x : α), a * u x) = a * f.limsup u
theorem ennreal.limsup_const_mul {α : Type u_1} {f : filter α} {u : α → ennreal} {a : ennreal} :
f.limsup (λ (x : α), a * u x) = a * f.limsup u
theorem ennreal.limsup_mul_le {α : Type u_1} {f : filter α} (u v : α → ennreal) :
f.limsup (u * v) f.limsup u * f.limsup v
theorem ennreal.limsup_add_le {α : Type u_1} {f : filter α} (u v : α → ennreal) :
f.limsup (u + v) f.limsup u + f.limsup v
theorem ennreal.limsup_liminf_le_liminf_limsup {α : Type u_1} {β : Type u_2} [countable β] {f : filter α} {g : filter β} (u : α → β → ennreal) :
f.limsup (λ (a : α), g.liminf (λ (b : β), u a b)) g.liminf (λ (b : β), f.limsup (λ (a : α), u a b))