upperCrossingTime_lt_of_le_upcrossingsBefore

English

If 0 < N and a < b and n ≤ upcrossingsBefore a b f N ω, then upperCrossingTime a b f N n ω < N.

Русский

Пусть 0 < N, a < b и n ≤ upcrossingsBefore a b f N ω. Тогда upperCrossingTime a b f N n ω < N.

LaTeX

$$$0< N\\;\\land\\; a

Lean4

theorem upperCrossingTime_lt_of_le_upcrossingsBefore (hN : 0 < N) (hab : a < b) (hn : n ≤ upcrossingsBefore a b f N ω) :
    upperCrossingTime a b f N n ω < N :=
  haveI : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N :=
    (upperCrossingTime_lt_nonempty hN).csSup_mem
      ((OrderBot.bddBelow _).finite_of_bddAbove (upperCrossingTime_lt_bddAbove hab))
  lt_of_le_of_lt (upperCrossingTime_mono hn) this

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