English
If hτ is a stopping time, then for any i, the set {ω | τ(ω) < i} is measurable in the i-th filtration, under a suitable predecessor relation on ι.
Русский
Если hτ — время останова, то для любого i множество {ω | τ(ω) < i} измеримо в f_i.
LaTeX
$$$$ \forall i, \MeasurableSet[f i] {\omega \mid τ(\omega) < i}. $$$$
Lean4
theorem measurableSet_lt_of_pred [PredOrder ι] (hτ : IsStoppingTime f τ) (i : ι) : MeasurableSet[f i] {ω | τ ω < i} :=
by
by_cases hi_min : IsMin i
· suffices {ω : Ω | τ ω < i} = ∅ by rw [this]; exact @MeasurableSet.empty _ (f i)
ext1 ω
simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]
rw [isMin_iff_forall_not_lt] at hi_min
exact hi_min (τ ω)
have : {ω : Ω | τ ω < i} = τ ⁻¹' Set.Iic (pred i) := by ext; simp [Iic_pred_of_not_isMin hi_min]
rw [this]
exact f.mono (pred_le i) _ (hτ.measurableSet_le <| pred i)
