eventually_gt_atTop

Mathlib.Order.Filter.AtTopBot.Defs

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

English

For any a, eventually a < x along atTop if NoTopOrder holds.

Русский

Для любого a существует x, удовлетворяющее a < x и x ∈ atTop, при условии отсутствия верхней границы.

LaTeX

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

Lean4

theorem eventually_gt_atTop [Preorder α] [NoTopOrder α] (a : α) : ∀ᶠ x in atTop, a < x :=
  Ioi_mem_atTop a

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

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

Разделы

Аффилиация

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