English
If N ≤ M and there is an n with upperCrossingTime a b f N n ω < N, then upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω.
Русский
Если существует n такое, что upperCrossingTime a b f N n ω < N, то верхнее время пересечения между M и N одинаково: верхнее время между M и n равно между N и n.
LaTeX
$$$N\\le M \\land \\mathrm{upperCrossingTime}(a,b,f,N,n,\\omega) < N\\Rightarrow \\mathrm{upperCrossingTime}(a,b,f,M,n,\\omega) = \\mathrm{upperCrossingTime}(a,b,f,N,n,\\omega).$$$
Lean4
theorem crossing_eq_crossing_of_upperCrossingTime_lt {M : ℕ} (hNM : N ≤ M)
(h : upperCrossingTime a b f N (n + 1) ω < N) :
upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧
lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω :=
by
have :=
(crossing_eq_crossing_of_lowerCrossingTime_lt hNM (lt_of_le_of_lt lowerCrossingTime_le_upperCrossingTime_succ h)).2
refine ⟨?_, this⟩
rw [upperCrossingTime_succ_eq, upperCrossingTime_succ_eq, eq_comm, this]
refine hitting_eq_hitting_of_exists hNM ?_
rw [upperCrossingTime_succ_eq, hitting_lt_iff] at h
· obtain ⟨j, hj₁, hj₂⟩ := h
exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
· exact le_rfl
