measurableSpace_const — Mathlib

English

The measurable space for a constant i in the stopping-time construction equals the i-th filtration space.

Русский

Измеримое пространство для константы i в конструировании остановочного времени равно пространству фильтрации F_i.

LaTeX

$$$\text{measurableSpace}(f, i) = f_i$$$

Lean4

@[simp]
theorem measurableSpace_const (f : Filtration ι m) (i : ι) : (isStoppingTime_const f i).measurableSpace = f i :=
  by
  ext1 s
  change MeasurableSet[(isStoppingTime_const f i).measurableSpace] s ↔ MeasurableSet[f i] s
  rw [IsStoppingTime.measurableSet]
  constructor <;> intro h
  · specialize h i
    simpa only [le_refl, Set.setOf_true, Set.inter_univ] using h
  · intro j
    by_cases hij : i ≤ j
    · simp only [hij, Set.setOf_true, Set.inter_univ]
      exact f.mono hij _ h
    · simp only [hij, Set.setOf_false, Set.inter_empty, @MeasurableSet.empty _ (f.1 j)]

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