min — Mathlib

English

If τ is a stopping time and i ≥ 0 (in additive setting), then ω ↦ τ(ω) + i is a stopping time.

Русский

Если τ — остановочное время и i ≥ 0, то ω ↦ τ(ω) + i — остановочное время.

LaTeX

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

Lean4

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

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