Documentation

Mathlib.Data.Fintype.Order

Order structures on finite types #

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.toFinset 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:

def Fintype.toOrderBot (α : Type u_1) [inst : Fintype α] [inst : Nonempty α] [inst : SemilatticeInf α] :

Constructs the ⊥⊥ of a finite nonempty SemilatticeInf.

Equations
def Fintype.toOrderTop (α : Type u_1) [inst : Fintype α] [inst : Nonempty α] [inst : SemilatticeSup α] :

Constructs the ⊤⊤ of a finite nonempty SemilatticeSup

Equations
def Fintype.toBoundedOrder (α : Type u_1) [inst : Fintype α] [inst : Nonempty α] [inst : Lattice α] :

Constructs the ⊤⊤ and ⊥⊥ of a finite nonempty Lattice.

Equations
noncomputable def Fintype.toCompleteLattice (α : Type u_1) [inst : Fintype α] [inst : Lattice α] [inst : BoundedOrder α] :

A finite bounded lattice is complete.

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def Fintype.toCompleteDistribLattice (α : Type u_1) [inst : Fintype α] [inst : DistribLattice α] [inst : BoundedOrder α] :

A finite bounded distributive lattice is completely distributive.

Equations
noncomputable def Fintype.toCompleteLinearOrder (α : Type u_1) [inst : Fintype α] [inst : LinearOrder α] [inst : BoundedOrder α] :

A finite bounded linear order is complete.

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def Fintype.toCompleteBooleanAlgebra (α : Type u_1) [inst : Fintype α] [inst : BooleanAlgebra α] :

A finite boolean algebra is complete.

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def Fintype.toCompleteLatticeOfNonempty (α : Type u_1) [inst : Fintype α] [inst : Nonempty α] [inst : Lattice α] :

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

Equations
noncomputable def Fintype.toCompleteLinearOrderOfNonempty (α : Type u_1) [inst : Fintype α] [inst : Nonempty α] [inst : LinearOrder α] :

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

Equations
  • One or more equations did not get rendered due to their size.

Concrete instances #

noncomputable instance Fin.completeLinearOrder {n : } :
Equations

Directed Orders #

theorem Directed.fintype_le {α : Type u_1} {r : ααProp} [inst : IsTrans α r] {β : Type u_2} {γ : Type u_3} [inst : Nonempty γ] {f : γα} [inst : Fintype β] (D : Directed r f) (g : βγ) :
z, (i : β) → r (f (g i)) (f z)
theorem Fintype.exists_le {α : Type u_1} [inst : Nonempty α] [inst : Preorder α] [inst : IsDirected α fun x x_1 => x x_1] {β : Type u_2} [inst : Fintype β] (f : βα) :
M, ∀ (i : β), f i M
theorem Fintype.bddAbove_range {α : Type u_1} [inst : Nonempty α] [inst : Preorder α] [inst : IsDirected α fun x x_1 => x x_1] {β : Type u_2} [inst : Fintype β] (f : βα) :