Library CT.Order.PartiallyOrderedSet
Record
PartiallyOrderedSet
{
element
:
Type
} :=
{
le
:
element
→
element
→
Prop
;
reflexive
:
∀
a
,
le
a
a
;
transitive
:
∀
a
b
c
,
le
a
b
∧
le
b
c
→
le
a
c
;
antisymmetric
:
∀
a
b
,
le
a
b
∧
le
b
a
→
a
=
b
}.