upperCrossingTime_eq_upperCrossingTime_of_lt

English

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

Русский

Если N ≤ M и верхнее время пересечения N+n меньше N, то верхнее время пересечения между M и (n+1) и нижнее время между M и n совпадают с теми же значениями для N.

LaTeX

$$$N\\le M\\land \\mathrm{upperCrossingTime}(a,b,f,N,n,\\omega) < N\\Rightarrow \\mathrm{upperCrossingTime}(a,b,f,M, n+1,\\omega) = \\mathrm{upperCrossingTime}(a,b,f,N,n+1,\\omega)\\land\\mathrm{lowerCrossingTime}(a,b,f,M,n,\\omega) = \\mathrm{lowerCrossingTime}(a,b,f,N,n,\\omega).$$$

Lean4

theorem upperCrossingTime_eq_upperCrossingTime_of_lt {M : ℕ} (hNM : N ≤ M) (h : upperCrossingTime a b f N n ω < N) :
    upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω :=
  by
  cases n
  · simp
  · exact (crossing_eq_crossing_of_upperCrossingTime_lt hNM h).1

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