upperCrossingTime_lt_succ — Mathlib

English

If n ≤ m, then upperCrossingTime(a,b,f,N,n,ω) ≤ upperCrossingTime(a,b,f,N,m,ω).

Русский

Если n ≤ m, то upperCrossingTime(a,b,f,N,n,ω) ≤ upperCrossingTime(a,b,f,N,m,ω).

LaTeX

$$$\forall \omega\; (n \le m) \Rightarrow \ upperCrossingTime(a,b,f,N,n,\omega) \le upperCrossingTime(a,b,f,N,m,\omega)$$$

Lean4

theorem upperCrossingTime_lt_succ (hab : a < b) (hn : upperCrossingTime a b f N (n + 1) ω ≠ N) :
    upperCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω :=
  lt_of_le_of_lt upperCrossingTime_le_lowerCrossingTime (lowerCrossingTime_lt_upperCrossingTime hab hn)

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