measurableSet_min_const_iff — Mathlib

English

Equivalence between measurability in the minimum space and measurability in both component spaces.

Русский

Эквивалентность измеримости в минимальном пространстве и измеримости в обоих составляющих пространствах.

LaTeX

$$Measured set in min space iff measured in both spaces.$$

Lean4

theorem measurableSet_min_const_iff (hτ : IsStoppingTime f τ) (s : Set Ω) {i : ι} :
    MeasurableSet[(hτ.min_const i).measurableSpace] s ↔ MeasurableSet[hτ.measurableSpace] s ∧ MeasurableSet[f i] s := by
  rw [measurableSpace_min_const hτ]; apply MeasurableSpace.measurableSet_inf

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