mono_bliminf'

Mathlib.Order.LiminfLimsup

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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