upperCrossingTime_stabilize' — Mathlib

English

For a<b, the set {n | upperCrossingTime(a,b,f,N,n,ω) < N} is bounded above.

Русский

Для a < b множество {n | upperCrossingTime(a,b,f,N,n,ω) < N} ограничено сверху.

LaTeX

$$$\forall a,b\; (a < b) \Rightarrow BddAbove \{n \mid upperCrossingTime(a,b,f,N,n,\omega) < N\}$$$

Lean4

theorem upperCrossingTime_stabilize' (hnm : n ≤ m) (hn : N ≤ upperCrossingTime a b f N n ω) :
    upperCrossingTime a b f N m ω = N :=
  upperCrossingTime_stabilize hnm
    (le_antisymm upperCrossingTime_le hn)
      -- `upperCrossingTime_bound_eq` provides an explicit bound

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