lowerCrossingTime_mono — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem lowerCrossingTime_mono (hnm : n ≤ m) : lowerCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N m ω :=
  by
  suffices Monotone fun n => lowerCrossingTime a b f N n ω by exact this hnm
  exact
    monotone_nat_of_le_succ fun n =>
      le_trans lowerCrossingTime_le_upperCrossingTime_succ upperCrossingTime_le_lowerCrossingTime

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