English
Let hτ be a stopping time and i ∈ ι with IsLUB(Iio(i), i). Then {ω : τ(ω) < i} is measurable with respect to F_i.
Русский
Пусть hτ — остановочное время, и для i выполнено IsLUB(Iio(i), i). Тогда {ω : τ(ω) < i} измеримо относительно F_i.
LaTeX
$$$\forall i,\, IsLUB(\mathrm{Iio}(i), i) \Rightarrow \{\omega \in \Omega \mid \tau(\omega) < i\} \in \mathcal{F}_i$$$
Lean4
theorem measurableSet_lt (hτ : IsStoppingTime f τ) (i : ι) : MeasurableSet[f i] {ω | τ ω < i} :=
by
obtain ⟨i', hi'_lub⟩ : ∃ i', IsLUB (Set.Iio i) i' := exists_lub_Iio i
rcases lub_Iio_eq_self_or_Iio_eq_Iic i hi'_lub with hi'_eq_i | h_Iio_eq_Iic
· rw [← hi'_eq_i] at hi'_lub ⊢
exact hτ.measurableSet_lt_of_isLUB i' hi'_lub
· have h_lt_eq_preimage : {ω : Ω | τ ω < i} = τ ⁻¹' Set.Iio i := rfl
rw [h_lt_eq_preimage, h_Iio_eq_Iic]
exact f.mono (lub_Iio_le i hi'_lub) _ (hτ.measurableSet_le i')
