lowerCrossingTime_le_upperCrossingTime_succ

English

For every ω, n, we have lowerCrossingTime(a,b,f,N,n,ω) ≤ upperCrossingTime(a,b,f,N,n+1,ω).

Русский

Для каждого ω и индекса n выполняется неравенство: lowerCrossingTime(a,b,f,N,n,ω) ≤ upperCrossingTime(a,b,f,N,n+1,ω).

LaTeX

$$$\forall \omega,\ n, \ lowerCrossingTime(a,b,f,N,n,\omega) \le upperCrossingTime(a,b,f,N,(n+1),\omega)$$$

Lean4

theorem lowerCrossingTime_le_upperCrossingTime_succ :
    lowerCrossingTime a b f N n ω ≤ upperCrossingTime a b f N (n + 1) ω :=
  by
  rw [upperCrossingTime_succ]
  exact le_hitting lowerCrossingTime_le ω

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