mem_atTop

Mathlib.Order.Filter.AtTopBot.Defs

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

English

For any a in a preorder, the upward ray {b | a ≤ b} belongs to atTop.

Русский

Для любого a в частично упорядоченном множестве множество {b | a ≤ b} принадлежит atTop.

LaTeX

$$$\\{b \\in \\alpha \\mid a \\le b\\} \\in \\mathrm{atTop}.$$$

Lean4

theorem mem_atTop [Preorder α] (a : α) : {b : α | a ≤ b} ∈ @atTop α _ :=
  mem_iInf_of_mem a <| Subset.refl _

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

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

Разделы

Аффилиация

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