order.order_dual

# Initial lemmas to work with the order_dual

## Definitions

to_dual and of_dual the order reversing identity maps, bundled as equivalences.

## Basic Lemmas to convert between an order and its dual

This file is similar to algebra/group/type_tags.lean

def order_dual.to_dual {α : Type u} :
α

to_dual is the identity function to the order_dual of a linear order.

Equations
def order_dual.of_dual {α : Type u} :
α

of_dual is the identity function from the order_dual of a linear order.

Equations
@[simp]
theorem order_dual.to_dual_symm_eq {α : Type u} :

@[simp]
theorem order_dual.of_dual_symm_eq {α : Type u} :

@[simp]
theorem order_dual.to_dual_of_dual {α : Type u} (a : order_dual α) :

@[simp]
theorem order_dual.of_dual_to_dual {α : Type u} (a : α) :

@[simp]
theorem order_dual.to_dual_inj {α : Type u} {a b : α} :

@[simp]
theorem order_dual.to_dual_le_to_dual {α : Type u} [has_le α] {a b : α} :

@[simp]
theorem order_dual.to_dual_lt_to_dual {α : Type u} [has_lt α] {a b : α} :

@[simp]
theorem order_dual.of_dual_inj {α : Type u} {a b : order_dual α} :

@[simp]
theorem order_dual.of_dual_le_of_dual {α : Type u} [has_le α] {a b : order_dual α} :

@[simp]
theorem order_dual.of_dual_lt_of_dual {α : Type u} [has_lt α] {a b : order_dual α} :

theorem order_dual.le_to_dual {α : Type u} [has_le α] {a : order_dual α} {b : α} :

theorem order_dual.lt_to_dual {α : Type u} [has_lt α] {a : order_dual α} {b : α} :

theorem order_dual.to_dual_le {α : Type u} [has_le α] {a : α} {b : order_dual α} :

theorem order_dual.to_dual_lt {α : Type u} [has_lt α] {a : α} {b : order_dual α} :