orderBot

Mathlib.Order.LatticeIntervals

URI: https://scilib.ai/kg/mathlib#Set.Ico.orderBot

← MathLib Explorer

English

Ico(a,b) has a bottom element whenever a < b; the bottom corresponds to a.

Русский

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

LaTeX

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

Lean4

/-- `Ico a b` has a bottom element whenever `a < b`. -/
instance orderBot [PartialOrder α] {a b : α} [Fact (a < b)] : OrderBot (Ico a b) :=
  (isLeast_Ico Fact.out).orderBot

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

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

Разделы

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

Аффилиация

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