measurableSpace_le_of_countable — Mathlib

English

If ι is countable, then the measurable space associated with τ is bounded by the ambient measurable space m.

Русский

Если множество индексов счетно, то связанная сигма‑алгебра τ вложена в исходную сигма‑алгебру m.

LaTeX

$$$[\text{Countable } ι] \Rightarrow h_τ.\mathrm{measurableSpace} \le m$$$

Lean4

theorem measurableSpace_le_of_countable [Countable ι] (hτ : IsStoppingTime f τ) : hτ.measurableSpace ≤ m :=
  by
  intro s hs
  change ∀ i, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i}) at hs
  rw [(_ : s = ⋃ i, s ∩ {ω | τ ω ≤ i})]
  · exact MeasurableSet.iUnion fun i => f.le i _ (hs i)
  · ext ω; constructor <;> rw [Set.mem_iUnion]
    · exact fun hx => ⟨τ ω, hx, le_rfl⟩
    · rintro ⟨_, hx, _⟩
      exact hx

Похожие утверждения