mono_blimsup' — Mathlib

English

If eventually p(x) → u(x) ≤ v(x) holds, then blimsup u f p ≤ blimsup v f p.

Русский

Если периодически выполняется p(x) → u(x) ≤ v(x), тогда blimsup u f p ≤ blimsup v f p.

LaTeX

$$$ \\exists^{\\text{eventually}} x\\in f:\\ p(x) \\to u(x) \\le v(x) \\Rightarrow \\ blimsup\\,u\\,f\\,p \\le blimsup\\,v\\,f\\,p $$$

Lean4

theorem mono_blimsup' (h : ∀ᶠ x in f, p x → u x ≤ v x) : blimsup u f p ≤ blimsup v f p :=
  sInf_le_sInf fun _ ha => (ha.and h).mono fun _ hx hx' => (hx.2 hx').trans (hx.1 hx')

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