English
For any s, the measurability of s ∩ {τ = i} in hτ.measurableSpace equals measurability of s ∩ {τ = i} in f_i.
Русский
Для любого s измеримость s ∩ {τ = i} в hτ.measurableSpace эквивалентна измеримости в f_i.
LaTeX
$$$\text{MeasurableSet}_{h_{\tau}}(s \cap \{\omega: τ(\omega) = i\}) \iff \text{MeasurableSet}_{f_i}(s \cap \{\omega: τ(\omega) = i\})$$$
Lean4
theorem measurableSet_inter_eq_iff (hτ : IsStoppingTime f τ) (s : Set Ω) (i : ι) :
MeasurableSet[hτ.measurableSpace] (s ∩ {ω | τ ω = i}) ↔ MeasurableSet[f i] (s ∩ {ω | τ ω = i}) :=
by
have : ∀ j, {ω : Ω | τ ω = i} ∩ {ω : Ω | τ ω ≤ j} = {ω : Ω | τ ω = i} ∩ {_ω | i ≤ j} :=
by
intro j
ext1 ω
simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_congr_right_iff]
intro hxi
rw [hxi]
constructor <;> intro h
· specialize h i
simpa only [Set.inter_assoc, this, le_refl, Set.setOf_true, Set.inter_univ] using h
· intro j
rw [Set.inter_assoc, this]
by_cases hij : i ≤ j
· simp only [hij, Set.setOf_true, Set.inter_univ]
exact f.mono hij _ h
· simp [hij]
