bliminf_antitone

Mathlib.Order.LiminfLimsup

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

English

If f ≤ g, then bliminf u g p ≤ bliminf u f p.

Русский

Если f ≤ g, то bliminf u g p ≤ bliminf u f p.

LaTeX

$$$ f \\le g \\Rightarrow \\operatorname{bliminf} u g p \\le \\operatorname{bliminf} u f p $$$

Lean4

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

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

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

Разделы

Аффилиация

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