instLinearOrder

Mathlib.Order.Basic

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

Lean4

/-- A subtype of a linear order is a linear order. We explicitly give the proofs of decidable
equality and decidable order in order to ensure the decidability instances are all definitionally
equal. -/
instance instLinearOrder [LinearOrder α] (p : α → Prop) : LinearOrder (Subtype p) :=
  @LinearOrder.lift (Subtype p) _ _ ⟨fun x y ↦ ⟨max x y, max_rec' _ x.2 y.2⟩⟩ ⟨fun x y ↦ ⟨min x y, min_rec' _ x.2 y.2⟩⟩
    (fun (a : Subtype p) ↦ (a : α)) Subtype.coe_injective (fun _ _ ↦ rfl) fun _ _ ↦ rfl

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

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

Разделы

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

Аффилиация

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