English
If there exists a hitting time, the image under hitting lies in s; otherwise, the condition is trivial. This ensures membership is preserved at hitting time.
Русский
Если существует время попадания, изображение попадания принадлежит s; иначе условие тривиально. Это обеспечивает принадлежность внутри s в момент попадания.
LaTeX
$$$\text{If }\exists j\in [n,m], u_j(\omega)\in s,\text{ then } u_{\text{hitting}(u,s,n,m,\omega)}(\omega)\in s.$$$
Lean4
theorem le_hitting {m : ι} (hnm : n ≤ m) (ω : Ω) : n ≤ hitting u s n m ω :=
by
simp only [hitting]
split_ifs with h
· refine le_csInf ?_ fun b hb => ?_
· obtain ⟨k, hk_Icc, hk_s⟩ := h
exact ⟨k, hk_Icc, hk_s⟩
· rw [Set.mem_inter_iff] at hb
exact hb.1.1
· exact hnm
