measurableSpace_min_const — Mathlib

English

The measurable space of the minimum with a constant equals the infimum of the stopping-time space and the constant index space.

Русский

Измеримое пространство минимума с константой равно инфиминуму между пространством останова и пространством константы.

LaTeX

$$$ (h_τ.min_const i).measurableSpace = h_τ.measurableSpace \sqcap f i $$$

Lean4

theorem measurableSpace_min_const (hτ : IsStoppingTime f τ) {i : ι} :
    (hτ.min_const i).measurableSpace = hτ.measurableSpace ⊓ f i := by
  rw [hτ.measurableSpace_min (isStoppingTime_const _ i), measurableSpace_const]

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