# mathlib3documentation

data.fintype.order

# Order structures on finite types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides order instances on fintypes.

## Computable instances #

On a fintype, we can construct

• an order_bot from semilattice_inf.
• an order_top from semilattice_sup.
• a bounded_order from lattice.

Those are marked as def to avoid defeqness issues.

## Completion instances #

Those instances are noncomputable because the definitions of Sup and Inf use set.to_finset and set membership is undecidable in general.

On a fintype, we can promote:

• a lattice to a complete_lattice.
• a distrib_lattice to a complete_distrib_lattice.
• a linear_order to a complete_linear_order.
• a boolean_algebra to a complete_boolean_algebra.

Those are marked as def to avoid typeclass loops.

## Concrete instances #

We provide a few instances for concrete types:

• fin.complete_linear_order
• bool.complete_linear_order
• bool.complete_boolean_algebra
@[reducible]
def fintype.to_order_bot (α : Type u_2) [fintype α] [nonempty α]  :

Constructs the ⊥ of a finite nonempty semilattice_inf.

Equations
@[reducible]
def fintype.to_order_top (α : Type u_2) [fintype α] [nonempty α]  :

Constructs the ⊤ of a finite nonempty semilattice_sup

Equations
@[reducible]
def fintype.to_bounded_order (α : Type u_2) [fintype α] [nonempty α] [lattice α] :

Constructs the ⊤ and ⊥ of a finite nonempty lattice.

Equations
@[reducible]
noncomputable def fintype.to_complete_lattice (α : Type u_2) [fintype α] [lattice α]  :

A finite bounded lattice is complete.

Equations
@[reducible]
noncomputable def fintype.to_complete_distrib_lattice (α : Type u_2) [fintype α]  :

A finite bounded distributive lattice is completely distributive.

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

A finite bounded linear order is complete.

Equations
@[reducible]
noncomputable def fintype.to_complete_boolean_algebra (α : Type u_2) [fintype α]  :

A finite boolean algebra is complete.

Equations
@[reducible]
noncomputable def fintype.to_complete_lattice_of_nonempty (α : 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
@[reducible]
noncomputable def fintype.to_complete_linear_order_of_nonempty (α : Type u_2) [fintype α] [nonempty α] [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

### Concrete instances #

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

### Directed Orders #

theorem directed.fintype_le {α : Type u_1} {r : α α Prop} [ r] {β : Type u_2} {γ : Type u_3} [nonempty γ] {f : γ α} [fintype β] (D : f) (g : β γ) :
(z : γ), (i : β), r (f (g i)) (f z)
theorem fintype.exists_le {α : Type u_1} [nonempty α] [preorder α] {β : Type u_2} [fintype β] (f : β α) :
(M : α), (i : β), f i M
theorem fintype.bdd_above_range {α : Type u_1} [nonempty α] [preorder α] {β : Type u_2} [fintype β] (f : β α) :