max_const — Mathlib

English

If τ and π are stopping times, then ω ↦ min(τ(ω), π(ω)) is a stopping time.

Русский

Если τ и π — остановочные времена, то ω ↦ min(τ(ω), π(ω)) является остановочным временем.

LaTeX

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

Lean4

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

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