# Type synonyms #

This file provides two type synonyms for order theory:

`OrderDual α`

: Type synonym of`α`

to equip it with the dual order (`a ≤ b≤ b`

becomes`b ≤ a≤ a`

).`Lex α`

: Type synonym of`α`

to equip it with its lexicographic order. The precise meaning depends on the type we take the lex of. Examples include`Prod`

,`Sigma`

,`List`

,`Finset`

.

## Notation #

`αᵒᵈ`

is notation for `OrderDual α`

.

The general rule for notation of `Lex`

types is to append `ₗ`

to the usual notation.

## Implementation notes #

One should not abuse definitional equality between `α`

and `αᵒᵈ`

/`Lex α`

. Instead, explicit
coercions should be inserted:

`OrderDual`

:`OrderDual.toDual : α → αᵒᵈ→ αᵒᵈ`

and`OrderDual.ofDual : αᵒᵈ → α→ α`

`Lex`

:`toLex : α → Lex α→ Lex α`

and`ofLex : Lex α → α→ α`

.

## See also #

This file is similar to `Algebra.Group.TypeTags`

.

### Order dual #

`toDual`

is the identity function to the `OrderDual`

of a linear order.

## Equations

- OrderDual.toDual = Equiv.refl α

@[simp]

@[simp]

@[simp]

def
OrderDual.rec
{α : Type u_1}
{C : αᵒᵈ → Sort u_2}
(h₂ : (a : α) → C (↑OrderDual.toDual a))
(a : αᵒᵈ)
:

C a

Recursor for `αᵒᵈ`

.

## Equations

- OrderDual.rec h₂ = h₂

**Alias** of the reverse direction of `OrderDual.toDual_le_toDual`

.

**Alias** of the reverse direction of `OrderDual.toDual_lt_toDual`

.

**Alias** of the reverse direction of `OrderDual.ofDual_le_ofDual`

.

**Alias** of the reverse direction of `OrderDual.ofDual_lt_ofDual`

.