instCompleteLinearOrder

Mathlib.Order.CompleteLattice.Lemmas

URI: https://scilib.ai/kg/mathlib#PUnit.instCompleteLinearOrder

Lean4

instance instCompleteLinearOrder : CompleteLinearOrder PUnit
    where
  __ := instBooleanAlgebra
  __ := instLinearOrder
  sSup := fun _ => unit
  sInf := fun _ => unit
  le_sSup := by intros; trivial
  sSup_le := by intros; trivial
  sInf_le := by intros; trivial
  le_sInf := by intros; trivial
  le_himp_iff := by intros; trivial
  himp_bot := by intros; trivial
  sdiff_le_iff := by intros; trivial
  top_sdiff := by intros; trivial

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

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

Разделы

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

Аффилиация

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