min_const — Mathlib

English

Given hτ is a stopping time, the function ω ↦ min(τ(ω), i) is also a stopping time for every fixed i.

Русский

Пусть hτ — остановочное время; функция ω ↦ min(τ(ω), i) является остановочным временем для любого фиксированного i.

LaTeX

$$$\forall i,\text{IsStoppingTime}(f, \lambda \omega. \min(\tau(\omega), i))$$$

Lean4

protected theorem min_const [LinearOrder ι] {f : Filtration ι m} {τ : Ω → ι} (hτ : IsStoppingTime f τ) (i : ι) :
    IsStoppingTime f fun ω => min (τ ω) i :=
  hτ.min (isStoppingTime_const f i)

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