notMem_of_lt_hitting — Mathlib

English

If k lies before the hitting time, then u_k(ω) ∉ s; i.e., once the hitting time bound is exceeded, the process does not re-enter s at earlier indices.

Русский

Если k находится до времени попадания, то u_k(ω) ∉ s; после достижения границы процесс не возвращается в s на ранних индексах.

LaTeX

$$$k<\text{hitting}(u,s,n,m,\omega) \Rightarrow u_k(\omega) \notin s$$$

Lean4

theorem notMem_of_lt_hitting {m k : ι} (hk₁ : k < hitting u s n m ω) (hk₂ : n ≤ k) : u k ω ∉ s := by
  classical
  intro h
  have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s := ⟨k, ⟨hk₂, le_trans hk₁.le <| hitting_le _⟩, h⟩
  refine not_le.2 hk₁ ?_
  simp_rw [hitting, if_pos hexists]
  exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hitting_le _⟩, h⟩

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