stoppedValue_upperCrossingTime — Mathlib

English

If upperCrossingTime(a,b,f,N,(n+1),ω) ≠ N, then b ≤ stoppedValue(f, upperCrossingTime(a,b,f,N,(n+1)), ω).

Русский

Если upperCrossingTime(a,b,f,N,(n+1),ω) ≠ N, то b ≤ остановленное значение функции f в это время.

LaTeX

$$$\text{upperCrossingTime}(a,b,f,N,(n+1),\omega) \neq N \Rightarrow b \le \text{stoppedValue}(f, \text{upperCrossingTime}(a,b,f,N,(n+1)), \omega)$$$

Lean4

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

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