Orders

In many areas of mathematics and computer science, we are interested in how elements compare. Can one element be considered less than another? Are two elements incomparable? Such questions motivate the study of orders, which capture various ways of comparing elements.

In this chapter, we begin by examining different kinds of order relations and how they combine to define preorders and partial orders. We’ll look at concrete examples and highlight their differences. We then explore how order structures can be represented formally, particularly within a type-theoretic framework.

The chapter concludes with a series of exercises designed to deepen our understanding and give us hands-on practice with ordered structures.

Preorder

A preorder on a type A is a binary relation on A that is reflexive and transitive.

Preorder.lean

structure Preorder {A : Type} (R : A → A → Prop) : Prop where
  refl : ∀ (a : A), R a a
  trans : ∀ {a b c : A}, R a b → R b c → R a c

The keyword structure introduces a new structured proposition called Preorder, which is simply a collection of logical propositions. It has two fields, refl (reflexivity) and trans (transitivity). Now, statements of the form Preoder R are propositions and thus, can be proven.

Partial Order

A partial order is a preorder that is also antisymmetric.

PartialOrder.lean

structure PartialOrder {A : Type} (R : A → A → Prop) : Prop where
  toPreorder : Preorder R
  antisymm : ∀ {a b : A}, R a b → R b a → a = b

Partially Ordered Set

A partially ordered set (or poset) is a structure consisting of three components: a type base; a binary relation R on base; and a proof that this relation forms a partial order.

Poset.lean

structure Poset where
  base : Type
  R    : base → base → Prop
  toPartialOrder : PartialOrder R

Special Elements

We say that z is a least element with respect to R if R z a, for every a : A. We say that z is a greatest element with respect to R if R a z, for every a : A.

SpecialElements.lean

-- Least
def Least {A : Type} (R : A → A → Prop) (z : A) : Prop := ∀ {a : A}, R z a
-- Greatest
def Greatest {A : Type} (R : A → A → Prop) (z : A) : Prop := ∀ {a : A}, R a z

We say that z is a minimal element with respect to R if, for every a : A, whenever R a z holds, it must follow that a = z. Similarly, we say that z is a maximal element with respect to R if, for every a : A, whenever R z a holds, it must follow that a = z.

SpecialElements.lean

-- Minimal
def Minimal {A : Type} (R : A → A → Prop) (z : A) : Prop := ∀ {a : A}, R a z → a = z
-- Maximal
def Maximal {A : Type} (R : A → A → Prop) (z : A) : Prop :=  ∀ {a : A}, R z a → a = z

Bounded Posets

A bounded poset is a poset that has both a least element and a greatest element.

BoundedPoset.lean

structure BoundedPoset extends Poset where
  l : base
  least : Least R l
  g : base
  greatest : Greatest R g

Special Elements relative to a Subtype

We say that z is an upper bound of a subtype P if it is greater than or equal to every element of Subtype P with respect to the relation R. An upper bound z is called the supremum (or least upper bound) of P if, for any other upper bound x, the relation R z x holds—that is, z is less than or equal to every other upper bound. An element z is the maximum of P if it is both a supremum of P and an actual member of Subtype P.

SpecialElements.lean

