# 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, inline]
abbrev Fintype.toOrderBot (α : Type u_2) [] [] [] :

Constructs the ⊥ of a finite nonempty SemilatticeInf.

Equations
Instances For
@[reducible, inline]
abbrev Fintype.toOrderTop (α : Type u_2) [] [] [] :

Constructs the ⊤ of a finite nonempty SemilatticeSup

Equations
Instances For
@[reducible, inline]
abbrev Fintype.toBoundedOrder (α : Type u_2) [] [] [] :

Constructs the ⊤ and ⊥ of a finite nonempty Lattice.

Equations
• = BoundedOrder.mk
Instances For
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteLattice (α : Type u_2) [] [] [] :

A finite bounded lattice is complete.

Equations
Instances For
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteDistribLatticeMinimalAxioms (α : Type u_2) [] [] [] :

A finite bounded distributive lattice is completely distributive.

Equations
• = { toCompleteLattice := , inf_sSup_le_iSup_inf := , iInf_sup_le_sup_sInf := }
Instances For
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteDistribLattice (α : Type u_2) [] [] [] :

A finite bounded distributive lattice is completely distributive.

Equations
Instances For
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteLinearOrder (α : Type u_2) [] [] [] :

A finite bounded linear order is complete.

Equations
• = CompleteLinearOrder.mk LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT
Instances For
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteBooleanAlgebra (α : Type u_2) [] [] :

A finite boolean algebra is complete.

Equations
Instances For
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteAtomicBooleanAlgebra (α : Type u_2) [] [] :

A finite boolean algebra is complete and atomic.

Equations
• = CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra
Instances For
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteLatticeOfNonempty (α : Type u_2) [] [] [] :

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
Instances For
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteLinearOrderOfNonempty (α : Type u_2) [] [] [] :

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
• = CompleteLinearOrder.mk LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT
Instances For

### Properties for PartialOrders #

theorem Finite.exists_ge_minimal {α : Type u_1} [] [] {a : α} {p : αProp} (h : p a) :
ba, Minimal p b
theorem Finite.exists_le_maximal {α : Type u_1} [] [] {a : α} {p : αProp} (h : p a) :
∃ (b : α), a b Maximal p b

### Concrete instances #

noncomputable instance Fin.completeLinearOrder {n : } [] :
Equations
• Fin.completeLinearOrder =
noncomputable instance Bool.completeLinearOrder :
Equations
noncomputable instance Bool.completeBooleanAlgebra :
Equations
noncomputable instance Bool.completeAtomicBooleanAlgebra :
Equations

### Directed Orders #

theorem Directed.finite_set_le {α : Type u_1} {r : ααProp} [IsTrans α r] {γ : Type u_3} [] {f : γα} (D : Directed r f) {s : Set γ} (hs : s.Finite) :
∃ (z : γ), is, r (f i) (f z)
theorem Directed.finite_le {α : Type u_1} {r : ααProp} [IsTrans α r] {β : Type u_2} {γ : Type u_3} [] {f : γα} [] (D : Directed r f) (g : βγ) :
∃ (z : γ), ∀ (i : β), r (f (g i)) (f z)
theorem Finite.exists_le {α : Type u_1} {β : Type u_2} [] [] [] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :
∃ (M : α), ∀ (i : β), f i M
theorem Finite.exists_ge {α : Type u_1} {β : Type u_2} [] [] [] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :
∃ (M : α), ∀ (i : β), M f i
theorem Set.Finite.exists_le {α : Type u_1} [] [] [IsDirected α fun (x1 x2 : α) => x1 x2] {s : Set α} (hs : s.Finite) :
∃ (M : α), is, i M
theorem Set.Finite.exists_ge {α : Type u_1} [] [] [IsDirected α fun (x1 x2 : α) => x1 x2] {s : Set α} (hs : s.Finite) :
∃ (M : α), is, M i
@[simp]
theorem Finite.bddAbove_range {α : Type u_1} {β : Type u_2} [] [] [] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :
@[simp]
theorem Finite.bddBelow_range {α : Type u_1} {β : Type u_2} [] [] [] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :
@[deprecated Directed.finite_le]
theorem Directed.fintype_le {α : Type u_1} {r : ααProp} [IsTrans α r] {β : Type u_2} {γ : Type u_3} [] {f : γα} [] (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} [] [] [] [IsDirected α fun (x1 x2 : α) => x1 x2] (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} [] [] [] [IsDirected α fun (x1 x2 : α) => x1 x2] (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} [] [] [] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :

Alias of Finite.bddAbove_range.

@[deprecated Finite.bddBelow_range]
theorem Fintype.bddBelow_range {α : Type u_1} {β : Type u_2} [] [] [] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :

Alias of Finite.bddBelow_range.