instLinearOrder

Mathlib.Order.Basic

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

Lean4

instance instLinearOrder : LinearOrder PUnit where
  le := fun _ _ ↦ True
  lt := fun _ _ ↦ False
  max := fun _ _ ↦ unit
  min := fun _ _ ↦ unit
  toDecidableEq := inferInstance
  toDecidableLE := fun _ _ ↦ Decidable.isTrue trivial
  toDecidableLT := fun _ _ ↦ Decidable.isFalse id
  le_refl := by intros; trivial
  le_trans := by intros; trivial
  le_total := by intros; exact Or.inl trivial
  le_antisymm := by intros; rfl
  lt_iff_le_not_ge := by simp only [not_true, and_false, forall_const]

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

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

Разделы

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

Аффилиация

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