upperCrossingTime_lt_lowerCrossingTime

English

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

Русский

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

LaTeX

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

Lean4

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

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