mathlib3 documentation

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

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:

Those are marked as def to avoid typeclass loops.

Concrete instances #

We provide a few instances for concrete types:

@[reducible]
def fintype.to_order_bot (α : Type u_2) [fintype α] [nonempty α] [semilattice_inf α] :

Constructs the of a finite nonempty semilattice_inf.

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

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

A finite bounded lattice 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

Concrete instances #

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

Directed Orders #

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