max — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem max [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → ι} (hτ : IsStoppingTime f τ)
    (hπ : IsStoppingTime f π) : IsStoppingTime f fun ω => max (τ ω) (π ω) :=
  by
  intro i
  simp_rw [max_le_iff, Set.setOf_and]
  exact (hτ i).inter (hπ i)

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