upcrossingsBefore_mono — Mathlib

English

For hab : a < b, the map N ↦ upcrossingsBefore a b f N ω is monotone in N for every ω.

Русский

Для a < b, отображение N ↦ upcrossingsBefore a b f N ω монотонно по N для каждого ω.

LaTeX

$$$\\text{Monotone}_{N}\\bigl(\\omega \\mapsto \\mathrm{upcrossingsBefore}(a,b,f,N,\\omega)\\bigr)\\;\\text{при } a

Lean4

theorem upcrossingsBefore_mono (hab : a < b) : Monotone fun N ω => upcrossingsBefore a b f N ω :=
  by
  intro N M hNM ω
  simp only [upcrossingsBefore]
  gcongr sSup {n | ?_} with n
  · exact upperCrossingTime_lt_bddAbove hab
  intro hn
  rw [upperCrossingTime_eq_upperCrossingTime_of_lt hNM hn]
  exact lt_of_lt_of_le hn hNM

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