English
If hitting u s n m ω < m, then u (hitting u s n m ω) ω ∈ s; i.e., once hitting is strictly before the end, the hitting point lies in the target set.
Русский
Если hitting u s n m ω < m, то u( hitting u s n m ω, ω ) ∈ s; то есть точка попадания принадлежит s.
LaTeX
$$$\text{If } \text{hitting}(u,s,n,m,\omega) < m, \text{ then } u_{\text{hitting}(u,s,n,m,\omega)}(\omega) \in s.$$$
Lean4
theorem hitting_lt_iff [WellFoundedLT ι] {m : ι} (i : ι) (hi : i ≤ m) :
hitting u s n m ω < i ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s :=
by
constructor <;> intro h'
· have h : ∃ j ∈ Set.Icc n m, u j ω ∈ s := by
by_contra h
simp_rw [hitting, if_neg h, ← not_le] at h'
exact h' hi
exact ⟨hitting u s n m ω, ⟨le_hitting_of_exists h, h'⟩, hitting_mem_set h⟩
· obtain ⟨k, hk₁, hk₂⟩ := h'
refine lt_of_le_of_lt ?_ hk₁.2
exact hitting_le_of_mem hk₁.1 (hk₁.2.le.trans hi) hk₂
