bliminf_sup_le_inf_aux_right

Mathlib.Order.LiminfLimsup

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

English

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

Русский

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

LaTeX

$$$ \\operatorname{bliminf} u f (p \\land q) \\le \\operatorname{bliminf} u f q $$$

Lean4

@[simp]
theorem bliminf_sup_le_inf_aux_right : (blimsup u f fun x => p x ∧ q x) ≤ blimsup u f q :=
  blimsup_and_le_inf.trans inf_le_right

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

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

Разделы

Аффилиация

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