upperCrossingTime_le — Mathlib

English

The stopped process of a submartingale is itself a submartingale.

Русский

Остановленный процесс субмартингала снова является субмартингалом.

LaTeX

$$$ \\text{stoppedProcess}(f,\\tau) \\ -> \\text{Submartingale} \\ $$$

Lean4

theorem upperCrossingTime_le : upperCrossingTime a b f N n ω ≤ N :=
  by
  cases n
  · simp only [upperCrossingTime_zero, Pi.bot_apply, bot_le]
  · simp only [upperCrossingTime_succ, hitting_le]

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