Hitting times

theorem MeasureTheory.hittingAfter_eq_coe_iff {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] [WellFoundedLT ι] {u : ι → Ω → β} {s : Set β} {n i : ι} {ω : Ω} : hittingAfter u s n ω = ↑i ↔ n ≤ i ∧ u i ω ∈ s ∧ ∀ j ∈ Set.Ico n i, u j ω ∉ s