English
If there exists a hitting in [n,m], then hitting ≤ i is equivalent to there existing a hit in [n,i].
Русский
Если существует попадание в [n,m], то hitting ≤ i эквивалентно существованию попадания в [n,i].
LaTeX
$$$\exists j\in [n,i], u_j(\omega)\in s$$$
Lean4
theorem hitting_le_iff_of_exists [WellFoundedLT ι] {m : ι} (h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s) :
hitting u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s :=
by
constructor <;> intro h'
· exact ⟨hitting u s n m ω, ⟨le_hitting_of_exists h_exists, h'⟩, hitting_mem_set h_exists⟩
· have h'' : ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s :=
by
obtain ⟨k₁, hk₁_mem, hk₁_s⟩ := h_exists
obtain ⟨k₂, hk₂_mem, hk₂_s⟩ := h'
refine ⟨min k₁ k₂, ⟨le_min hk₁_mem.1 hk₂_mem.1, min_le_min hk₁_mem.2 hk₂_mem.2⟩, ?_⟩
exact min_rec' (fun j => u j ω ∈ s) hk₁_s hk₂_s
obtain ⟨k, hk₁, hk₂⟩ := h''
refine le_trans ?_ (hk₁.2.trans (min_le_right _ _))
exact hitting_le_of_mem hk₁.1 (hk₁.2.trans (min_le_left _ _)) hk₂
