English
If the index set ι carries the discrete topology, and u is adapted to f while τ is a stopping time for f, then the stopped process obtained from u at τ is adapted to f.
Русский
Если индексное множество ι имеет дискретную топологию, и u является адаптированным к f, а τ — остановка по f, то останленный процесс, полученный из u по τ, адаптирован к f.
LaTeX
$$$ [DiscreteTopology\ ι] \wedge (hu : \text{Adapted } f\ u) \wedge (hτ : \text{IsStoppingTime } f\ τ) \Rightarrow (\text{Adapted } f\ (\text{stoppedProcess } u\ τ)) $$$
Lean4
/-- If the indexing order has the discrete topology, then the stopped process of an adapted process
is adapted. -/
theorem stoppedProcess_of_discrete [DiscreteTopology ι] (hu : Adapted f u) (hτ : IsStoppingTime f τ) :
Adapted f (MeasureTheory.stoppedProcess u τ) :=
(hu.progMeasurable_of_discrete.stoppedProcess hτ).adapted
