English
Let hτ and hπ be stopping times for the same filtration. The set {ω : τ(ω) ≤ π(ω)} is measurable with respect to the σ-algebra associated to π.
Русский
Пусть hτ и hπ — времена останова для одной и той же фильтрации. Множество {ω : τ(ω) ≤ π(ω)} измеримо относительно σ-алгебры, связанной с π.
LaTeX
$$$\{\omega : \tau(\omega) \le \pi(\omega)\} \in \mathcal{F}_{\pi}$$$
Lean4
theorem measurableSet_stopping_time_le [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι]
[MeasurableSpace ι] [BorelSpace ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
MeasurableSet[hπ.measurableSpace] {ω | τ ω ≤ π ω} :=
by
suffices MeasurableSet[(hτ.min hπ).measurableSpace] {ω : Ω | τ ω ≤ π ω} by rw [measurableSet_min_iff hτ hπ] at this;
exact this.2
rw [← Set.univ_inter {ω : Ω | τ ω ≤ π ω}, ← hτ.measurableSet_inter_le_iff hπ, Set.univ_inter]
exact measurableSet_le_stopping_time hτ hπ
