upperCrossingTime_lt_bddAbove — Mathlib

English

If a<b, then 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_lt_bddAbove (hab : a < b) : BddAbove {n | upperCrossingTime a b f N n ω < N} :=
  by
  obtain ⟨k, hk⟩ := exists_upperCrossingTime_eq f N ω hab
  refine ⟨k, fun n (hn : upperCrossingTime a b f N n ω < N) => ?_⟩
  by_contra hn'
  exact hn.ne (upperCrossingTime_stabilize (not_le.1 hn').le hk)

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