lowerCrossingTime_lt_upperCrossingTime

English

If a < b and upperCrossingTime(a,b,f,N,(n+1),ω) ≠ N, then lowerCrossingTime(a,b,f,N,n,ω) < upperCrossingTime(a,b,f,N,(n+1),ω).

Русский

Если a < b и верхнее время кроссинга на позиции n+1 не равно N, то нижнее время на позиции n меньше верхнего времени на позиции n+1.

LaTeX

$$$\forall a,b\ f,N,n,ω\; (a < b \land upperCrossingTime(a,b,f,N,(n+1),ω) \neq N) \Rightarrow lowerCrossingTime(a,b,f,N,n,ω) < upperCrossingTime(a,b,f,N,(n+1),ω)$$$

Lean4

theorem lowerCrossingTime_lt_upperCrossingTime (hab : a < b) (hn : upperCrossingTime a b f N (n + 1) ω ≠ N) :
    lowerCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω :=
  by
  refine
    lt_of_le_of_ne lowerCrossingTime_le_upperCrossingTime_succ fun h =>
      not_le.2 hab <| le_trans (stoppedValue_upperCrossingTime hn) ?_
  simp only [stoppedValue]
  rw [← h]
  exact stoppedValue_lowerCrossingTime (h.symm ▸ hn)

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