upperCrossingTime_stabilize — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem upperCrossingTime_stabilize (hnm : n ≤ m) (hn : upperCrossingTime a b f N n ω = N) :
    upperCrossingTime a b f N m ω = N :=
  le_antisymm upperCrossingTime_le (le_trans (le_of_eq hn.symm) (upperCrossingTime_mono hnm))

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