The complete lattice of preorders on a type

The preorders on a type, ordered by inclusion of their relations, form a complete lattice, as the equivalence relations on a type do (Setoid.completeLattice). The top preorder relates every two elements, the bottom preorder is equality, and the infimum of a family relates two elements when every member of the family does.

Main definitions

• Preorder.ofLE: the preorder of a reflexive transitive relation.
• Preorder.instCompleteLattice: the complete lattice of preorders on a type.

Implementation notes

[UPSTREAM] candidate: mathlib orders Setoid α in Mathlib.Data.Setoid.Basic but not Preorder α. ofLE supplies the strict order because the default proof of lt_iff_le_not_ge fails when the relation is assembled from another preorder's ≤, as the meet's is.

Instance search keys the DecidableRel instances of ⊤ and ⊥ on ≤ alone, so the instance of ⊥ also decides any preorder whose relation unfolds to an equation, such as r a b = true for a Bool-valued r. A preorder given as a term needs its own instance.

@[reducible]

def Preorder.ofLE {α : Type u_1} (r : α → α → Prop) (hrefl : ∀ (a : α), r a a) (htrans : ∀ (a b c : α), r a b → r b c → r a c) : Preorder α

The preorder of a reflexive transitive relation, with a < b ↔ a ≤ b ∧ ¬ b ≤ a.

Equations

• Preorder.ofLE r hrefl htrans = { le := r, le_refl := hrefl, le_trans := htrans, lt_iff_le_not_ge := ⋯ }

@[instance_reducible]

instance Preorder.instLE_linglib {α : Type u_1} : LE (Preorder α)

Preorders are ordered by inclusion: p ≤ q when q relates every pair that p does.

Equations

• Preorder.instLE_linglib = { le := fun (p q : Preorder α) => ∀ ⦃a b : α⦄, a ≤ b → a ≤ b }

theorem Preorder.le_def {α : Type u_1} {p q : Preorder α} : p ≤ q ↔ ∀ ⦃a b : α⦄, a ≤ b → a ≤ b

@[instance_reducible]

instance Preorder.instPartialOrder_linglib {α : Type u_1} : PartialOrder (Preorder α)

Equations

• Preorder.instPartialOrder_linglib = { toLE := Preorder.instLE_linglib, lt := fun (p q : Preorder α) => p ≤ q ∧ ¬q ≤ p, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[instance_reducible]

instance Preorder.instInfSet_linglib {α : Type u_1} : InfSet (Preorder α)

Equations

• Preorder.instInfSet_linglib = { sInf := fun (S : Set (Preorder α)) => Preorder.ofLE (fun (a b : α) => ∀ p ∈ S, a ≤ b) ⋯ ⋯ }

@[instance_reducible]

instance Preorder.instCompleteLattice {α : Type u_1} : CompleteLattice (Preorder α)

Equations

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

@[simp]

theorem Preorder.top_le {α : Type u_1} (a b : α) : a ≤ b

@[simp]

theorem Preorder.bot_le_iff {α : Type u_1} {a b : α} : a ≤ b ↔ a = b

@[instance_reducible]

instance Preorder.instDecidableRelLe_linglib {α : Type u_1} : DecidableRel LE.le

Equations

• Preorder.instDecidableRelLe_linglib x✝¹ x✝ = isTrue trivial

@[instance_reducible]

instance Preorder.instDecidableRelLeOfDecidableEq_linglib {α : Type u_1} [DecidableEq α] : DecidableRel LE.le

Equations

• Preorder.instDecidableRelLeOfDecidableEq_linglib a b = decEq a b

theorem Preorder.inf_iff_and {α : Type u_1} {p q : Preorder α} {a b : α} : a ≤ b ↔ a ≤ b ∧ a ≤ b

theorem Preorder.sInf_iff {α : Type u_1} {S : Set (Preorder α)} {a b : α} : a ≤ b ↔ ∀ p ∈ S, a ≤ b