English
Under directedness and generation hypotheses, hτ.measurableSpace ≤ m holds.
Русский
При заданных предположениях направленности и порождения выполняется вложение hτ.measurableSpace ⊆ m.
LaTeX
$$$h_{\tau}.\mathrm{measurableSpace} \le m$ under the stated hypotheses$$
Lean4
theorem measurableSpace_le [IsCountablyGenerated (atTop : Filter ι)] [IsDirected ι (· ≤ ·)] (hτ : IsStoppingTime f τ) :
hτ.measurableSpace ≤ m := by
intro s hs
cases isEmpty_or_nonempty ι
· haveI : IsEmpty Ω := ⟨fun ω => IsEmpty.false (τ ω)⟩
apply Subsingleton.measurableSet
· change ∀ i, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i}) at hs
obtain ⟨seq : ℕ → ι, h_seq_tendsto⟩ := (atTop : Filter ι).exists_seq_tendsto
rw [(_ : s = ⋃ n, s ∩ {ω | τ ω ≤ seq n})]
· exact MeasurableSet.iUnion fun i => f.le (seq i) _ (hs (seq i))
· ext ω; constructor <;> rw [Set.mem_iUnion]
· intro hx
suffices ∃ i, τ ω ≤ seq i from ⟨this.choose, hx, this.choose_spec⟩
rw [tendsto_atTop] at h_seq_tendsto
exact (h_seq_tendsto (τ ω)).exists
· rintro ⟨_, hx, _⟩
exact hx
