stoppedProcess_eq_of_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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