∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ}
  {ω : Ω}, MeasureTheory.lowerCrossingTime a b f N n ω ≤ MeasureTheory.upperCrossingTime a b f N (n + 1) ω