measurableSet_inter_le_iff — Mathlib

English

Equivalence between measurability of s ∩ {τ ≤ π} in the stopping-time space and in the minimum space.

Русский

Эквивалентность измеримости в пространстве пересечения остановок и минимума.

LaTeX

$$Iff between measurability in min-space and in the intersection with τ ≤ π.$$

Lean4

theorem measurableSet_inter_le_iff [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι]
    [MeasurableSpace ι] [BorelSpace ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) (s : Set Ω) :
    MeasurableSet[hτ.measurableSpace] (s ∩ {ω | τ ω ≤ π ω}) ↔
      MeasurableSet[(hτ.min hπ).measurableSpace] (s ∩ {ω | τ ω ≤ π ω}) :=
  by
  constructor <;> intro h
  · have : s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω} := by rw [Set.inter_assoc, Set.inter_self]
    rw [this]
    exact measurableSet_inter_le _ hπ _ h
  · rw [measurableSet_min_iff hτ hπ] at h
    exact h.1

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