lowerCrossingTime_lt_of_lt_upcrossingsBefore

English

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

Русский

Если 0 < N, a < b и n < upcrossingsBefore a b f N ω, то lowerCrossingTime a b f N n ω < N.

LaTeX

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

Lean4

theorem lowerCrossingTime_lt_of_lt_upcrossingsBefore (hN : 0 < N) (hab : a < b) (hn : n < upcrossingsBefore a b f N ω) :
    lowerCrossingTime a b f N n ω < N :=
  lt_of_le_of_lt lowerCrossingTime_le_upperCrossingTime_succ (upperCrossingTime_lt_of_le_upcrossingsBefore hN hab hn)

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