mathlib documentation


Order structures on finite types #

This file provides order instances on fintypes:

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 α] [semilattice_inf α] :

Constructs the of a finite inhabited semilattice_inf.

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

Constructs the of a finite inhabited semilattice_sup

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

Constructs the and of a finite inhabited lattice.

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

A finite bounded lattice is complete.

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 .


fin #

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