∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω}, (MeasureTheory.hittingAfter u s n ω = ⊤) = ∀ (j : ι), n ≤ j → u j ω ∉ s