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