upperCrossingTime_eq_of_bound_le — Mathlib

English

For hab: a<b and N ≤ n, upperCrossingTime(a,b,f,N,n,ω) = N.

Русский

При a<b и N ≤ n выполняется upperCrossingTime(a,b,f,N,n,ω) = N.

LaTeX

$$$\forall a,b, f, N, ω\; (a < b) \land N \le n \Rightarrow upperCrossingTime(a,b,f,N,n,\omega) = N$$$

Lean4

theorem upperCrossingTime_eq_of_bound_le (hab : a < b) (hn : N ≤ n) : upperCrossingTime a b f N n ω = N :=
  le_antisymm upperCrossingTime_le (le_trans (upperCrossingTime_bound_eq f N ω hab).symm.le (upperCrossingTime_mono hn))

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