# 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`

source
@[reducible, inline]
abbrev Fintype.toOrderBot (α : Type u_2) [Fintype α] [Nonempty α] [SemilatticeInf α] :
OrderBot α

Constructs the `⊥` of a finite nonempty `SemilatticeInf`.

Equations

- Fintype.toOrderBot α = { bot := Finset.univ.inf' ⋯ id, bot_le := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Fintype.toOrderTop (α : Type u_2) [Fintype α] [Nonempty α] [SemilatticeSup α] :
OrderTop α

Constructs the `⊤` of a finite nonempty `SemilatticeSup`

Equations

- Fintype.toOrderTop α = { top := Finset.univ.sup' ⋯ id, le_top := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Fintype.toBoundedOrder (α : Type u_2) [Fintype α] [Nonempty α] [Lattice α] :
BoundedOrder α

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

Equations

- Fintype.toBoundedOrder α = { toOrderTop := Fintype.toOrderTop α, toOrderBot := Fintype.toOrderBot α }

Instances For

source
@[reducible, inline]
noncomputable abbrev 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.

Instances For

source
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteDistribLatticeMinimalAxioms (α : Type u_2) [Fintype α] [DistribLattice α] [BoundedOrder α] :
CompleteDistribLattice.MinimalAxioms α

A finite bounded distributive lattice is completely distributive.

Equations

- Fintype.toCompleteDistribLatticeMinimalAxioms α = { toCompleteLattice := Fintype.toCompleteLattice α, inf_sSup_le_iSup_inf := ⋯, iInf_sup_le_sup_sInf := ⋯ }

Instances For

source
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteDistribLattice (α : Type u_2) [Fintype α] [DistribLattice α] [BoundedOrder α] :
CompleteDistribLattice α

A finite bounded distributive lattice is completely distributive.

Equations

- Fintype.toCompleteDistribLattice α = CompleteDistribLattice.ofMinimalAxioms (Fintype.toCompleteDistribLatticeMinimalAxioms α)

Instances For

source
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteLinearOrder (α : Type u_2) [Fintype α] [LinearOrder α] [BoundedOrder α] :
CompleteLinearOrder α

A finite bounded linear order is complete.

If the `α` is already a `BiheytingAlgebra`, then prefer to construct this instance manually using `Fintype.toCompleteLattice` instead, to avoid creating a diamond with `LinearOrder.toBiheytingAlgebra`.

Equations

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

Instances For

source
@[reducible, inline]
noncomputable abbrev 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.

Instances For

source
@[reducible, inline]
noncomputable abbrev Fintype.toCompleteAtomicBooleanAlgebra (α : Type u_2) [Fintype α] [BooleanAlgebra α] :
CompleteAtomicBooleanAlgebra α

A finite Boolean algebra is complete and atomic.

Equations

- Fintype.toCompleteAtomicBooleanAlgebra α = CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra

Instances For

source
@[reducible, inline]
noncomputable abbrev 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 α

Instances For

source
@[reducible, inline]
noncomputable abbrev 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

- Fintype.toCompleteLinearOrderOfNonempty α = Fintype.toCompleteLinearOrder α

Instances For

### Concrete instances #

source
noncomputable instance Fin.completeLinearOrder {n : ℕ} [NeZero n] :
CompleteLinearOrder (Fin n)
Equations

- Fin.completeLinearOrder = Fintype.toCompleteLinearOrder (Fin n)

source
noncomputable instance Bool.completeBooleanAlgebra :
CompleteBooleanAlgebra Bool
Equations

- Bool.completeBooleanAlgebra = Fintype.toCompleteBooleanAlgebra Bool

source
noncomputable instance Bool.completeLinearOrder :
CompleteLinearOrder Bool
Equations

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

source
noncomputable instance Bool.completeAtomicBooleanAlgebra :
CompleteAtomicBooleanAlgebra Bool
Equations

- Bool.completeAtomicBooleanAlgebra = Fintype.toCompleteAtomicBooleanAlgebra Bool

### Directed Orders #

source
theorem Directed.finite_set_le {α : Type u_1} {r : α → α → Prop} [IsTrans α r] {γ : Type u_3} [Nonempty γ] {f : γ → α} (D : Directed r f) {s : Set γ} (hs : s.Finite) :
∃ (z : γ), ∀ i ∈ s, r (f i) (f z)
source
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)
source
theorem Finite.exists_le {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] (f : β → α) :
∃ (M : α), ∀ (i : β), f i ≤ M
source
theorem Finite.exists_ge {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] (f : β → α) :
∃ (M : α), ∀ (i : β), M ≤ f i
source
theorem Set.Finite.exists_le {α : Type u_1} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {s : Set α} (hs : s.Finite) :
∃ (M : α), ∀ i ∈ s, i ≤ M
source
theorem Set.Finite.exists_ge {α : Type u_1} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {s : Set α} (hs : s.Finite) :
∃ (M : α), ∀ i ∈ s, M ≤ i
source
@[simp]
theorem Finite.bddAbove_range {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] (f : β → α) :
BddAbove (Set.range f)
source
@[simp]
theorem Finite.bddBelow_range {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] (f : β → α) :
BddBelow (Set.range f)