measurableSet_eq_of_countable' — Mathlib

English

If τ has countable range, then for each i, the set {ω : τ(ω) = i} is measurable.

Русский

Если образ τ счётен, то множество {ω : τ(ω) = i} измеримо.

LaTeX

$$$\text{If } (\mathrm{Set.range}\, τ) \text{ is Countable, then } {ω : τ(ω) = i} \in h_τ.measurableSpace$.$$

Lean4

protected theorem measurableSet_eq_of_countable' [Countable ι] (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[hτ.measurableSpace] {ω | τ ω = i} :=
  hτ.measurableSet_eq_of_countable_range' (Set.to_countable _) i

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