blimsup_monotone_filter

Mathlib.Order.LiminfLimsup

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

English

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

Русский

Если фильтр f меньше g, то blimsup u f p ≤ blimsup u g p.

LaTeX

$$$ f \\le g \\Rightarrow \\blimsup u f p \\le \\blimsup u g p $$$

Lean4

theorem blimsup_monotone_filter (h : f ≤ g) : blimsup u f p ≤ blimsup u g p :=
  sInf_le_sInf fun _ ha => ha.filter_mono h

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

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

Разделы

Аффилиация

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