Theorems · Theorem · general topology

ENNReal.limsup_toReal_eq

∀ {ι : Type u_4} {f : Filter ι} {u : ι → ENNReal} [f.NeBot] {b : ENNReal},
  b ≠ ⊤ → (∀ᶠ (i : ι) in f, u i ≤ b) → Filter.limsup (fun i => (u i).toReal) f = (Filter.limsup u f).toReal

If u : ι → ℝ≥0∞ is bounded, then we have liminf (toReal ∘ u) = toReal (liminf u).

Defined in

Mathlib.Topology.Instances.ENNReal.Lemmas

Cited by

0 results in Mathlib

Foundations

Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Filter.NeBot