# Type synonyms #

This file provides two type synonyms for order theory:

`OrderDual α`

: Type synonym of`α`

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

becomes`b ≤ 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 α`

and`ofLex : Lex α → α`

.

## See also #

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

.

### Order dual #

@[simp]

@[simp]

@[simp]

theorem
OrderDual.toDual_ofDual
{α : Type u_1}
(a : αᵒᵈ)
:

↑OrderDual.toDual (↑OrderDual.ofDual a) = a

@[simp]

**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`

.