measurableSpace_le_of_countable_range

English

For countable τ, the equality-set {ω : τ(ω) = i} is measurable.

Русский

Для счетного τ множество равенств измеримо.

LaTeX

$$$\{ω : τ(ω) = i\}$ measurable when Set.range τ is countable.$$

Lean4

protected theorem measurableSpace_le_of_countable_range (hτ : IsStoppingTime f τ)
    (h_countable : (Set.range τ).Countable) : hτ.measurableSpace ≤ m :=
  by
  intro s hs
  change ∀ i, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i}) at hs
  rw [(_ : s = ⋃ i ∈ Set.range τ, s ∩ {ω | τ ω ≤ i})]
  · exact MeasurableSet.biUnion h_countable fun i _ => f.le i _ (hs i)
  · ext ω
    constructor <;> rw [Set.mem_iUnion]
    · exact fun hx => ⟨τ ω, by simpa using hx⟩
    · rintro ⟨i, hx⟩
      simp only [Set.mem_range, Set.iUnion_exists, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq, exists_prop,
        exists_and_right] at hx
      exact hx.2.1

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