mono_bliminf

Mathlib.Order.LiminfLimsup

URI: https://scilib.ai/kg/mathlib#Filter.mono_bliminf

English

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

Русский

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

LaTeX

$$$ \\exists^{\\text{eventually}} x\\ (p(x) \\to u(x) \\le v(x)) \\Rightarrow \\bliminf u f p \\le \\bliminf v f p $$$

Lean4

theorem mono_bliminf (h : ∀ x, p x → u x ≤ v x) : bliminf u f p ≤ bliminf v f p :=
  mono_bliminf' <| Eventually.of_forall h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru