eventually_ge_atTop

Mathlib.Order.Filter.AtTopBot.Defs

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

English

For any a, eventually x ≥ a along atTop.

Русский

Для любого a существует элемент x, такой что x ≥ a и x находится в atTop вплоть до бесконечности.

LaTeX

$$$\\forall a,\\ \\forall^\\! x\\ in\\ \\mathrm{atTop},\\ a \\le x.$$$

Lean4

theorem eventually_ge_atTop [Preorder α] (a : α) : ∀ᶠ x in atTop, a ≤ x :=
  mem_atTop a

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

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

Разделы

Аффилиация

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