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 supₛ and infₛ 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 CompleteBooleanAlgebra.

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

ink

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

Constructs the ⊥⊥ of a finite nonempty SemilatticeInf.

Equations

• Fintype.toOrderBot α = OrderBot.mk (_ : ∀ (a : α), Finset.inf' Finset.univ (_ : ∃ x, x ∈ Finset.univ) id ≤ id a)

ink

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

Constructs the ⊤⊤ of a finite nonempty SemilatticeSup

Equations

• Fintype.toOrderTop α = OrderTop.mk (_ : ∀ (a : α), id a ≤ Finset.sup' Finset.univ (_ : ∃ x, x ∈ Finset.univ) id)

ink

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

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

Equations

• Fintype.toBoundedOrder α = let src := Fintype.toOrderBot α; let src_1 := Fintype.toOrderTop α; BoundedOrder.mk

ink

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

A finite bounded lattice is complete.

Equations

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

ink

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

A finite bounded distributive lattice is completely distributive.

Equations

• Fintype.toCompleteDistribLattice α = let src := Fintype.toCompleteLattice α; CompleteDistribLattice.mk (_ : ∀ (a : α) (s : Set α), (⨅ b, ⨅ h, a ⊔ b) ≤ a ⊔ infₛ s)

ink

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

A finite bounded linear order is complete.

Equations

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

ink

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

A finite boolean algebra is complete.

Equations

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

ink

noncomputable def Fintype.toCompleteLatticeOfNonempty (α : Type u_1) [inst : Fintype α] [inst : Nonempty α] [inst : 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 ⊤⊤.

Equations

• Fintype.toCompleteLatticeOfNonempty α = Fintype.toCompleteLattice α

ink

noncomputable def Fintype.toCompleteLinearOrderOfNonempty (α : Type u_1) [inst : Fintype α] [inst : Nonempty α] [inst : 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 ⊤⊤.

Equations

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

Concrete instances

ink

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

Equations

• Fin.completeLinearOrder = Fintype.toCompleteLinearOrder (Fin (n + 1))

ink

noncomputable instance Bool.completeLinearOrder : CompleteLinearOrder Bool

Equations

• Bool.completeLinearOrder = Fintype.toCompleteLinearOrder Bool

ink

noncomputable instance Bool.completeBooleanAlgebra : CompleteBooleanAlgebra Bool

Equations

• Bool.completeBooleanAlgebra = Fintype.toCompleteBooleanAlgebra Bool

Directed Orders

ink

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)

ink

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

ink

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 : β → α) : BddAbove (Set.range f)