toConditionallyCompleteLattice

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#CompleteLattice.toConditionallyCompleteLattice

Lean4

/-- A complete lattice is a conditionally complete lattice, as there are no restrictions
on the properties of sInf and sSup in a complete lattice. -/
instance (priority := 100) toConditionallyCompleteLattice [CompleteLattice α] : ConditionallyCompleteLattice α :=
  { ‹CompleteLattice α› with
    le_csSup := by intros; apply le_sSup; assumption
    csSup_le := by intros; apply sSup_le; assumption
    csInf_le := by intros; apply sInf_le; assumption
    le_csInf := by intros; apply le_sInf; assumption }
    -- see Note [lower instance priority]

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

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

Разделы

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

Аффилиация

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