isPredPrelimit_top

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#Order.isPredPrelimit_top

English

Let α be a preorder with a greatest element ⊤. Then ⊤ is a pred-prelimit.

Русский

Пусть α имеет предкласс упорядоченности с верхним элементом ⊤. Тогда ⊤ является пред-предлимитным элементом.

LaTeX

$$$IsPredPrelimit(\top)$$$

Lean4

theorem isPredPrelimit_top [OrderTop α] : IsPredPrelimit (⊤ : α) :=
  isMax_top.isPredPrelimit

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

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

Разделы

Аффилиация

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