instConditionallyCompleteLattice

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#OrderDual.instConditionallyCompleteLattice

Lean4

instance instConditionallyCompleteLattice (α : Type*) [ConditionallyCompleteLattice α] :
    ConditionallyCompleteLattice αᵒᵈ :=
  { OrderDual.instInf α, OrderDual.instSup α,
    OrderDual.instLattice α with
    le_csSup := ConditionallyCompleteLattice.csInf_le (α := α)
    csSup_le := ConditionallyCompleteLattice.le_csInf (α := α)
    le_csInf := ConditionallyCompleteLattice.csSup_le (α := α)
    csInf_le := ConditionallyCompleteLattice.le_csSup (α := α) }

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

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

Разделы

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

Аффилиация

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