Order structures on finite types

This file provides order instances on fintypes.

Computable instances

On a Fintype, we can construct

• an OrderBot from SemilatticeInf.
• an OrderTop from SemilatticeSup.
• a BoundedOrder from Lattice.

Those are marked as def to avoid defeqness issues.

Completion instances

Those instances are noncomputable because the definitions of sSup and sInf use Set.toFinset and set membership is undecidable in general.

On a Fintype, we can promote:

• a Lattice to a CompleteLattice.
• a DistribLattice to a CompleteDistribLattice.
• a LinearOrder to a CompleteLinearOrder.
• a BooleanAlgebra to a CompleteAtomicBooleanAlgebra.

Those are marked as def to avoid typeclass loops.

Concrete instances

We provide a few instances for concrete types:

• Fin.completeLinearOrder
• Bool.completeLinearOrder
• Bool.completeBooleanAlgebra

@[reducible]

def Fintype.toOrderBot (α : Type u_2) [Fintype α] [Nonempty α] [SemilatticeInf α] : OrderBot α

Constructs the ⊥ of a finite nonempty SemilatticeInf.

@[reducible]

def Fintype.toOrderTop (α : Type u_2) [Fintype α] [Nonempty α] [SemilatticeSup α] : OrderTop α

Constructs the ⊤ of a finite nonempty SemilatticeSup

@[reducible]

def Fintype.toBoundedOrder (α : Type u_2) [Fintype α] [Nonempty α] [Lattice α] : BoundedOrder α

Constructs the ⊤ and ⊥ of a finite nonempty Lattice.

@[reducible]

noncomputable def Fintype.toCompleteLattice (α : Type u_2) [Fintype α] [Lattice α] [BoundedOrder α] : CompleteLattice α

A finite bounded lattice is complete.

@[reducible]

noncomputable def Fintype.toCompleteDistribLattice (α : Type u_2) [Fintype α] [DistribLattice α] [BoundedOrder α] : CompleteDistribLattice α

A finite bounded distributive lattice is completely distributive.

@[reducible]

noncomputable def Fintype.toCompleteLinearOrder (α : Type u_2) [Fintype α] [LinearOrder α] [BoundedOrder α] : CompleteLinearOrder α

A finite bounded linear order is complete.

@[reducible]

noncomputable def Fintype.toCompleteBooleanAlgebra (α : Type u_2) [Fintype α] [BooleanAlgebra α] : CompleteBooleanAlgebra α

A finite boolean algebra is complete.

@[reducible]

noncomputable def Fintype.toCompleteAtomicBooleanAlgebra (α : Type u_2) [Fintype α] [BooleanAlgebra α] : CompleteAtomicBooleanAlgebra α

A finite boolean algebra is complete and atomic.

@[reducible]

noncomputable def Fintype.toCompleteLatticeOfNonempty (α : Type u_2) [Fintype α] [Nonempty α] [Lattice α] : CompleteLattice α

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 ⊤.

@[reducible]

noncomputable def Fintype.toCompleteLinearOrderOfNonempty (α : Type u_2) [Fintype α] [Nonempty α] [LinearOrder α] : CompleteLinearOrder α

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 ⊤.

Concrete instances

noncomputable instance Fin.completeLinearOrder {n : ℕ} : CompleteLinearOrder (Fin (n + 1))

noncomputable instance Bool.completeLinearOrder : CompleteLinearOrder Bool

noncomputable instance Bool.completeBooleanAlgebra : CompleteBooleanAlgebra Bool

noncomputable instance Bool.completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra Bool

Directed Orders

theorem Directed.fintype_le {α : Type u_1} {r : α → α → Prop} [IsTrans α 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 α] [IsDirected α fun x x_1 => x ≤ x_1] {β : Type u_2} [Fintype β] (f : β → α) : ∃ M, ∀ (i : β), f i ≤ M

theorem Fintype.exists_ge {α : Type u_1} [Nonempty α] [Preorder α] [IsDirected α fun x x_1 => x ≥ x_1] {β : Type u_2} [Fintype β] (f : β → α) : ∃ M, ∀ (i : β), M ≤ f i

theorem Fintype.bddAbove_range {α : Type u_1} [Nonempty α] [Preorder α] [IsDirected α fun x x_1 => x ≤ x_1] {β : Type u_2} [Fintype β] (f : β → α) : BddAbove (Set.range f)

theorem Fintype.bddBelow_range {α : Type u_1} [Nonempty α] [Preorder α] [IsDirected α fun x x_1 => x ≥ x_1] {β : Type u_2} [Fintype β] (f : β → α) : BddBelow (Set.range f)