orderTop

Mathlib.Order.LatticeIntervals

URI: https://scilib.ai/kg/mathlib#Set.Ioc.orderTop

← MathLib Explorer

English

Ioc(a,b) has a top element whenever a < b; the top corresponds to b.

Русский

Ioc(a,b) имеет верхнюю границу при a < b; верхняя граница соответствует b.

LaTeX

$$$[PartialOrder\\;α] {a\\,b:\\alpha} [Fact (a

Lean4

/-- `Ioc a b` has a top element whenever `a < b`. -/
instance orderTop [PartialOrder α] {a b : α} [Fact (a < b)] : OrderTop (Ioc a b) :=
  (isGreatest_Ioc Fact.out).orderTop

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

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

Разделы

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

Аффилиация

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