bliminf_antitone_filter

Mathlib.Order.LiminfLimsup

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

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 \\bliminf u g p \\le \\bliminf u f p $$$

Lean4

theorem bliminf_antitone_filter (h : f ≤ g) : bliminf u g p ≤ bliminf u f p :=
  sSup_le_sSup fun _ ha => ha.filter_mono h

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

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

Разделы

Аффилиация

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