mathlib documentation

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