stoppedValue_lowerCrossingTime — Mathlib

English

If lowerCrossingTime(a,b,f,N,n,ω) ≠ N, then the stopped value of f at that time satisfies stoppedValue(f, lowerCrossingTime(a,b,f,N,n), ω) ≤ a.

Русский

Если lowerCrossingTime(a,b,f,N,n,ω) ≠ N, то остановленное значение функции f в этот момент не превосходит a.

LaTeX

$$$\text{lowerCrossingTime}(a,b,f,N,n,ω) \neq N \;\Rightarrow\; \text{stoppedValue}(f, \text{lowerCrossingTime}(a,b,f,N,n), ω) \le a$$$

Lean4

theorem stoppedValue_lowerCrossingTime (h : lowerCrossingTime a b f N n ω ≠ N) :
    stoppedValue f (lowerCrossingTime a b f N n) ω ≤ a :=
  by
  obtain ⟨j, hj₁, hj₂⟩ := (hitting_le_iff_of_lt _ (lt_of_le_of_ne lowerCrossingTime_le h)).1 le_rfl
  exact stoppedValue_hitting_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 lowerCrossingTime_le⟩, hj₂⟩

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