le_sup_of_le_right

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.EventuallyLE.le_sup_of_le_right

← MathLib Explorer

English

If h ≤ᶠ[l] g, then h ≤ᶠ[l] f ⊔ g.

Русский

Если h ≤ᶠ[l] g, то h ≤ᶠ[l] f ⊔ g.

LaTeX

$$$$ h \\leq^{\\!l} g \\Rightarrow h \\leq^{\\!l} f \\sqcup g. $$$$

Lean4

theorem le_sup_of_le_right [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hg : h ≤ᶠ[l] g) : h ≤ᶠ[l] f ⊔ g :=
  hg.mono fun _ => _root_.le_sup_of_le_right

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

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

Разделы

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

Аффилиация

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