Theorems · Theorem · general topology

ENNReal.exists_upcrossings_of_not_bounded_under

∀ {ι : Type u_4} {l : Filter ι} {x : ι → ℝ},
  Filter.liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤ →
    (¬Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun i => |x i|) →
      ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Defined in

Mathlib.Topology.Instances.ENNReal.Lemmas

Cited by

1 results in Mathlib

Foundations

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