measurableSpace_mono — Mathlib

English

If hτ ≤ hπ as stopping-time spaces, then hτ.measurableSpace ≤ hπ.measurableSpace.

Русский

Если пространства измеримости для двух остановочных времен удовлетворяют неравенству, то первое пространство подмножество второго.

LaTeX

$$$h_{\tau}.\mathrm{measurableSpace} \le h_{\pi}.\mathrm{measurableSpace}$$$

Lean4

theorem measurableSpace_mono (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) (hle : τ ≤ π) :
    hτ.measurableSpace ≤ hπ.measurableSpace := by
  intro s hs i
  rw [(_ : s ∩ {ω | π ω ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | π ω ≤ i})]
  · exact (hs i).inter (hπ i)
  · ext
    simp only [Set.mem_inter_iff, iff_self_and, and_congr_left_iff, Set.mem_setOf_eq]
    intro hle' _
    exact le_trans (hle _) hle'

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