ordConnectedSubsetConditionallyCompleteLinearOrder

Mathlib.Order.CompleteLatticeIntervals

URI: https://scilib.ai/kg/mathlib#ordConnectedSubsetConditionallyCompleteLinearOrder

Lean4

/-- A nonempty `OrdConnected` set in a conditionally complete linear order is naturally a
conditionally complete linear order. -/
noncomputable instance ordConnectedSubsetConditionallyCompleteLinearOrder [Inhabited s] [OrdConnected s] :
    ConditionallyCompleteLinearOrder s :=
  subsetConditionallyCompleteLinearOrder s (fun h => sSup_within_of_ordConnected h)
    (fun h => sInf_within_of_ordConnected h)

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

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

Разделы

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

Аффилиация

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