le_sup_of_le_left

Mathlib.Order.Filter.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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