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 α.

Equations

• αᵒᵈ = α

def «term_ᵒᵈ» : Lean.TrailingParserDescr

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

Equations

• «term_ᵒᵈ» = Lean.ParserDescr.trailingNode `«term_ᵒᵈ» 1024 0 (Lean.ParserDescr.symbol "ᵒᵈ")

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 αᵒᵈ

Equations

• OrderDual.instLE α = { le := fun (x y : α) => y ≤ x }

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

Equations

• OrderDual.instLT α = { lt := fun (x y : α) => y < x }

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

Equations

• OrderDual.instOrd α = { compare := fun (a b : α) => compare b a }

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

Equations

• OrderDual.instSup α = { max := fun (x1 x2 : α) => x1 ⊓ x2 }

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

Equations

• OrderDual.instInf α = { min := fun (x1 x2 : α) => x1 ⊔ x2 }

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 αᵒᵈ

Equations

• OrderDual.instPreorder α = { toLE := OrderDual.instLE α, toLT := OrderDual.instLT α, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

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

Equations

• OrderDual.instPartialOrder α = { toPreorder := inferInstanceAs (Preorder αᵒᵈ), le_antisymm := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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

The opposite linear order to a given linear order

Equations

• LinearOrder.swap α x✝ = inferInstanceAs (LinearOrder αᵒᵈ)

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

Equations

• OrderDual.instInhabited = x

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 α