hitting_le — Mathlib

English

If the lower bound i equals the upper bound m, then hitting time equals m; more generally, if i is at the end, the hitting time aligns with the boundary.

Русский

Если нижняя граница совпадает с верхней, время попадания равно верхней границе; в общем случае попадание следует границе.

LaTeX

$$$i = m \Rightarrow \text{hitting}(u,s,n,m) = m$$$

Lean4

theorem hitting_le {m : ι} (ω : Ω) : hitting u s n m ω ≤ m :=
  by
  simp only [hitting]
  split_ifs with h
  · obtain ⟨j, hj₁, hj₂⟩ := h
    change j ∈ {i | u i ω ∈ s} at hj₂
    exact (csInf_le (BddBelow.inter_of_left bddBelow_Icc) (Set.mem_inter hj₁ hj₂)).trans hj₁.2
  · exact le_rfl

Похожие утверждения