English
If m1 ≤ m2, then the hitting time is nondecreasing in the upper bound: hitting u s n m1 ω ≤ hitting u s n m2 ω for all ω.
Русский
Если m1 ≤ m2, то время попадания не убывает при увеличении верхнего предела: hitting u s n m1 ω ≤ hitting u s n m2 ω для всех ω.
LaTeX
$$$\\forall m_1,m_2\\in ι,\\ m_1 \\le m_2 \\Rightarrow\\ \\forall \\omega\\in Ω,\\ hitting\\ u\\ s\\ n\\ m_1\\omega \\le hitting\\ u\\ s\\ n\\ m_2\\omega.$$$
Lean4
theorem hitting_mono {m₁ m₂ : ι} (hm : m₁ ≤ m₂) : hitting u s n m₁ ω ≤ hitting u s n m₂ ω :=
by
by_cases h : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
· exact (hitting_eq_hitting_of_exists hm h).le
· simp_rw [hitting, if_neg h]
split_ifs with h'
· obtain ⟨j, hj₁, hj₂⟩ := h'
refine le_csInf ⟨j, hj₁, hj₂⟩ ?_
by_contra hneg; push_neg at hneg
obtain ⟨i, hi₁, hi₂⟩ := hneg
exact h ⟨i, ⟨hi₁.1.1, hi₂.le⟩, hi₁.2⟩
· exact hm
