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