English
For any i, the set {ω ∈ Ω : τ(ω) = i} is measurable; this is the intersection of {τ ≤ i} and {τ ≥ i}.
Русский
Для каждого i множество {ω ∈ Ω : τ(ω) = i} измеримо; это пересечение {τ ≤ i} и {τ ≥ i}.
LaTeX
$$$\forall i, \{\omega \in \Omega \mid \tau(\omega) = i\} = \{\omega \in \Omega \mid \tau(\omega) \le i\} \cap \{\omega \in \Omega \mid \tau(\omega) \ge i\}$$$
Lean4
theorem add {f : Filtration ℕ m} {τ π : Ω → ℕ} (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
IsStoppingTime f (τ + π) := by
intro i
rw [(_ : {ω | (τ + π) ω ≤ i} = ⋃ k ≤ i, {ω | π ω = k} ∩ {ω | τ ω + k ≤ i})]
·
exact
MeasurableSet.iUnion fun k =>
MeasurableSet.iUnion fun hk => (hπ.measurableSet_eq_le hk).inter (hτ.add_const_nat i)
ext ω
simp only [Pi.add_apply, Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff, exists_prop]
refine ⟨fun h => ⟨π ω, by cutsat, rfl, h⟩, ?_⟩
rintro ⟨j, hj, rfl, h⟩
assumption
