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.

Equations

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

@[reducible]

def Fintype.toOrderTop (α : Type u_2) [Fintype α] [Nonempty α] [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)

@[reducible]

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

Constructs the ⊤ and ⊥ of a finite nonempty Lattice.

Equations

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

@[reducible]

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

A finite bounded lattice is complete.

Equations

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

@[reducible]

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

A finite bounded distributive lattice is completely distributive.

Equations

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

@[reducible]

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

A finite bounded linear order is complete.

Equations

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

@[reducible]

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

A finite boolean algebra is complete.

Equations

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

@[reducible]

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

A finite boolean algebra is complete and atomic.

Equations

• Fintype.toCompleteAtomicBooleanAlgebra α = CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra

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

Equations

• Fintype.toCompleteLatticeOfNonempty α = Fintype.toCompleteLattice α

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

Equations

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

Concrete instances

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

Equations

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

noncomputable instance Bool.completeLinearOrder : CompleteLinearOrder Bool

Equations

• Bool.completeLinearOrder = Fintype.toCompleteLinearOrder Bool

noncomputable instance Bool.completeBooleanAlgebra : CompleteBooleanAlgebra Bool

Equations

• Bool.completeBooleanAlgebra = Fintype.toCompleteBooleanAlgebra Bool

noncomputable instance Bool.completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra Bool

Equations

• Bool.completeAtomicBooleanAlgebra = Fintype.toCompleteAtomicBooleanAlgebra Bool

Directed Orders

theorem Directed.finite_set_le {α : Type u_1} {r : α → α → Prop} [IsTrans α r] {γ : Type u_3} [Nonempty γ] {f : γ → α} (D : Directed r f) {s : Set γ} (hs : Set.Finite s) : ∃ (z : γ), ∀ i ∈ s, r (f i) (f z)

theorem Directed.finite_le {α : Type u_1} {r : α → α → Prop} [IsTrans α r] {β : Type u_2} {γ : Type u_3} [Nonempty γ] {f : γ → α} [Finite β] (D : Directed r f) (g : β → γ) : ∃ (z : γ), ∀ (i : β), r (f (g i)) (f z)

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

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

theorem Set.Finite.exists_le {α : Type u_1} [Nonempty α] [Preorder α] [IsDirected α fun (x x_1 : α) => x ≤ x_1] {s : Set α} (hs : Set.Finite s) : ∃ (M : α), ∀ i ∈ s, i ≤ M

theorem Set.Finite.exists_ge {α : Type u_1} [Nonempty α] [Preorder α] [IsDirected α fun (x x_1 : α) => x ≥ x_1] {s : Set α} (hs : Set.Finite s) : ∃ (M : α), ∀ i ∈ s, M ≤ i

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

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

@[deprecated Directed.finite_le]

theorem Directed.fintype_le {α : Type u_1} {r : α → α → Prop} [IsTrans α r] {β : Type u_2} {γ : Type u_3} [Nonempty γ] {f : γ → α} [Finite β] (D : Directed r f) (g : β → γ) : ∃ (z : γ), ∀ (i : β), r (f (g i)) (f z)

Alias of Directed.finite_le.

@[deprecated Finite.exists_le]

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

Alias of Finite.exists_le.

@[deprecated Finite.exists_ge]

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

Alias of Finite.exists_ge.

@[deprecated Finite.bddAbove_range]

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

Alias of Finite.bddAbove_range.

@[deprecated Finite.bddBelow_range]

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

Alias of Finite.bddBelow_range.