blimsup_mono

Mathlib.Order.LiminfLimsup

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

English

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

Русский

Если ∀x, p(x) → q(x), тогда blimsup u f p ≤ blimsup u f q.

LaTeX

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

Lean4

theorem blimsup_mono (h : ∀ x, p x → q x) : blimsup u f p ≤ blimsup u f q :=
  sInf_le_sInf fun a ha => ha.mono <| by tauto

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

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

Разделы

Аффилиация

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