stoppedProcess_eq_of_ge — Mathlib

English

If τ(ω) ≥ i, then the stopped process at time i equals the value u(i) at ω.

Русский

Если τ(ω) ≥ i, тогда на момент i остановленный процесс равен значению u(i) в ω.

LaTeX

$$$\text{stoppedProcess}(u, \tau, i)(\omega) = u(i, \omega) \quad \text{whenever } \tau(\omega) \ge i$$$

Lean4

theorem stoppedProcess_eq_of_ge {u : ι → Ω → β} {τ : Ω → ι} {i : ι} {ω : Ω} (h : τ ω ≤ i) :
    stoppedProcess u τ i ω = u (τ ω) ω := by simp [stoppedProcess, min_eq_right h]

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