processing...
home
items
order theory
create a passkey
account
chatqed
Coq
Agda
Lean
references
items
authors
citations
tools
unicode
settings
help
Order Theory
Preorder
a ≤ a (reflexive),
(
a ≤ b
)
×
(
b ≤ c
)
→
(
a ≤ c
)
(transitive).
Meet
x ∧ y ≤ x, x ∧ y ≤ y,
(
a ≤ x
)
×
(
a ≤ y
)
→ a ≤ x ∧ y.
Join
x ≤ x ∨ y, y ≤ x ∨ y,
(
x ≤ a
)
×
(
y ≤ a
)
→ x ∨ y ≤ a.
Partial Order
(
x ≤ y
)
×
(
y ≤ x
)
→ x = y (antisymmetric).
Order
Lattice
Comparison with Cateogory Theory
References