adapted_stoppedProcess — Mathlib

English

If u is adapted and τ is a stopping time, then the stoppedProcess u τ is adapted.

Русский

Если u адаптирован, а τ — время останова, то остановленный процесс адаптирован.

LaTeX

$$$\text{Adapted}(f, \text{stoppedProcess}(u, \tau))$$$

Lean4

theorem adapted_stoppedProcess [PseudoMetrizableSpace ι] (h : ProgMeasurable f u) (hτ : IsStoppingTime f τ) :
    Adapted f (MeasureTheory.stoppedProcess u τ) :=
  (h.stoppedProcess hτ).adapted

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