upperCrossingTime_mono — 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_mono (hnm : n ≤ m) : upperCrossingTime a b f N n ω ≤ upperCrossingTime a b f N m ω :=
  by
  suffices Monotone fun n => upperCrossingTime a b f N n ω by exact this hnm
  exact
    monotone_nat_of_le_succ fun n =>
      le_trans upperCrossingTime_le_lowerCrossingTime lowerCrossingTime_le_upperCrossingTime_succ

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