The complete lattice of preorders on a type

[UPSTREAM] candidate. This mirrors CompleteLattice (Setoid α) (Mathlib.Data.Setoid.Basic) for preorders: the preorders on a fixed type α, ordered by relation inclusion (p ≤ q iff every p-related pair is q-related), form a complete lattice.

• ⊤ is the total preorder (everything related) — the coarsest order.
• ⊥ is equality (· = ·) — the finest preorder.
• p ⊓ q is the intersection of the two relations.
• ⨅ i, p i (sInf) is the intersection of a family.

This is the order-theoretic substrate of refinement in default-reasoning and conditional semantics: refining a normality/plausibility ordering by a criterion is meet with that criterion's induced preorder, so the refinement calculus (commutativity, idempotence, the total order as unit) is just the meet-semilattice laws. Preorder.lift (mathlib) supplies the criterion orders; this file supplies the algebra that combines them.

Mathlib has CompleteLattice (Setoid α) but no order structure on Preorder α; this fills that gap.

@[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 α

Smart constructor: a Preorder from a reflexive-transitive relation, with the strict order taken canonically (a < b ↔ a ≤ b ∧ ¬ b ≤ a). Avoids the default-lt synthesis failing on relations built pointwise.

Equations

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

@[implicit_reducible]

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

Preorders are ordered by relation inclusion: p ≤ q iff every pair related by p is related by q (i.e. p is finer).

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

@[implicit_reducible]

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

Equations

• Preorder.instPartialOrder_linglib = { le := fun (x1 x2 : Preorder α) => x1 ≤ x2, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[implicit_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) ⋯ ⋯ }

@[implicit_reducible]

instance Preorder.instCompleteLattice_linglib {α : 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

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

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