Theorems · Definition · order theory

Antisymmetrization

(α : Type u_1) → (r : α → α → Prop) → [IsPreorder α r] → Type u_1

The partial order derived from a preorder by making pairwise comparable elements equal. This is the quotient by fun a b => a ≤ b ∧ b ≤ a.

Defined in

Mathlib.Order.Antisymmetrization

Cited by

25 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

IsPreorder