blimsup_and_le_inf

Mathlib.Order.LiminfLimsup

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

← MathLib Explorer

English

blimsup u f (p ∧ q) ≤ blimsup u f p ⊓ blimsup u f q

Русский

blimsup u f (p ∧ q) ≤ blimsup u f p ∧ blimsup u f q

LaTeX

$$$ \\operatorname{blimsup} u f (\\,\\lambda x. p x \\land q x\\,) \\le \\operatorname{blimsup} u f p \\sqcap \\operatorname{blimsup} u f q $$$

Lean4

theorem blimsup_and_le_inf : (blimsup u f fun x => p x ∧ q x) ≤ blimsup u f p ⊓ blimsup u f q :=
  le_inf (blimsup_mono <| by tauto) (blimsup_mono <| by tauto)

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

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

Разделы

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

Аффилиация

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