Record is_PartialOrder
(car : Type)
(eq : car -> car -> Prop)
(le : car -> car -> Prop)
(monotone : (car -> car) -> Prop)
(antitone : (car -> car) -> Prop) : Prop :=
{ po_equiv_le_def : forall x y, eq x y <-> (le x y /\ le y x)
; po_le_refl : forall x, le x x
; po_le_trans : forall x y z, le x y -> le y z -> le x z
; po_monotone_def : forall f, monotone f <-> (forall x y, le x y -> le (f x) (f y))
; po_antitone_def : forall f, antitone f <-> (forall x y, le x y -> le (f y) (f x))
}.
Record PartialOrder : Type :=
{ po_car :> Setoid
; le : po_car -> po_car -> Prop
; monotone : (po_car -> po_car) -> Prop
; antitone : (po_car -> po_car) -> Prop
; po_proof : is_PartialOrder (@st_eq po_car) le monotone antitone
}.
Notation "x == y" := (st_eq x y) (at level 70, no associativity) : po_scope.
Notation "x <= y" := (le _ x y) : po_scope.
Lemma po_st : forall X eq le mnt ant, @is_PartialOrder X eq le mnt ant -> Setoid_Theory X eq.
Section PartialOrder.
Variable X : PartialOrder.
Definition makePartialOrder car eq le monotone antitone p1 p2 p3 p4 p5 :=
let p := (@Build_is_PartialOrder car eq le monotone antitone p1 p2 p3 p4 p5) in
@Build_PartialOrder (Build_Setoid (po_st p)) le monotone antitone p.
The axioms and basic properties of a partial order
Lemma equiv_le_def : forall x y:X, x == y <-> (x <= y /\ y <= x).
Lemma le_refl : forall x:X, x <= x.
Lemma le_trans : forall x y z : X, x <= y -> y <= z -> x <= z.
Lemma monotone_def : forall f, monotone X f <-> (forall x y, x <= y -> (f x) <= (f y)).
Lemma antitone_def : forall f, antitone X f <-> (forall x y, x <= y -> (f y) <= (f x)).
Lemma le_equiv_refl : forall x y:X, x == y -> x <= y.
Lemma le_antisym : forall x y:X, x <= y -> y <= x -> x == y.
Lemma le_refl : forall x:X, x <= x.
Lemma le_trans : forall x y z : X, x <= y -> y <= z -> x <= z.
Lemma monotone_def : forall f, monotone X f <-> (forall x y, x <= y -> (f x) <= (f y)).
Lemma antitone_def : forall f, antitone X f <-> (forall x y, x <= y -> (f y) <= (f x)).
Lemma le_equiv_refl : forall x y:X, x == y -> x <= y.
Lemma le_antisym : forall x y:X, x <= y -> y <= x -> x == y.
Section MonotoneAntitone.
Variable A : Type.
Variable le : A -> A -> Prop.
Definition monotone (f: A -> A) := forall x y, le x y -> le (f x) (f y).
Lemma monotone_def : forall f, monotone f <-> (forall x y, le x y -> le (f x) (f y)).
Definition antitone (f: A -> A) := forall x y, le x y -> le (f y) (f x).
Lemma antitone_def : forall f, antitone f <-> (forall x y, le x y -> le (f y) (f x)).
End MonotoneAntitone.
End Default.
Variable A : Type.
Variable le : A -> A -> Prop.
Definition monotone (f: A -> A) := forall x y, le x y -> le (f x) (f y).
Lemma monotone_def : forall f, monotone f <-> (forall x y, le x y -> le (f x) (f y)).
Definition antitone (f: A -> A) := forall x y, le x y -> le (f y) (f x).
Lemma antitone_def : forall f, antitone f <-> (forall x y, le x y -> le (f y) (f x)).
End MonotoneAntitone.
End Default.