# mathlibdocumentation

data.fintype.order

# Order structures on finite types #

This file provides order instances on fintypes:

• A semilattice_inf instance on a fintype allows constructing an order_bot.
• A semilattice_sup instance on a fintype allows constructing an order_top.
• A lattice instance on a fintype allows constructing a bounded_order.
• A lattice instance on a fintype can be promoted to a complete_lattice.
• A linear_order instance on a fintype can be promoted to a complete_linear_order.

Getting to a bounded_order from a lattice is computable, but the subsequent definitions are not, since the definitions of Sup and Inf use set.to_finset, which implicitly requires a decidable_pred instance for every s : set α.

The complete_linear_order instance for fin (n + 1) is the only proper instance in this file. The rest are defs to avoid loops in typeclass inference.

def fintype.to_order_bot (α : Type u_2) [fintype α] [inhabited α]  :

Constructs the ⊥ of a finite inhabited semilattice_inf.

Equations
def fintype.to_order_top (α : Type u_2) [fintype α] [inhabited α]  :

Constructs the ⊤ of a finite inhabited semilattice_sup

Equations
def fintype.to_bounded_order (α : Type u_2) [fintype α] [inhabited α] [lattice α] :

Constructs the ⊤ and ⊥ of a finite inhabited lattice.

Equations
noncomputable def fintype.to_complete_lattice (α : Type u_2) [fintype α] [hl : lattice α] [hb : bounded_order α] :

A finite bounded lattice is complete.

Equations
noncomputable def fintype.to_complete_linear_order (α : Type u_2) [fintype α] [h : linear_order α]  :

A finite bounded linear order is complete.

Equations
noncomputable def fintype.to_complete_lattice_of_lattice (α : Type u_2) [fintype α] [nonempty α] [lattice α] :

A nonempty finite lattice is complete. If the lattice is already a bounded_order, then use fintype.to_complete_lattice instead, as this gives definitional equality for ⊥ and ⊤.

Equations
noncomputable def fintype.to_complete_linear_order_of_linear_order (α : Type u_2) [fintype α] [nonempty α] [h : linear_order α] :

A nonempty finite linear order is complete. If the linear order is already a bounded_order, then use fintype.to_complete_linear_order instead, as this gives definitional equality for ⊥ and ⊤.

Equations

### fin#

@[protected, instance]
noncomputable def fin.complete_linear_order {n : } :
Equations