English
The definition of hitting time is given by a conditional expression: it equals m if there is no hitting j in [n,m], and equals sInf of the set of indices in [n,m] that hit s otherwise.
Русский
Определение времени попадания задаётся через условное выражение: время равно m, если нет попадания в интервале [n,m], иначе это infimum множества индексов, приводящих к попаданию.
LaTeX
$$$\text{hitting}(u,s,n,m) = \begin{cases} m &\text{если не существует } j\in [n,m], u_j\in s, \\ \mathrm{sInf}([n,m]\cap \{i: u_i\in s\}) &\text{иначе}. \end{cases}$$$
Lean4
theorem hitting_def [Preorder ι] [InfSet ι] (u : ι → Ω → β) (s : Set β) (n m : ι) :
hitting u s n m = fun x => if ∃ j ∈ Set.Icc n m, u j x ∈ s then sInf (Set.Icc n m ∩ {i : ι | u i x ∈ s}) else m :=
rfl
