upperCrossingTime_zero — Mathlib

English

The successor of the upper crossing time satisfies a simple recursion: it equals the hitting time of f above b at the time given by the lower crossing construction.

Русский

Потомок верхнего времени пересечения определяется через простую рекурсию: он равен времени попадания выше b, начиная с времени, заданного нижним временем пересечения.

LaTeX

$$$ upperCrossingTime(a,b,f,N,(n+1)) = hitting\\, f\\; (\\{t \\ge b\\}) \\; (lowerCrossingTimeAux(a,f, (upperCrossingTime(a,b,f,N,n)), N)) $$$

Lean4

@[simp]
theorem upperCrossingTime_zero : upperCrossingTime a b f N 0 = ⊥ :=
  rfl

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