le_apply_bliminf

Mathlib.Order.LiminfLimsup

URI: https://scilib.ai/kg/mathlib#sInfHom.le_apply_bliminf

← MathLib Explorer

English

Let g be a sInfHom. Then bliminf (g ∘ u) f p ≤ g (bliminf u f p).

Русский

Пусть g — отображение типа sInfHom. Тогда bliminf (g ∘ u) f p ≤ g (bliminf u f p).

LaTeX

$$$\\operatorname{bliminf}(g \\circ u) f p \\le g(\\operatorname{bliminf} u f p)$$$

Lean4

theorem _root_.sInfHom.le_apply_bliminf [CompleteLattice γ] (g : sInfHom α γ) :
    bliminf (g ∘ u) f p ≤ g (bliminf u f p) :=
  (sInfHom.dual g).apply_blimsup_le

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

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

Разделы

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

Аффилиация

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