measurableSet_inter_le_const_iff — Mathlib

English

If the range of τ is countable, then {ω : i ≤ τ(ω)} is measurable in the min-space for all i.

Русский

Если образ τ счётен, то {ω : i ≤ τ(ω)} измеримо в минимальном пространстве для всех i.

LaTeX

$$$\forall i,\; {ω : i \le τ(ω)} ∈ h_τ.measurableSpace$ when (Set.range τ).Countable.$$

Lean4

theorem measurableSet_inter_le_const_iff (hτ : IsStoppingTime f τ) (s : Set Ω) (i : ι) :
    MeasurableSet[hτ.measurableSpace] (s ∩ {ω | τ ω ≤ i}) ↔
      MeasurableSet[(hτ.min_const i).measurableSpace] (s ∩ {ω | τ ω ≤ i}) :=
  by
  rw [IsStoppingTime.measurableSet_min_iff hτ (isStoppingTime_const _ i), IsStoppingTime.measurableSpace_const,
    IsStoppingTime.measurableSet]
  refine ⟨fun h => ⟨h, ?_⟩, fun h j => h.1 j⟩
  specialize h i
  rwa [Set.inter_assoc, Set.inter_self] at h

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