upperCrossingTime_le_lowerCrossingTime

English

For every trajectory ω and all parameters a, b, f, N, n, the upper crossing time at index n never exceeds the corresponding lower crossing time at the same index: upperCrossingTime(a, b, f, N, n, ω) ≤ lowerCrossingTime(a, b, f, N, n, ω).

Русский

Для каждой траектории ω и всех параметров a, b, f, N, n верхнее время кроссинга на позиции n не превосходит соответствующее нижнее время кроссинга на той же позиции: upperCrossingTime(a, b, f, N, n, ω) ≤ lowerCrossingTime(a, b, f, N, n, ω).

LaTeX

$$$\forall \omega\, (\ upperCrossingTime(a,b,f,N,n,\omega) \le \ lowerCrossingTime(a,b,f,N,n,\omega)\ )$$$

Lean4

theorem upperCrossingTime_le_lowerCrossingTime : upperCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N n ω := by
  simp only [lowerCrossingTime, le_hitting upperCrossingTime_le ω]

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