Order dual

This file defines OrderDual α, a type synonym reversing the meaning of all inequalities, with notation αᵒᵈ.

Notation

αᵒᵈ is notation for OrderDual α.

Implementation notes

One should not abuse definitional equality between α and αᵒᵈ. Instead, explicit coercions should be inserted:

• OrderDual.toDual : α → αᵒᵈ and OrderDual.ofDual : αᵒᵈ → α

def OrderDual (α : Type u_2) : Type u_2

Type synonym to equip a type with the dual order: ≤ means ≥ and < means >. αᵒᵈ is notation for OrderDual α.

def «term_ᵒᵈ» : Lean.TrailingParserDescr

Type synonym to equip a type with the dual order: ≤ means ≥ and < means >. αᵒᵈ is notation for OrderDual α.

instance OrderDual.instNonempty (α : Type u_2) [h : Nonempty α] : Nonempty αᵒᵈ

instance OrderDual.instSubsingleton (α : Type u_2) [h : Subsingleton α] : Subsingleton αᵒᵈ

instance OrderDual.instLE (α : Type u_2) [LE α] : LE αᵒᵈ

instance OrderDual.instLT (α : Type u_2) [LT α] : LT αᵒᵈ

instance OrderDual.instOrd (α : Type u_2) [Ord α] : Ord αᵒᵈ

instance OrderDual.instSup (α : Type u_2) [Min α] : Max αᵒᵈ

instance OrderDual.instInf (α : Type u_2) [Max α] : Min αᵒᵈ

instance OrderDual.instIsTransLE {α : Type u_1} [LE α] [T : IsTrans α LE.le] : IsTrans αᵒᵈ LE.le

instance OrderDual.instIsTransLT {α : Type u_1} [LT α] [T : IsTrans α LT.lt] : IsTrans αᵒᵈ LT.lt

instance OrderDual.instTrichotomousLt {α : Type u_1} [LT α] [T : Std.Trichotomous LT.lt] : Std.Trichotomous LT.lt

instance OrderDual.instPreorder (α : Type u_2) [Preorder α] : Preorder αᵒᵈ

instance OrderDual.instPartialOrder (α : Type u_2) [PartialOrder α] : PartialOrder αᵒᵈ

instance OrderDual.instDecidableEq (α : Type u_2) [DecidableEq α] : DecidableEq αᵒᵈ

instance OrderDual.instDecidableLT (α : Type u_2) [LT α] [DecidableLT α] : DecidableLT αᵒᵈ

instance OrderDual.instDecidableLE (α : Type u_2) [LE α] [DecidableLE α] : DecidableLE αᵒᵈ

instance OrderDual.instLinearOrder (α : Type u_2) [LinearOrder α] : LinearOrder αᵒᵈ

def LinearOrder.swap (α : Type u_2) : LinearOrder α → LinearOrder α

The opposite linear order to a given linear order

instance OrderDual.instInhabited {α : Type u_1} [Inhabited α] : Inhabited αᵒᵈ

theorem OrderDual.Ord.dual_dual (α : Type u_2) [H : Ord α] : instOrd αᵒᵈ = H

theorem OrderDual.Preorder.dual_dual (α : Type u_2) [H : Preorder α] : instPreorder αᵒᵈ = H

theorem OrderDual.instPartialOrder.dual_dual (α : Type u_2) [H : PartialOrder α] : instPartialOrder αᵒᵈ = H

theorem OrderDual.instLinearOrder.dual_dual (α : Type u_2) [H : LinearOrder α] : instLinearOrder αᵒᵈ = H

DenselyOrdered for OrderDual

instance OrderDual.denselyOrdered (α : Type u_2) [LT α] [h : DenselyOrdered α] : DenselyOrdered αᵒᵈ

@[simp]

theorem denselyOrdered_orderDual {α : Type u_1} [LT α] : DenselyOrdered αᵒᵈ ↔ DenselyOrdered α