upperCrossingTime_succ — Mathlib

English

Equality for the succ step: the (n+1)-th upper crossing time equals the hitting time of the upper set above b after applying the lower crossing construction.

Русский

Эквивалентность на шаге суcc: время верхнего пересечения (n+1) равно времени попадания выше 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

theorem upperCrossingTime_succ :
    upperCrossingTime a b f N (n + 1) ω =
      hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω :=
  by rw [upperCrossingTime]

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