English
For a stopping time hτ with countable range, the sets {ω | τ(ω) = i} are measurable in F_i for all i.
Русский
Для времени останова с счетным диапазоном множество {ω | τ(ω) = i} измеримо в F_i для всех i.
LaTeX
$$$$ \forall i, \MeasurableSet[f i] {\omega \mid τ(\omega) = i}. $$$$
Lean4
protected theorem measurableSet_eq_of_countable_range (hτ : IsStoppingTime f τ) (h_countable : (Set.range τ).Countable)
(i : ι) : MeasurableSet[f i] {ω | τ ω = i} :=
by
have : {ω | τ ω = i} = {ω | τ ω ≤ i} \ ⋃ (j ∈ Set.range τ) (_ : j < i), {ω | τ ω ≤ j} :=
by
ext1 a
simp only [Set.mem_setOf_eq, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq', Set.mem_diff, Set.mem_iUnion,
exists_prop, not_exists, not_and]
constructor <;> intro h
· simp only [h, lt_iff_le_not_ge, le_refl, and_imp, imp_self, imp_true_iff, and_self_iff]
· exact h.1.eq_or_lt.resolve_right fun h_lt => h.2 a h_lt le_rfl
rw [this]
refine (hτ.measurableSet_le i).diff ?_
refine MeasurableSet.biUnion h_countable fun j _ => ?_
classical
rw [Set.iUnion_eq_if]
split_ifs with hji
· exact f.mono hji.le _ (hτ.measurableSet_le j)
· exact @MeasurableSet.empty _ (f i)
