measurableSet_min_iff — Mathlib

English

The measurable space of the minimum equals the infimum of the two spaces; a set is measurable in the minimum iff it is measurable in both spaces.

Русский

Измеримое пространство минимума равно пересечению минимальных сигма-алгебр; множество измеримо в минимуме тогда и только тогда, когда оно измеримо в обоих пространствах.

LaTeX

$$$\text{Measurable}(s)\_{(h_τ.min h_π).measurableSpace} \iff \text{Measurable}(s)\_{h_τ.measurableSpace} \land \text{Measurable}(s)\_{h_π.measurableSpace}$$$

Lean4

theorem measurableSet_min_iff (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) (s : Set Ω) :
    MeasurableSet[(hτ.min hπ).measurableSpace] s ↔
      MeasurableSet[hτ.measurableSpace] s ∧ MeasurableSet[hπ.measurableSpace] s :=
  by rw [measurableSpace_min hτ hπ]; rfl

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