measurableSet_ge_of_countable_range'

English

If Set.range τ is countable, then {ω : i ≤ τ(ω)} is measurable in the stopping-time sigma-algebra for each i.

Русский

Если Set.range τ счётно, то {ω : i ≤ τ(ω)} измеримо в сигма-алгебре останова для каждого i.

LaTeX

$$$\{ω : i \le τ(ω)\}$ is measurable in $h_τ.measurableSpace$ when $(\mathrm{Set.range}\, τ)$ is countable.$$

Lean4

protected theorem measurableSet_ge_of_countable_range' (hτ : IsStoppingTime f τ) (h_countable : (Set.range τ).Countable)
    (i : ι) : MeasurableSet[hτ.measurableSpace] {ω | i ≤ τ ω} :=
  by
  have : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω} :=
    by
    ext1 ω
    simp only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]
    rw [@eq_comm _ i, or_comm]
  rw [this]
  exact (hτ.measurableSet_eq_of_countable_range' h_countable i).union (hτ.measurableSet_gt' i)

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