mono_blimsup

Mathlib.Order.LiminfLimsup

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

English

If p x → q x for all x, then blimsup u f p ≤ blimsup u f q.

Русский

Если p(x) → q(x) для всех x, то blimsup u f p ≤ blimsup u f q.

LaTeX

$$$ \\forall x\\ (p(x) \\to q(x)) \\Rightarrow \\blimsup u f p \\le \\blimsup u f q $$$

Lean4

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

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

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

Разделы

Аффилиация

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