isStoppingTime_of_measurableSet_eq

English

If for every i, the set {ω : τ(ω) = i} is measurable, then τ is a stopping time.

Русский

Если для каждого i множество {ω : τ(ω) = i} измеримо, то τ является остановочным временем.

LaTeX

$$$\big(\forall i, \{\omega \in \Omega \mid \tau(\omega) = i\} \in \mathcal{F}_i\big) \Rightarrow \text{IsStoppingTime}(f, \tau)$$$

Lean4

theorem isStoppingTime_of_measurableSet_eq [Preorder ι] [Countable ι] {f : Filtration ι m} {τ : Ω → ι}
    (hτ : ∀ i, MeasurableSet[f i] {ω | τ ω = i}) : IsStoppingTime f τ :=
  by
  intro i
  rw [show {ω | τ ω ≤ i} = ⋃ k ≤ i, {ω | τ ω = k} by ext; simp]
  refine MeasurableSet.biUnion (Set.to_countable _) fun k hk => ?_
  exact f.mono hk _ (hτ k)

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