add_const — Mathlib

English

If τ and π are stopping times, then ω ↦ τ(ω) + π(ω) is a stopping time (in Nat as base).

Русский

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

LaTeX

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

Lean4

theorem add_const [AddGroup ι] [Preorder ι] [AddRightMono ι] [AddLeftMono ι] {f : Filtration ι m} {τ : Ω → ι}
    (hτ : IsStoppingTime f τ) {i : ι} (hi : 0 ≤ i) : IsStoppingTime f fun ω => τ ω + i :=
  by
  intro j
  simp_rw [← le_sub_iff_add_le]
  exact f.mono (sub_le_self j hi) _ (hτ (j - i))

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