lowerCrossingTime_stabilize — Mathlib

English

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

Русский

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

LaTeX

$$$\forall n,m\; (n \le m \land lowerCrossingTime(a,b,f,N,n,ω) = N) \Rightarrow lowerCrossingTime(a,b,f,N,m,ω) = N$$$

Lean4

theorem lowerCrossingTime_stabilize (hnm : n ≤ m) (hn : lowerCrossingTime a b f N n ω = N) :
    lowerCrossingTime a b f N m ω = N :=
  le_antisymm lowerCrossingTime_le (le_trans (le_of_eq hn.symm) (lowerCrossingTime_mono hnm))

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