isStoppingTime_upperCrossingTime — Mathlib

English

If n ≤ m and upperCrossingTime(a,b,f,N,n,ω) = N, then upperCrossingTime(a,b,f,N,m,ω) = N.

Русский

Если n ≤ m и upperCrossingTime(a,b,f,N,n,ω) = N, тогда upperCrossingTime(a,b,f,N,m,ω) = N.

LaTeX

$$$\forall n,m\; (n \le m) \land upperCrossingTime(a,b,f,N,n,ω) = N \Rightarrow upperCrossingTime(a,b,f,N,m,ω) = N$$$

Lean4

theorem isStoppingTime_upperCrossingTime (hf : Adapted ℱ f) : IsStoppingTime ℱ (upperCrossingTime a b f N n) :=
  hf.isStoppingTime_crossing.1

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