-- UpperBound
def UpperBound {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop := 
∀ (a : A), P a → R a z
-- Supremum
structure Supremum {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop where
  -- Upper Bound
  UB : (UpperBound R P z)
  -- Least Upper Bound
  LUB : ∀ (x : A), (UpperBound R P x → R z x)
-- Maximum
structure Maximum {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop where
  -- Supremum
  toSupremum : (Supremum R P z)
  -- In Subtype P
  Sub : P z

Conversely, we say that z is a lower bound of a subtype P if it is smaller than or equal to every element of Subtype P with respect to the relation R. A lower bound z is called the infimum (or greatest lower bound) of P if, for any other lower bound x, the relation R x z holds—that is, z is greater than or equal to every other upper bound. An element z is the minimum of P if it is both an infimum of P and an actual member of Subtype P.

SpecialElements.lean

-- LowerBound
def LowerBound {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop := ∀ (a : A), P a → R z a
-- Infimum
structure Infimum {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop where
  -- Lower Bound
  LB : (LowerBound R P z)
  -- Greatest Lower Bound
  GLB : ∀ (x : A), (LowerBound R P x → R x z)
-- Minimum
structure Minimum {A : Type} (R : A → A → Prop) (P : A → Prop) (z : A) : Prop where
  -- Infimum
  toInfimum : (Infimum R P z)
  -- In Subtype P
  Sub : P z

Lattice

A lattice is an abstract mathematical structure that can be defined in two equivalent ways: either order-theoretically, as a partially ordered set satisfying certain conditions, or algebraically, as a structure equipped with operations that obey specific laws.

Lattice as a poset

A lattice is a partially ordered set in which every pair of elements has a unique supremum (also called the join) and a unique infimum (also called the meet). The following definition introduces a structure Lattice that builds on an existing Poset by adding operations and properties for meet and join. The corresponding fields infimum and supremum are proofs that meet a b and join a b do indeed satisfy the formal definitions of infimum and supremum with respect to the underlying order relation R.

Lattice.lean

@[ext] structure Lattice extends Poset where
  meet : base → base → base
  infimum : ∀ {a b : base}, Infimum R (fun (x : base) => (x = a) ∨ (x = b)) (meet a b)
  join : base → base → base
  supremum : ∀ {a b : base}, Supremum R (fun (x : base) => (x = a) ∨ (x = b)) (join a b)

The @[ext] attribute is a convenience provided by Lean’s metaprogramming framework. It automatically generates an extensionality lemma for the structure, allowing users to prove equality between two lattice instances by showing that all their corresponding components are equal. In practice, this means that to show two lattices are equal, it suffices to prove that their base types and the relations on them are the same, and that the meet and join operations agree on all inputs. This can simplify proofs and reasoning about structures built on top of Lattice, as we will see below.

Lattice as an algebra

An alternative way to describe a lattice is as an algebraic structure consisting of a base type equipped with two binary operations, meet and join. These operations are required to be commutative and associative, and they must satisfy the absorption laws, as described below.

LatticeAlg.lean

@[ext] structure LatticeAlg where
  base : Type
  meet : base → base → base
  join : base → base → base
  meetcomm : ∀ {a b : base}, meet a b = meet b a
  joincomm : ∀ {a b : base}, join a b = join b a
  meetass  : ∀ {a b c : base}, meet (meet a b) c = meet a (meet b c)
  joinass  : ∀ {a b c : base}, join (join a b) c = join a (join b c)
  abslaw1  : ∀ {a b : base}, join a (meet a b) = a
  abslaw2  : ∀ {a b : base}, meet a (join a b) = a

This algebraic perspective is equivalent to the order-theoretic definition and emphasizes the operational behavior of meets and joins rather than their characterization via suprema and infima.

There are usually 2 more laws regarding the idempotency of the meet and join operations that can be derived from the other axioms.

LatticeAlg.lean

-- meet is idempotent
theorem meetidpt {C : LatticeAlg} : ∀ (a : C.base), C.meet a a = a := by
  intro a
  calc
    C.meet a a = C.meet a (C.join a (C.meet a a)) := congrArg (C.meet a) C.abslaw1.symm
    _          = a                                := C.abslaw2

-- join is idempotent
theorem joinidpt {C : LatticeAlg} : ∀ (a : C.base), C.join a a = a := by
  intro a
  calc
    C.join a a = C.join a (C.meet a (C.join a a)) := congrArg (C.join a) C.abslaw2.symm
    _          = a                                := C.abslaw1

The following result will be of interest later.

LatticeAlg.lean

theorem meetjoin {C : LatticeAlg} : ∀ {a b : C.base}, (C.meet a b = a) ↔ (C.join a b = b) := by
  intro a b
  apply Iff.intro
  -- C.meet a b = a → C.join a b = b
  intro h
  rw [C.meetcomm] at h
  rw [C.joincomm, h.symm]
  exact C.abslaw1
  -- C.join a b = b → C.meet a b = a
  intro h
  rw [h.symm]
  exact C.abslaw2

From Lattice to LatticeAlg

Any Lattice structure naturally induces a corresponding LatticeAlg structure on its underlying base type with the meet and join operations from the lattice. The proof below demonstrates this construction, using the refine keyword to explicitly specify the values of all required LatticeAlg fields.

LatticetoLatticeAlg.lean

def LatticetoLatticeAlg : Lattice → LatticeAlg := by
  intro C
  refine {
    base := C.base,
    meet := C.meet,
    join := C.join,
    meetcomm := by
      intro a b
      apply C.toPoset.toPartialOrder.antisymm
      -- C.R (C.meet a b) (C.meet b a)
      apply C.infimum.GLB
      intro z h
      cases h
      -- b
      rename_i hz
      apply C.infimum.LB
      exact Or.inr hz
      -- a
      rename_i hz
      apply C.infimum.LB
      exact Or.inl hz
      -- C.R (C.meet b a) (C.meet a b)
      apply C.infimum.GLB
      intro z h
      cases h
      -- a
      rename_i hz
      apply C.infimum.LB
      exact Or.inr hz
      -- b
      rename_i hz
      apply C.infimum.LB
      exact Or.inl hz
    joincomm := by
      intro a b
      apply C.toPoset.toPartialOrder.antisymm
      -- C.R (C.join a b) (C.join b a)
      apply C.supremum.LUB
      intro z h
      cases h
      -- a
      rename_i hz
      apply C.supremum.UB
      exact Or.inr hz
      -- b
      rename_i hz
      apply C.supremum.UB
      exact Or.inl hz
      -- C.R (C.join b a) (C.join a b)
      apply C.supremum.LUB
      intro z h
      cases h
      -- b
      rename_i hz
      apply C.supremum.UB
      exact Or.inr hz
      -- a
      rename_i hz
      apply C.supremum.UB
      exact Or.inl hz
    meetass := by
      intro a b c
      apply C.toPoset.toPartialOrder.antisymm
      -- C.R (C.meet (C.meet a b) c) (C.meet a (C.meet b c))
      apply C.infimum.GLB
      intro z h
      cases h
      -- a
      rename_i hz
      have h1 : C.R (C.meet (C.meet a b) c) (C.meet a b) := by
        apply C.infimum.LB
        exact Or.inl rfl
      have h2 : C.R (C.meet a b) z := by
        apply C.infimum.LB
        exact Or.inl hz
      exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
      -- C.meet b c
      rename_i hz
      rw [hz]
      apply C.infimum.GLB
      intro d hd
      cases hd
      -- b
      rename_i hd
      rw [hd]
      have h1 : C.R (C.meet (C.meet a b) c) (C.meet a b) := by
        apply C.infimum.LB
        exact Or.inl rfl
      have h2 : C.R (C.meet a b) b := by
        apply C.infimum.LB
        exact Or.inr rfl
      exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
      -- c
      rename_i hd
      apply C.infimum.LB
      exact Or.inr hd
      -- C.R (C.meet a (C.meet b c)) (C.meet (C.meet a b) c)
      apply C.infimum.GLB
      intro z h
      cases h
      -- C.meet a b
      rename_i hz
      rw [hz]
      apply C.infimum.GLB
      intro d hd
      cases hd
      -- a
      rename_i hd
      apply C.infimum.LB
      exact Or.inl hd
      -- b
      rename_i hd
      rw [hd]
      have h1 : C.R (C.meet a (C.meet b c)) (C.meet b c) := by
        apply C.infimum.LB
        exact Or.inr rfl
      have h2 : C.R (C.meet b c) b := by
        apply C.infimum.LB
        exact Or.inl rfl
      exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
      -- c
      rename_i hz
      have h1 : C.R (C.meet a (C.meet b c)) (C.meet b c) := by
        apply C.infimum.LB
        exact Or.inr rfl
      have h2 : C.R (C.meet b c) z := by
        apply C.infimum.LB
        exact Or.inr hz
      exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
    joinass := by
      intro a b c
      apply C.toPoset.toPartialOrder.antisymm
      -- C.R (C.join (C.join a b) c) (C.join a (C.join b c))
      apply C.supremum.LUB
      intro z h
      cases h
      -- C.join a b
      rename_i hz
      rw [hz]
      apply C.supremum.LUB
      intro d hd
      cases hd
      -- a
      rename_i hd
      apply C.supremum.UB
      exact Or.inl hd
      -- b
      rename_i hd
      have h1 : C.R d (C.join b c) := by
        apply C.supremum.UB
        exact Or.inl hd
      have h2 : C.R (C.join b c) (C.join a (C.join b c)) := by
        apply C.supremum.UB
        exact Or.inr rfl
      exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
      -- c
      rename_i hz
      have h1 : C.R z (C.join b c) := by
        apply C.supremum.UB
        exact Or.inr hz
      have h2 : C.R (C.join b c) (C.join a (C.join b c)) := by
        apply C.supremum.UB
        exact Or.inr rfl
      exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
      -- C.R (C.join a (C.join b c)) (C.join (C.join a b) c)
      apply C.supremum.LUB
      intro z h
      cases h
      -- a
      rename_i hz
      have h1 : C.R z (C.join a b) := by
        apply C.supremum.UB
        exact Or.inl hz
      have h2 : C.R (C.join a b) (C.join (C.join a b) c) := by
        apply C.supremum.UB
        exact Or.inl rfl
      exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
      -- C.join b c
      rename_i hz
      rw [hz]
      apply C.supremum.LUB
      intro d hd
      cases hd
      -- b
      rename_i hd
      have h1 : C.R d (C.join a b) := by
        apply C.supremum.UB
        exact Or.inr hd
      have h2 : C.R (C.join a b) (C.join (C.join a b) c) := by
        apply C.supremum.UB
        exact Or.inl rfl
      exact C.toPoset.toPartialOrder.toPreorder.trans h1 h2
      -- c
      rename_i hd
      apply C.supremum.UB
      exact Or.inr hd
    abslaw1 := by
      intro a b
      apply C.toPoset.toPartialOrder.antisymm
      -- C.R (C.join a (C.meet a b)) a
      apply C.supremum.LUB
      intro d hd
      cases hd
      -- a
      rename_i hd
      rw [hd]
      apply C.toPoset.toPartialOrder.toPreorder.refl
      -- C.meet a b
      rename_i hd
      rw [hd]
      apply C.infimum.LB
      exact Or.inl rfl
      -- C.R a (C.join a (C.meet a b))
      apply C.supremum.UB
      exact Or.inl rfl
    abslaw2 := by
      intro a b
      apply C.toPoset.toPartialOrder.antisymm
      -- C.R (C.meet a (C.join a b)) a
      apply C.infimum.LB
      exact Or.inl rfl
      -- C.R a (C.meet a (C.join a b))
      apply C.infimum.GLB
      intro d hd
      cases hd
      -- a
      rename_i hd
      rw [hd]
      apply C.toPoset.toPartialOrder.toPreorder.refl
      -- C.join a b
      rename_i hd
      rw [hd]
      apply C.supremum.UB
      exact Or.inl rfl
  }

From LatticeAlg to Lattice

Conversely, every LatticeAlg structure gives rise to a corresponding Lattice structure on its underlying base type. The construction begins by defining a partial order LAR on the base, as shown below. We will say that a ≤ b if, and only if, meet a b = a.

LatticeAlgtoLattice.lean

def LAR {C : LatticeAlg} : C.base → C.base → Prop := by
  intro a b
  exact C.meet a b = a

The relation LAR is a Preorder.

LatticeAlgtoLattice.lean

theorem TLARPreorder {C : LatticeAlg} : Preorder (@LAR C) := by
  apply Preorder.mk
  -- refl
  intro a
  rw [LAR]
  exact meetidpt a
  -- trans
  intro a b c h1 h2
  rw [LAR] at *
  rw [h1.symm, C.meetass, h2]

The relation LAR is a PartialOrder.

LatticeAlgtoLattice.lean

theorem TLARPartialOrder {C : LatticeAlg} : PartialOrder (@LAR C) := by
  apply PartialOrder.mk
  -- toPreorder
  exact TLARPreorder
  -- antisymm
  intro a b h1 h2
  calc
    a = C.meet a b := h1.symm
    _ = C.meet b a := C.meetcomm
    _ = b          := h2

In summary, we are now ready to prove that every LatticeAlg structure induces a corresponding Lattice structure on its base type, preserving the same meet and join operations.

LatticeAlgtoLattice.lean

def LatticeAlgtoLattice : LatticeAlg → Lattice := by
  intro C
  refine {
    toPoset := {
      base := C.base,
      R := @LAR C,
      toPartialOrder := TLARPartialOrder
    }
    meet := C.meet,
    infimum := by
      intro a b
      apply Infimum.mk
      -- LowerBound
      intro z hz
      cases hz
      -- a
      rename_i hz
      rw [hz]
      have h1 : C.meet (C.meet a b) a = (C.meet a b) := by
        calc
          C.meet (C.meet a b) a = C.meet a (C.meet a b) := C.meetcomm.symm
          _                     = C.meet (C.meet a a) b := C.meetass.symm
          _                     = C.meet a b            := congrArg (fun x => C.meet x b) (meetidpt a)
      exact h1
      -- b
      rename_i hz
      rw [hz]
      have h1 : C.meet (C.meet a b) b = (C.meet a b) := by
        calc
          C.meet (C.meet a b) b = C.meet a (C.meet b b) := C.meetass
          _                     = C.meet a b            := congrArg (fun x => C.meet a x) (meetidpt b)
      exact h1
      -- Greatest LowerBound
      intro x h
      have ha : C.meet x a = x := by
        apply h
        exact Or.inl rfl
      have hb : C.meet x b = x := by
        apply h
        exact Or.inr rfl
      have h1 : C.meet x (C.meet a b) = x := by
        calc
          C.meet x (C.meet a b) = C.meet (C.meet x a) b := C.meetass.symm
          _                     = C.meet x b            := congrArg (fun z => C.meet z b) ha
          _                     = x                     := hb
      exact h1
    join := C.join,
    supremum := by
      intro a b
      apply Supremum.mk
      -- UpperBound
      intro z hz
      cases hz
      -- a
      rename_i hz
      rw [hz]
      exact C.abslaw2
      -- b
      rename_i hz
      rw [hz, C.joincomm]
      exact C.abslaw2
      -- Least UpperBound
      intro x h
      have ha : C.meet a x = a := by
        apply h
        exact Or.inl rfl
      have hb : C.meet b x = b := by
        apply h
        exact Or.inr rfl
      have hax : C.join a x = x := meetjoin.mp ha
      have hbx : C.join b x = x := meetjoin.mp hb
      have h1 : C.join (C.join a b) x = x := by
        calc
          C.join (C.join a b) x = C.join a (C.join b x) := C.joinass
          _                     = C.join a x            := congrArg (fun z => C.join a z) hbx
          _                     = x                     := hax
      exact meetjoin.mpr h1
  }

Compositions

The ext attribute now allows us to prove that the two constructions defined above are mutually inverse.

LatticeAlgtoLattice ∘ LatticetoLatticeAlg = id

Compositions.lean

theorem TIdLattice : LatticeAlgtoLattice ∘ LatticetoLatticeAlg = id := by
  funext C
  apply Lattice.ext
  -- base
  exact rfl
  -- R
  have hR : (LatticeAlgtoLattice (LatticetoLatticeAlg C)).R = C.R := by
    funext a b
    apply propext
    apply Iff.intro
    -- ((LatticeAlgtoLattice ∘ LatticetoLatticeAlg) C).R a b → C.R a b
    intro h
    have hs : C.meet a b = a := h
    rw [hs.symm]
    apply C.infimum.LB
    exact Or.inr rfl
    -- C.R a b → (LatticeAlgtoLattice (LatticetoLatticeAlg C)).R a b
    intro h
    have hs : C.meet a b = a := by
      apply C.toPoset.toPartialOrder.antisymm
      -- C.R (C.meet a b) a
      apply C.infimum.LB
      exact Or.inl rfl
      -- C.R a (C.meet a b)
      apply C.infimum.GLB
      intro z hz
      cases hz
      -- a
      rename_i hz
      rw [hz]
      exact C.toPoset.toPartialOrder.toPreorder.refl a
      -- b
      rename_i hz
      rw [hz]
      exact h
    exact hs
  exact heq_of_eq hR
  -- meet
  exact HEq.refl C.meet
  -- join
  exact HEq.refl C.join

LatticetoLatticeAlg ∘ LatticeAlgtoLattice = id

Compositions.lean

theorem TIdLatticeAlg : LatticetoLatticeAlg ∘ LatticeAlgtoLattice = id := by
  funext C
  apply LatticeAlg.ext
  -- base
  exact rfl
  -- meet
  exact HEq.refl C.meet
  -- join
  exact HEq.refl C.join

Distributive Lattice

A distributive lattice is a lattice satisfying an extra law regarding the distributivity of meet over join.

DistLatticeAlg.lean

@[ext] structure DistLatticeAlg extends LatticeAlg where
  dist : ∀ {a b c : base}, meet a (join b c) = join (meet a b) (meet a c)

Complete Lattice

A complete lattice is a partially ordered set in which every subtype has both an infimum, that we will call meet, and a supremum, that we will call join.

CompleteLattice.lean

structure CompleteLattice extends Poset where
  meet : (base → Prop) → base
  infimum : ∀ {P : base → Prop}, Infimum R P (meet P)
  join : (base → Prop) → base
  supremum : ∀ {P : base → Prop}, Supremum R P (join P)

From CompleteLattice to Lattice

Clearly, every CompleteLattice is, in particular, a Lattice.

CompleteLattice.lean

def CompleteLatticetoLattice : CompleteLattice → Lattice := by
  intro C
  refine {
    toPoset := C.toPoset,
    meet := (fun a b => C.meet (fun (x : C.base) => (x = a) ∨ (x = b))),
    infimum := fun {a b} => C.infimum
    join := (fun a b => C.join (fun (x : C.base) => (x = a) ∨ (x = b))),
    supremum := fun {a b} => C.supremum
  }

From CompleteLattice to BoundedPoset

Also, every CompleteLattice is, in particular, a BoundedPoset. To prove this fact, we need to prove that the supremum of the PFalse predicate is, precisely, the Least element (exercise) and the infimum of the PFalse predicate is, precisely, the Greatest element (exercise). Thus, every CompleteLattice, which has both infima and suprema for all subtypes, contains a least and a greatest element, i.e., is a BoundedPoset.

CompleteLattice.lean

def CompleteLatticetoBoundedPoset : CompleteLattice → BoundedPoset := by
  intro C
  refine {
    toPoset := C.toPoset,
    l := C.join (PFalse),
    least := (TLeastSupPFalse C.R (C.join PFalse)).mpr (C.supremum)
    g := C.meet (PFalse),
    greatest := (TGreatestInfPFalse C.R (C.meet PFalse)).mpr (C.infimum)
  }

Exercises

Inverse Partial Order

Exercises.lean

-- If `R` is a preorder, then the inverse relation `R^` is also a preorder
theorem TPreorderInv {A : Type} (R : A → A → Prop) : Preorder R → 
Preorder (inverse R) := by sorry

-- If `R` is a partial order, then the inverse relation `R^` is also a partial order
theorem TPartialOrderInv {A : Type} (R : A → A → Prop) : PartialOrder R → 
PartialOrder (inverse R) := by sorry

Special Elements

Exercises.lean

-- If `R` is a partial order and `z1` and `z2` are `least` elements, then they are equal.
theorem LeastUnique {A : Type} (R : A → A → Prop) (z1 z2 : A) (h : PartialOrder R) 
(h1 : Least R z1) (h2 : Least R z2) : z1 = z2 := by sorry

-- If `R` is a partial order and `z1` and `z2` are `greatest` elements, then they are equal.
theorem GreatestUnique {A : Type} (R : A → A → Prop) (z1 z2 : A) (h : PartialOrder R) 
(h1 : Greatest R z1) (h2 : Greatest R z2) : z1 = z2  := by sorry

-- If `R` is a partial order and `z` is the least element, then it is a minimal element
def LeasttoMinimal {A : Type} (R : A → A → Prop) (z : A) (h : PartialOrder R) : 
Least R z → Minimal R z := by sorry

-- If `R` is a partial order and `z` is the greatest element, then it is a maximal element
def GreatesttoMaximal {A : Type} (R : A → A → Prop) (z : A) (h : PartialOrder R) : 
Greatest R z → Maximal R z := by sorry

-- A least element for `R` is a greatest element for `R^`
def LeasttoGreatestInv {A : Type} (R : A → A → Prop) (z : A) : Least R z → 
Greatest (inverse R) z := by sorry

-- A greatest element for `R` is a least element for `R^`
def GreatesttoLeastInv {A : Type} (R : A → A → Prop) (z : A) : Greatest R z → 
Least (inverse R) z := by sorry

-- A minimal element for `R` is a maximal element for `R^`
def MinimaltoMaximalInv {A : Type} (R : A → A → Prop) (z : A) : Minimal R z → 
Maximal (inverse R) z := by sorry

-- A maximal element for `R` is a minimal element for `R^`
def MaximaltoMinimalInv {A : Type} (R : A → A → Prop) (z : A) : Maximal R z → 
Minimal (inverse R) z := by sorry

Restriction

Exercises.lean

-- The `Restriction` of a relation to a Subtype
def Restriction {A : Type} (R : A → A → Prop) (P : A → Prop) : 
Subtype P → Subtype P → Prop := by
  intro a1 a2
  exact R a1.val a2.val
  
-- If `R` is a preorder then `Restriction R P`, for a predicate `P`, is a preorder
theorem TPRestriction {A : Type} (R : A → A → Prop) (P : A → Prop) : 
Preorder R → Preorder (Restriction R P) := by sorry

-- If `R` is a partial order then `Restriction R P`, for a predicate `P`, is a partial ordre
theorem TPORestriction {A : Type} (R : A → A → Prop) (P : A → Prop) : 
PartialOrder R → PartialOrder (Restriction R P) := by sorry

Special Elements relative to a Subtype

Exercises.lean

-- The supremum of the False predicate is the least element
theorem TLeastSupPFalse {A : Type} (R : A → A → Prop) (z : A) : 
Least R z ↔ Supremum R PFalse z := by sorry

-- The infimum of the False predicate is the greatest element
theorem TGreatestInfPFalse {A : Type} (R : A → A → Prop) (z : A) : 
Greatest R z ↔ Infimum R PFalse z := by sorry
  
-- The infimum of the True predicate is the least element
theorem TLeastInfPTrue {A : Type} (R : A → A → Prop) (z : A) : 
Least R z ↔ Infimum R PTrue z := by sorry

-- The supremum of the True predicate is the greatest element
theorem TGreatestSupPTrue {A : Type} (R : A → A → Prop) (z : A) : 
Greatest R z ↔ Supremum R PTrue z := by sorry

(N, ≤)

Exercises.lean

-- The `≤` relation for `N`
def NLeq : N → N → Prop := by
  intro n m
  exact ∃ (k : N), n + k = m

-- Notation for `≤`
notation : 65 lhs:65 " ≤ " rhs:66 => NLeq lhs rhs

-- `≤` is a preorder
theorem TPreorderNLeq : Preorder NLeq := by sorry

-- `≤` is a partial order
theorem TPartialOrderNLeq : PartialOrder NLeq := by sorry

-- `(N, ≤)` is a partially ordered type
def instPosetNLeq : Poset := by sorry

-- `z` is the least element
theorem TNLeqzL : ∀ {n : N}, z ≤ n := by sorry

-- No `s n` is below `z`
theorem TNLeqzR : ∀ {n : N}, ¬ (s n ≤ z) := by sorry

-- If `n ≤ m` then `s n ≤ s m`
theorem TNLeqSuccT : ∀ {n m : N}, (n ≤ m) → (s n ≤ s m) := by sorry

-- If `n ≰ m` then `s n ≰ s m`
theorem TNLeqSuccF : ∀ {n m : N}, (¬ (n ≤ m)) → (¬ (s n ≤ s m)) := by sorry

-- `≤` is decidable
def instDecidableNLeq : ∀ {n m : N}, Decidable (n ≤ m) := by sorry

-- `min n m` is a lower bound of `n`
theorem TMinNLeqL : ∀ {n m : N}, (mini n m) ≤ n := by sorry

-- `min n m` is a lower bound of `m`
theorem TMinNLeqR : ∀ {n m : N}, (mini n m) ≤ m := by sorry

-- `min n m` is the infimum for `n` and `m`
theorem TInfNLeq : ∀ {n m : N}, Infimum NLeq (fun (x : N) => (x = n) ∨ (x = m))
(mini n m) := by sorry
  
-- `max n m` is an upper bound of `n`
theorem TMaxNLeqL : ∀ {n m : N}, n ≤ (maxi n m) := by sorry

-- `max n m` is an upper bound of `m`
theorem TMaxNLeqR : ∀ {n m : N}, m ≤ (maxi n m) := by sorry

-- `max n m` is the supremum of `n` and `m`
theorem TSupNLeq : ∀ {n m : N}, Supremum NLeq (fun (x : N) => (x = n) ∨ (x = m)) 
(maxi n m) := by sorry

-- `(N, ≤)` is a lattice
def instLatticeNLeq : Lattice := by sorry

-- `min n (max m p) = max (min n m) (min n p)`
theorem TDistNLeq : ∀ {n m p : N}, mini n (maxi m p) = maxi (mini n m) (mini n p) 
:= by sorry
  
-- `(N,≤)` is a distributive lattice
def instDistLatticeAlgNLeq : DistLatticeAlg := by sorry

(N, ∣)

Exercises.lean

-- The `∣` (divisor) relation for `N`
def NDiv : N → N → Prop := by
  intro n m
  exact ∃ (k : N), n * k = m
  
-- Notation for divisor (`\mid`)
notation : 65 lhs:65 " ∣ " rhs:66 => NDiv lhs rhs

-- `∣` is a preorder
theorem TPreorderNDiv : Preorder NDiv := by sorry

-- `∣` is a partial order
theorem TPartialOrderNDiv : PartialOrder NDiv := by sorry

-- `(N, ∣)` is a partially ordered type
def instPosetNDiv : Poset := by sorry

-- `one` is the `least` element for `∣`
theorem TNDivOne : Least NDiv one := by sorry

-- `z` is the `greatest` element for `∣`
theorem TNDivZ : Greatest NDiv z := by sorry

-- `(N, ∣)` is a bounded partially ordered type
def instBoundedPosetNDiv : BoundedPoset := by sorry

-- `z` does not divide any successor
theorem TNDivzL : ∀ {n : N}, ¬ (z ∣ s n) := by sorry

-- `(N, ∣)` is a lattice
def instLatticeNDiv : Lattice := by sorry

(Prop, →)

Exercises.lean

-- The `→` relation for `Prop`
def PropLeq : Prop → Prop → Prop := by
  intro P Q
  exact P → Q

-- `→` is a preorder
theorem TPreorderPropLeq : Preorder PropLeq := by sorry

-- `→` is a partial order
theorem TPartialOrderPropLeq : PartialOrder PropLeq := by sorry

-- `(Prop, →)` is a partially ordered type
def instPosetPropLeq : Poset := by sorry

-- `False` is the `least` element for `→`
theorem TPropLeqFalse : Least PropLeq False := by sorry

-- `True` is the `greatest` element for `→`
theorem TPropLeqTrue : Greatest PropLeq True := by sorry

-- `(Prop, →)` is a bounded partially ordered type
def instBoundedPropLeq : BoundedPoset := by sorry

-- `(Prop, ∧, ∨)` is a lattice (as an algebra)
def instLatticeAlgProp : LatticeAlg := by sorry

-- `(Prop, →)` is a complete lattice
def instCompleteLatticeProp : CompleteLattice := by sorry