English
Let n, m1, m2 be indices with m1 ≤ m2 and let ω ∈ Ω. If there exists some j between n and m1 such that u(j, ω) ∈ s, then the hitting times with upper bounds m1 and m2 coincide: hitting u s n m1 ω = hitting u s n m2 ω.
Русский
Пусть n, m1, m2 — индексы с условием m1 ≤ m2 и пусть ω ∈ Ω. Если существует j между n и m1 таким, что u(j, ω) ∈ s, тогда времена попадания с верхними пределами m1 и m2 совпадают: hitting u s n m1 ω = hitting u s n m2 ω.
LaTeX
$$$\\forall m_1,m_2\\in ι,\\ m_1 \\le m_2\\ \\land\\ (\\exists j\\in \\mathrm{Icc}(n,m_1),\\ u(j,\\omega)\\in s) \\Longrightarrow\\ hitting\\ u\\ s\\ n\\ m_1\\ \\omega = hitting\\ u\\ s\\ n\\ m_2\\ \\omega.$$$
Lean4
theorem hitting_eq_hitting_of_exists {m₁ m₂ : ι} (h : m₁ ≤ m₂) (h' : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s) :
hitting u s n m₁ ω = hitting u s n m₂ ω :=
by
simp only [hitting, if_pos h']
obtain ⟨j, hj₁, hj₂⟩ := h'
rw [if_pos]
· refine le_antisymm ?_ (by gcongr; exacts [bddBelow_Icc.inter_of_left, ⟨j, hj₁, hj₂⟩])
refine le_csInf ⟨j, Set.Icc_subset_Icc_right h hj₁, hj₂⟩ fun i hi => ?_
by_cases hi' : i ≤ m₁
· exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hi.1.1, hi'⟩, hi.2⟩
· change j ∈ {i | u i ω ∈ s} at hj₂
exact ((csInf_le bddBelow_Icc.inter_of_left ⟨hj₁, hj₂⟩).trans hj₁.2).trans (le_of_not_ge hi')
exact ⟨j, ⟨hj₁.1, hj₁.2.trans h⟩, hj₂⟩
