- Fundamental set theory
- Theory of Sets EII-3 Correspondences
- EII-3-1 Graphs et correspondences
- Additional lemmas
- EII-3-2 Inverse of a correspondence
- EII-3-3 Composition of two correspondences
- EII-3-4 Functions
- EII-3-5 Restrictions and extensions of functions
- EII-3-6 Definition of a function by means of a term
- EII-3-7 Composition of two functions. Inverse function
- EII-3-8 Retractions and sections
- EII-3-9 Functions of two arguments
- Theory of Sets: EII-4 Union and intersection of a family of sets
- EII-4-1 Definition of the union and intersection of a family of sets
- EII-4-2 Properties of union and intersection
- EII-4-3 Images of a union and an intersection
- EII-4-4 complement of unions and intersections
- EII-4-5 union and intersection of two sets
- EII-4-6 Coverings
- EII-4-7 Partitions
- EII-4-8 Sum of a family of sets
- EII-5 Product of a family of sets
- Theory of Sets EII-6 Equivalence relations
- EII-6-1 Definition of an equivalence relation
- EII-6-2 Equivalence classes; quotient set
- EII-6-3 Relations compatible with an equivalence relation
- EII-6-4 saturated subsets
- EII-6-5 Mappings compatible with equivalence relations
- EII-6-6 Inverse image of an equivalence relation; induced equivalence relation
- EII-6-7 Quotients of equivalence relations
- EII-6-8 Product of two equivalence relations
Library set5
Theory of Sets EIII-1 Order relations. Ordered sets
Copyright INRIA (2009-2010) Apics Team (Jose Grimm).
Require Export set2.
Require Export set3.
Require Export set4.
Set Implicit Arguments.
Import Correspondence.
Import Bfunction.
Module Border.
We define
antisymmetric_r for a relation and is_antisymmetric for a
graph and refkexive_rr for a relation
Definition antisymmetric_r (r:EEP) :=
forall x y, r x y -> r y x -> x = y.
Definition is_antisymmetric (r:Set) :=
is_graph r & forall x y, related r x y -> related r y x -> x = y.
Definition reflexive_rr (r:EEP) :=
forall x y, r x y -> (r x x & r y y).
We define an order and a preorder relation
Definition order_r (r:EEP) :=
transitive_r r & antisymmetric_r r & reflexive_rr r.
Definition preorder_r (r:EEP) :=
transitive_r r & reflexive_rr r.
Lemma equality_is_order: order_r(fun x y => x = y).
Proof. red. ee;red; au. ir. ue.
Qed.
Lemma sub_is_order: order_r sub.
Proof. red. ee. red. ir. ap (sub_trans H H0).
red. ir. app extensionality. red. ir. split; app sub_refl.
Qed.
Definition opposite_relation (r:EEP) := fun x y => r y x.
Lemma opposite_is_preorder_r: forall r,
preorder_r r -> preorder_r (opposite_relation r).
Proof. uf preorder_r. uf opposite_relation. ir. nin H. split. red. ir.
app (H _ _ _ H2 H1). red. ir. set (H0 _ _ H1). int.
Qed.
Lemma opposite_is_order_r: forall r,
order_r r -> order_r (opposite_relation r).
Proof. ir. red in H. ee. assert (preorder_r r). red. int.
nin (opposite_is_preorder_r H2). red. eee.
uf opposite_relation. red. ir. app H0.
Qed.
An order is either a relation or a graph
Definition order_re (r:EEP) x :=
order_r r & reflexive_r r x.
Definition order (r:Set) :=
is_reflexive r & is_transitive r & is_antisymmetric r.
Lemma order_is_graph: forall r, order r -> is_graph r.
Proof. ir. nin H; nin H; am. Qed.
Hint Resolve order_is_graph : fprops.
Definition opposite_order := inverse_graph.
Definition preorder (r: Set) :=
is_reflexive r & is_transitive r.
Lemma preorder_graph : forall r, preorder r -> is_graph r.
Proof. ir. nin H. nin H. am. Qed.
Lemma order_preorder : forall r, order r -> preorder r.
Proof. ir. red in H. red. eee. Qed.
Lemma order_has_graph0: forall r x,
order_re r x -> is_graph_of (graph_on r x) r.
Proof. red. uf related. uf graph_on. ir. ap iff_eq; ir; Ztac.
destruct H as [ [_ [_ H3]] H1]. nin (H3 _ _ H0). wri H1 H. wri H1 H2.
fprops. aw.
awii H2.
Qed.
Lemma graph_on_rw3: forall r x u v,
order_re r x ->
related (graph_on r x) u v = r u v.
Proof. ir. sy. app (order_has_graph0 H).
Qed.
Lemma order_has_graph: forall r x,
order_re r x -> exists g, is_graph_of g r.
Proof. ir. exists (graph_on r x). app order_has_graph0.
Qed.
Lemma order_if_has_graph: forall r g,
is_graph g -> is_graph_of g r ->
order_r r -> order_re r (domain g).
Proof. red. uf is_graph_of. uf related. ir. split. am. red. ir.
aw. ap iff_eq. ir. nin H2. wri H0 H2. red in H1. ee.
red in H4; ee. nin (H4 _ _ H2). am. ir. exists y. wrr H0.
Qed.
Lemma order_if_has_graph2: forall r g,
is_graph g -> is_graph_of g r ->
order_r r -> order g.
Proof. ir. red in H0. red in H1. red. ee. red. ee. am. ir.
rwi inc_substrate_rw H4. ufi related H0. nin H4. nin H4. wri H0 H4.
nin (H3 _ _ H4). red. wrr H0. nin H4. wri H0 H4. nin (H3 _ _ H4).
red. wrr H0. am. red. ee. am. intros x y z. do 3 wr H0. app H1.
red. ee. am. intros x y. wr H0. wr H0. app H2.
Qed.
Lemma order_has_graph2: forall r x,
order_re r x -> exists g,
g = graph_on r x &
order g & (forall u v, r u v = related g u v).
Proof. ir. exists (graph_on r x). ee. tv.
assert (is_graph (graph_on r x)). app graph_on_graph.
assert (is_graph_of (graph_on r x) r). app order_has_graph0. red in H. ee.
app (order_if_has_graph2 H0 H1 H). ir.
pose (order_has_graph0 H). ufi is_graph_of i. app i.
Qed.
Lemma preorder_from_rel: forall r x,
preorder_r r -> preorder (graph_on r x).
Proof. ir. assert (is_graph (graph_on r x)). uf graph_on. red. ir.
Ztac. awi H1. nin H1. am. nin H. split. split. am.
ir. ufi graph_on H2. uf graph_on. rwi inc_substrate_rw H2. nin H2. nin H2.
Ztac. clear H2. red. Ztac. awi H3. ee. fprops. awi H4. nin (H1 _ _ H4). aw.
nin H2. Ztac. clear H2. red. Ztac. awi H3. ee. fprops. awi H4.
nin (H1 _ _ H4). aw. am.
split. am. uf related. uf graph_on. ir. nin (Z_all H2). nin (Z_all H3).
awi H4. awi H5. awi H6. awi H7. ee. app Z_inc. fprops. aw.
ap (H _ _ _ H5 H7).
Qed.
Lemma order_from_rel: forall r x,
order_r r -> order (graph_on r x).
Proof. ir. assert (preorder (graph_on r x)). app preorder_from_rel.
red in H. red. intuition. red in H0. ee. red. eee. red. ee. nin H0. am.
uf related. uf graph_on. ir. Ztac. clear H3. Ztac. awi H5; awi H6.
destruct H as [_ [H8 _]]. app H8.
Qed.
Lemma order_reflexivity_pr: forall r x u v,
order_re r x -> r u v -> (inc u x & inc v x).
Proof. ir. destruct H as [ [_ [_ H1]] H2]. red in H1; red in H2.
rw H2. rw H2. app H1.
Qed.
Lemma order_symmetricity_pr: forall r x u v,
order_re r x -> (r u v & r v u) = (inc u x & inc v x & u = v).
Proof. ir. app iff_eq. ir. ee.
cp (order_reflexivity_pr _ _ H H0). ee. am.
cp (order_reflexivity_pr _ _ H H1). ee. am.
red in H; ee. red in H; ee. app H3. ir.
destruct H as [ _ H1]. red in H1. ee.
rw H2. wr H1. am. rw H2. wr H1. am.
Qed.
Lemma order_reflexivity: forall r a,
order r -> inc a (substrate r) = related r a a.
Proof. ir. red in H. ee. red in H. ee. app iff_eq. ee. app H2.
ir. substr_tac.
Qed.
Lemma order_antisymmetry: forall r a b,
order r -> related r a b -> related r b a -> a = b.
Proof. ir. red in H. ee. red in H3. ee. app H4.
Qed.
Lemma order_transitivity: forall r a b c,
order r -> related r a b -> related r b c -> related r a c.
Proof. ir. red in H. ee. red in H2. ee. app (H4 a b c).
Qed.
Lemma inter_rel_order : forall z,
nonempty z -> (forall r, inc r z -> order r) ->
order (intersection z).
Proof. ir. red. assert (is_reflexive (intersection z)).
app inter_rel_reflexive. ir. destruct (H0 _ H1) as [H3 [H4 H5]]. am.
eee. app inter_rel_transitive. ir. destruct (H0 _ H2) as [H3 [H4 H5]]. am.
red. split. nin H1; am. uf related. ir. nin H.
cp (intersection_forall H2 H). cp (intersection_forall H3 H).
destruct (H0 _ H) as [ _ [ _ [_ H6] ]]. app H6.
Qed.
Definition gle (r x y:Set) := related r x y.
Definition gge (r x y:Set) := gle r y x.
Definition glt (r x y:Set) := gle r x y & x <> y.
Definition ggt (r x y:Set) := gge r x y & x <> y.
Lemma lt_leq_trans : forall r x y z,
order r -> glt r x y -> gle r y z -> glt r x z.
Proof. ir. nin H0. split. apply order_transitivity with y. am. am. am.
red; ir; ap H2. wri H3 H1. app (order_antisymmetry H H0 H1).
Qed.
Lemma leq_lt_trans : forall r x y z,
order r -> gle r x y -> glt r y z -> glt r x z.
Proof. ir. nin H1. split. apply order_transitivity with y. am. am. am.
red; ir; ap H2. rwi H3 H0. app (order_antisymmetry H H1 H0).
Qed.
Lemma lt_lt_trans: forall r a b c, order r ->
glt r a b -> glt r b c -> glt r a c.
Proof. ir. red in H0. ee. app (leq_lt_trans H H0 H1).
Qed.
Lemma not_le_gt: forall r x y, order r -> gle r x y -> glt r y x -> False.
Proof. ir. nin H1. elim H2. app (order_antisymmetry H H1 H0).
Qed.
Ltac order_tac:=
match goal with
| H1: gle ?r ?x _ |- inc ?x (substrate ?r)
=> exact (inc_arg1_substrate H1)
| H1: glt ?r ?x _ |- inc ?x (substrate ?r)
=> nin H1; order_tac
| H1:gle ?r _ ?x |- inc ?x (substrate ?r)
=> exact (inc_arg2_substrate H1)
| H1:glt ?r _ ?x |- inc ?x (substrate ?r)
=> nin H1; order_tac
| H: order ?r, H1: inc ?u (substrate ?r) |- related ?r ?u ?u
=> wrr order_reflexivity
| H: order ?r |- inc (J ?u ?u) ?r
=> change (related r u u); wrr order_reflexivity
| H: order ?r |- gle ?r ?u ?u
=> wrr order_reflexivity
| H1: gle ?r ?x ?y, H2: gle ?r ?y ?x, H:order ?r |-
?x = ?y => exact (order_antisymmetry H H1 H2)
| H:order ?r, H1:related ?r ?x ?y, H2: related ?r ?y ?x |- ?x = ?y
=> app (order_antisymmetry H H1 H2)
| H:order ?r, H1: inc (J ?x ?y) ?r , H2: inc (J ?y ?x) ?r |- ?x = ?y
=> app (order_antisymmetry H H1 H2)
| H:order ?r, H1:related ?r ?u ?v, H2: related ?r ?v ?w
|- related ?r ?u ?w
=> app (order_transitivity H H1 H2)
| H:order ?r, H1:gle ?r ?u ?v, H2: gle ?r ?v ?w
|- gle ?r ?u ?w
=> app (order_transitivity H H1 H2)
| H: order ?r, H1: inc (J ?u ?v) ?r, H2: inc (J ?v ?w) ?r |-
inc (J ?u ?w) ?r
=> change (related r u w); app (order_transitivity H H1 H2)
| H1: gle ?r ?x ?y, H2: glt ?r ?y ?x, H: order ?r |- _
=> elim (not_le_gt H H1 H2)
| H1:glt ?r ?x ?y, H2: glt ?r ?y ?x, H:order ?r |- _
=> destruct H1 as [H1 _] ; elim (not_le_gt H H1 H2)
| H1:order ?r, H2:glt ?r ?x ?y, H3: gle ?r ?y ?z |- glt ?r ?x ?z
=> exact (lt_leq_trans H1 H2 H3)
| H1:order ?r, H2:gle ?r ?x ?y, H3: glt ?r ?y ?z |- glt ?r ?x ?z
=> exact (leq_lt_trans H1 H2 H3)
| H1:order ?r, H2:glt ?r ?x ?y, H3: glt ?r ?y ?z |- glt ?r ?x ?z
=> exact (lt_lt_trans H1 H2 H3)
| H1:order ?r, H2:gle ?r ?x ?y |- glt ?r ?x ?y
=> split; tv; red; ir
| H:glt ?r ?x ?y |- gle ?r ?x ?y
=> nin H ; am
| H1:(inc _ (Zo _ _)), H2 :(inc _ (Zo _ _)) |- _
=> nin (Z_all H1); nin (Z_all H2); clear H1; clear H2; ee
end.
Lemma order_is_order: forall r,
order r -> order_r (related r).
Proof. ir. red. red in H. ee. red. red in H0. ee. am. red. nin H1. am.
red. red in H. ee. ir. ee.
ap (H2 _ (inc_arg1_substrate H3)). ap (H2 _ (inc_arg2_substrate H3)).
Qed.
Lemma substrate_opposite_order: forall r,
order r -> substrate(opposite_order r) = substrate r.
Proof. ir. assert (Ha: is_graph r). fprops.
assert(is_graph (opposite_order r)). fprops.
set_extens; rwii inc_substrate_rw H1; rww inc_substrate_rw.
nin H1; nin H1; awi H1; [ right | left ]; ex_tac.
nin H1; nin H1; [ right | left ] ; exists x0; aw.
Qed.
Hint Rewrite substrate_opposite_order : aw.
Lemma substrate_domain_order: forall f,
order f -> substrate f = domain f.
Proof. ir. set_extens. assert (related f x x). order_tac. uf domain. aw.
red in H1. ex_tac. aw. uf substrate. inter2tac.
Qed.
Lemma opposite_is_order: forall r,
order r -> order (opposite_order r).
Proof. ir. set (g:= opposite_order r).
assert (is_graph g). uf g. fprops.
assert (is_graph_of g (opposite_relation (related r))). red.
uf opposite_relation. uf g. uf related. ir. aw.
assert(order_r (opposite_relation (related r))). app opposite_is_order_r.
app order_is_order. app (order_if_has_graph2 H0 H1 H2).
Qed.
Hint Resolve opposite_is_order: fprops.
Lemma diagonal_order : forall x,
order(identity_g x).
Proof. ir. cp (diagonal_equivalence x). red in H. ee.
red. eee. red. split. nin H. am. ir. red in H2. awi H2. eee.
Qed.
Order induced by a relation on a set
Lemma order_from_rel1: forall r x,
transitive_r r ->
(forall u v, inc u x -> inc v x -> r u v -> r v u -> u = v) ->
(forall u, inc u x -> r u u) ->
order (graph_on r x).
Proof. ir.
assert (graph_on r x = graph_on (fun a b => inc a x & inc b x & r a b) x).
uf graph_on. set_extens; Ztac. awi H4. awi H3. eee. ee. am. rw H2.
app order_from_rel.
red. ee; red;ir. ee. am. am. apw H y. ee. app H0. eee.
Qed.
Lemma substrate_graph_on: forall (r:EEP) x,
(forall a, inc a x -> r a a) ->
substrate (graph_on r x) = x.
Proof. ir. app extensionality. app graph_on_substrate. red. ir.
cp (H _ H0). assert (related (graph_on r x) x0 x0).
uf graph_on. red. Ztac. fprops. aw. substr_tac.
Qed.
Inclusion order on the powerset of a set, or a part of it
Definition inclusion_suborder (b:Set) :=
graph_on sub b.
Definition inclusion_order (a:Set) := inclusion_suborder (powerset a).
Lemma subinclusion_is_order: forall a,
order (inclusion_suborder a).
Proof. ir. uf inclusion_suborder. app order_from_rel. app sub_is_order.
Qed.
Lemma inclusion_is_order: forall a,
order (inclusion_order a).
Proof. ir. uf inclusion_order. app subinclusion_is_order.
Qed.
Lemma substrate_subinclusion_order:forall a,
substrate (inclusion_suborder a) = a.
Proof. ir. uf inclusion_suborder. app substrate_graph_on.
ir. fprops.
Qed.
Lemma substrate_inclusion_order: forall a,
substrate (inclusion_order a) = powerset a.
Proof. ir. uf inclusion_order. app substrate_subinclusion_order.
Qed.
Lemma subinclusion_order_rw: forall a u v ,
related (inclusion_suborder a) u v = (inc u a & inc v a & sub u v).
Proof. ir. uf inclusion_suborder. rww graph_on_rw1.
Qed.
Lemma inclusion_order_rw: forall a u v ,
related (inclusion_order a) u v = (sub u a & sub v a & sub u v).
Proof. ir. uf inclusion_order. rw subinclusion_order_rw. aw.
Qed.
Hint Rewrite substrate_inclusion_order : aw.
Hint Rewrite substrate_subinclusion_order : aw.
Hint Resolve inclusion_is_order subinclusion_is_order: fprops.
Hint Rewrite subinclusion_order_rw inclusion_order_rw: aw.
Extension order on partial functions from
x to y
Definition extension_order x y :=
graph_on extends (set_of_sub_functions x y).
Hint Rewrite set_of_sub_functions_rw : bw.
Lemma extends_in_prop: forall x y,
order_r extends &
(forall u, inc u (set_of_sub_functions x y) -> extends u u).
Proof. ir. uf extends. split. red. eee; red; ir. eee. apw sub_trans (graph y0).
apw sub_trans (target y0). eee.
assert (graph x0 = graph y0). app extensionality.
assert (target x0 = target y0). app extensionality.
app function_exten1. eee. ir. bwi H. eee.
Qed.
Lemma extension_is_order: forall x y,
order (extension_order x y).
Proof. ir. uf extension_order. nin (extends_in_prop x y).
app order_from_rel.
Qed.
Lemma substrate_extension_order: forall x y,
substrate (extension_order x y) = (set_of_sub_functions x y).
Proof. ir. uf extension_order. nin (extends_in_prop x y).
app substrate_graph_on.
Qed.
Lemma extension_order_rw : forall E F f g,
gle (extension_order E F) g f =
(inc g (set_of_sub_functions E F) & inc f (set_of_sub_functions E F)
& extends g f).
Proof. ir. uf gle. uf related. uf extension_order. rww graph_on_rw0.
Qed.
Lemma extension_order_pr1 : forall E F f g,
gle (extension_order E F) g f =
(inc g (set_of_sub_functions E F) & inc f (set_of_sub_functions E F)
& sub (graph f) (graph g)).
Proof. ir. rw extension_order_rw. uf extends. app iff_eq. ir. eee.
ir. nin H. nin H0. cp H; cp H0. bwi H; bwi H0. eee. rw H5. fprops.
Qed.
Lemma extension_order_pr2 : forall E F f g,
gle (opposite_order (extension_order E F)) g f =
(inc g (set_of_sub_functions E F) & inc f (set_of_sub_functions E F)
& sub (graph g) (graph f)).
Proof. ir. uf gle. uf related. aw.
replace (inc (J f g) (extension_order E F)) with
(gle (extension_order E F) f g). rw extension_order_pr1.
app iff_eq; ir; eee. tv.
Qed.
Hint Rewrite extension_order_rw: aw.
Hint Resolve extension_is_order: fprops.
Lemma extension_order_pr : forall E F f g x,
gle (opposite_order (extension_order E F)) f g ->
inc x (source f) -> W x f = W x g.
Proof. ir. ufi opposite_order H. rwi inverse_graph_pr2 H. awi H. ee.
app (W_extends H2 H0).
Qed.
Hint Rewrite substrate_extension_order: aw.
Example 4. Order between partitions on a set
Definition set_of_partition_set x :=
Zo(powerset(powerset x)) (fun z => partition z x).
Definition partition_fun_of_set y x:=
canonical_injection y (powerset x).
Lemma partition_set_in_double_powerset: forall y x,
partition y x -> inc y (powerset (powerset x)).
Proof. ir. app powerset_inc. red. ir. app powerset_inc. red. ir.
pose (union_inc H1 H0). red in H. ee. ue.
Qed.
Lemma set_of_partition_rw: forall x y,
inc y (set_of_partition_set x) = partition y x.
Proof. ir. uf set_of_partition_set. app iff_eq. ir. Ztac. am.
ir. Ztac. app partition_set_in_double_powerset.
Qed.
Lemma pfs_function: forall y x,
partition y x -> is_function (partition_fun_of_set y x).
Proof. ir. uf partition_fun_of_set. app ci_function. app powerset_sub.
app partition_set_in_double_powerset.
Qed.
Lemma pfs_W: forall y x a,
partition y x -> inc a y ->
W a (partition_fun_of_set y x) = a.
Proof. ir. uf partition_fun_of_set. app ci_W.
app powerset_sub. app partition_set_in_double_powerset.
Qed.
Lemma pfs_partition: forall y x,
partition y x -> partition_fam (graph (partition_fun_of_set y x)) x.
Proof. ir. cp (pfs_function H).
assert (Ha:forall i, inc i y -> V i (graph (partition_fun_of_set y x)) = i).
ir. change(W i (partition_fun_of_set y x) = i). app pfs_W.
assert (domain (graph (partition_fun_of_set y x)) = y).
red in H0. ee. wrr H2. uf partition_fun_of_set.
uf canonical_injection. aw.
red. ee. fprops. red. rw H1. ir. rw (Ha _ H2). rw (Ha _ H3).
red in H; ee. app H5.
set_extens. nin (unionb_exists H2). ee. rwi H1 H3. rwi (Ha _ H3) H4.
red in H. ee. wr H. union_tac.
cp H. red in H. ee. wri H H2. nin (union_exists H2). ee.
apply unionb_inc with x1. rww H1. rw (Ha _ H7). am.
Qed.
All these lemmas say that, essentially, a partition is a partition set
Definition coarser x := graph_on coarser_c (set_of_partition_set x).
Lemma coarser_related: forall x y y',
related (coarser x) y y' =
(partition y x & partition y' x & coarser_c y y').
Proof. ir. uf coarser. uf graph_on. uf related. app iff_eq. ir.
nin (Z_all H). awi H0. rwi set_of_partition_rw H0.
rwi set_of_partition_rw H0. awi H0. awi H1. intuition.
ir. ee. Ztac. aw. eee; rww set_of_partition_rw. aw.
Qed.
Lemma coarser_related_bis: forall x y y',
related (coarser x) y y' =
(partition y x & partition y' x &
forall a, inc a y' -> exists b, inc b y & sub a b).
Proof. ir. rww coarser_related.
Qed.
Lemma coarser_substrate : forall x,
substrate (coarser x) = set_of_partition_set x.
Proof. ir. uf coarser. app extensionality. app graph_on_substrate.
red. ir. apply inc_arg1_substrate with x0. uf related. uf graph_on.
Ztac. aw. eee. aw. app coarser_reflexive.
Qed.
Lemma coarser_order : forall x, order (coarser x).
Proof. ir. assert (is_graph (coarser x)).
uf coarser. app graph_on_graph.
red. ee;split;tv. ir.
rw coarser_related. rwi coarser_substrate H0. rwi set_of_partition_rw H0.
eee. app coarser_reflexive. ir. rw coarser_related.
rwi coarser_related H0. rwi coarser_related H1. eee.
app (coarser_transitive H5 H3).
ir. rwi coarser_related H0. rwi coarser_related H1. ee.
app (coarser_antisymmetric H0 H4 H5 H3).
Qed.
Lemma smallest_partition_is_smallest: forall x y,
nonempty x ->
partition y x -> related (coarser x) (smallest_partition x) y.
Proof. ir. rw coarser_related. ee. app partition_smallest. am. red. ir.
uf smallest_partition. ex_tac.
cp (partition_set_in_double_powerset H0). awi H2.
app powerset_sub. app H2.
Qed.
Lemma largest_partition_is_largest: forall x y,
partition y x -> related (coarser x) y (largest_partition x).
Proof. ir. rw coarser_related. ee. am. app partition_largest. red. ir.
ufi largest_partition H0. rwi L_range_rw H0. nin H0. ee. red in H. ee.
wri H H0. nin (union_exists H0). ee. ex_tac. wr H1. red. ir. db_tac.
Qed.
Definition partition_relation_set y x :=
partition_relation (partition_fun_of_set y x) x.
Lemma prs_is_equivalence: forall y x,
partition y x -> is_equivalence (partition_relation_set y x).
Proof. ir. uf partition_relation_set. app partition_is_equivalence.
app pfs_function. app pfs_partition.
Qed.
Definition partition_relation_set_aux y x :=
Zo (powerset (coarse x)) (fun z => exists a, inc a y & z = coarse a).
Lemma partition_relation_set_pr1: forall y x a,
partition y x ->
inc a y -> inc (coarse a) (partition_relation_set_aux y x).
Proof. ir. cp (partition_set_in_double_powerset H). rwi powerset_inc_rw H1.
assert (inc a (powerset x)). app H1. rwi powerset_inc_rw H2.
uf partition_relation_set_aux. uf coarse.
Ztac. app powerset_inc. red. ir. awi H3. ee. aw. eee. ex_tac.
Qed.
Lemma partition_relation_set_pr: forall y x,
partition y x ->
partition_relation_set y x =
union (partition_relation_set_aux y x).
Proof. ir. assert (partition_fam (graph(partition_fun_of_set y x)) x).
app pfs_partition. cp (partition_set_in_double_powerset H).
assert (Ha:source (partition_fun_of_set y x) = y).
uf partition_fun_of_set. uf canonical_injection. aw.
rwi powerset_inc_rw H1. uf partition_relation_set. rw graph_exten.
ir. rw partition_relation_pr. uf in_same_coset. rw Ha. app iff_eq. ir.
nin H2. ee. rwi pfs_W H3. rwi pfs_W H4. uf related.
apply union_inc with (coarse x0). uf coarse. fprops.
app partition_relation_set_pr1. am. am. am. am.
ir. red in H2. nin (union_exists H2). ee. ufi partition_relation_set_aux H4.
Ztac. nin H6. ee. ex_tac. rwi H7 H3. ufi coarse H3. awi H3. ee;rww pfs_W.
app pfs_function. am. cp (prs_is_equivalence H). fprops.
red. ir. nin (union_exists H2). ee. ufi partition_relation_set_aux H4.
Ztac. rwi powerset_inc_rw H5.
assert (inc y0 (coarse x)). app H5. ufi coarse H7. awi H7. ee. am.
Qed.
Lemma sub_partition_relation_set_coarse: forall y x,
partition y x -> sub (partition_relation_set y x) (coarse x).
Proof. ir. rw partition_relation_set_pr. red. ir.
nin (union_exists H0). ee. ufi partition_relation_set_aux H2.
Ztac. app (powerset_sub H3). am.
Qed.
Lemma nondisjoint :forall a b c, inc a b -> inc a c -> disjoint b c -> False.
Proof. ir. red in H1. empty_tac1 a. inter2tac.
Qed.
Lemma partition_relation_set_order: forall x y y',
partition y x -> partition y' x ->
sub (partition_relation_set y' x)(partition_relation_set y x) =
related (coarser x) y y'.
Proof. ir. rww partition_relation_set_pr. rww partition_relation_set_pr.
rw coarser_related. uf coarser_c. app iff_eq. ir. eee. ir.
cp (partition_relation_set_pr1 H0 H2).
assert (nonempty a). red in H0. eee. nin H4.
assert (inc (J y0 y0) (union (partition_relation_set_aux y x))). app H1.
apply union_inc with (coarse a). uf coarse. fprops. am.
nin (union_exists H5). ee. ufi partition_relation_set_aux H7. Ztac.
nin H9. red in H; ee.
assert (inc y0 x1). rwi H10 H6. ufi coarse H6. awi H6; ee;am. ex_tac.
red. ir.
assert (inc (J y0 x2) (union (partition_relation_set_aux y x))). app H1.
apply union_inc with (coarse a). uf coarse. fprops. am.
nin (union_exists H15). ee. ufi partition_relation_set_aux H17. Ztac.
nin H19. ee. rwi H20 H16. ufi coarse H16. awi H16. ee.
nin (H12 _ _ H19 H9). wrr H23. elim (nondisjoint H21 H13 H23).
ir. ee. red. ir. nin (union_exists H4). ee.
ufi partition_relation_set_aux H6. Ztac. clear H6. nin H8. ee.
cp (H3 _ H6). nin H9. ee. apply union_inc with (coarse x3).
assert (sub (coarse x2) (coarse x3)). uf coarse. app product_monotone.
app H11. wrr H8. app partition_relation_set_pr1.
Qed.
Lemma partition_relation_set_order_antisymmetric: forall x y y',
partition y x -> partition y' x ->
(partition_relation_set y' x = partition_relation_set y x) ->
y = y'.
Proof. assert (forall x y y',
partition y x -> partition y' x ->
(partition_relation_set y' x = partition_relation_set y x) ->
sub y y').
ir. rwi (partition_relation_set_pr H) H1.
rwi (partition_relation_set_pr H0) H1. red. ir.
cp (partition_relation_set_pr1 H H2).
assert (nonempty x0). red in H. eee. nin H4.
assert (inc (J y0 y0) (coarse x0)). uf coarse. fprops.
assert (inc (J y0 y0) (union (partition_relation_set_aux y' x))).
rw H1. union_tac.
nin (union_exists H6). ee. ufi partition_relation_set_aux H8. Ztac.
nin H10. ee. clear H8. assert (x0 = x2). set_extens.
assert (inc (J x3 x3) (coarse x0)). uf coarse. fprops.
assert (inc (J x3 x3) (union (partition_relation_set_aux y' x))).
rw H1. union_tac.
nin (union_exists H13). ee. ufi partition_relation_set_aux H15. Ztac.
nin H17. ee. clear H15.
assert (inc (J y0 x3) (coarse x0)). uf coarse. fprops.
assert (inc (J y0 x3) (union (partition_relation_set_aux y' x))).
rw H1. union_tac.
cp (union_exists H19). nin H20. ee. ufi partition_relation_set_aux H21.
Ztac. nin H23. ee. clear H21.
rwi H24 H20. ufi coarse H20. awi H20. awi H20. ee.
rwi H18 H14. ufi coarse H14. awi H14. awi H14. ee.
red in H0. ee. nin (H29 _ _ H17 H23). nin (H29 _ _ H17 H10).
wr H31. am. rwi H11 H7. ufi coarse H7. awi H7. awi H7. ee.
rwi H30 H31. elim (nondisjoint H21 H32 H31). elim (nondisjoint H26 H25 H30).
assert (inc (J y0 x3) x1). rw H11. uf coarse. app product_pair_inc.
rwi H11 H7. ufi coarse H7. awi H7; eee.
assert (inc (J y0 x3) (union (partition_relation_set_aux y' x))).
apply union_inc with x1. am. uf partition_relation_set_aux. Ztac. exists x2.
au. rwi H1 H13. nin (union_exists H13). ee.
ufi partition_relation_set_aux H15. Ztac. nin H17. ee. rwi H18 H14.
ufi coarse H14. awi H14. ee.
ufi coarse H5. awi H5. ee.
red in H. ee. nin (H24 _ _ H17 H2). wrr H25. elim (nondisjoint H19 H22 H25).
rww H8.
ir. app extensionality.
app (H _ _ _ H0 H1 H2). symmetry in H2. app (H _ _ _ H1 H0 H2).
Qed.
Lemma preorder_prop1: forall g,
is_graph g ->
sub (identity_g (substrate g)) g -> sub (compose_graph g g) g ->
compose_graph g g = g.
Proof. ir. app extensionality. red. ir. aw. ee. app H.
wri (pair_recov (H _ H2)) H2. ex_tac.
app H0. aw. ee. substr_tac. tv.
Qed.
Theorem order_pr: forall r,
order r =
(compose_graph r r = r &
intersection2 r (opposite_order r) = identity_g (substrate r)).
Proof. ir. app iff_eq. ir.
pose (d:= identity_g (substrate r)).
assert(intersection2 r (opposite_order r) = d). set_extens.
nin (intersection2_both H0).
rwi inverse_graph_rw H2. ee. assert (J (P x) (Q x) = x). aw. wri H4 H1.
cp (order_antisymmetry H H1 H3).
uf d. wr H4. aw. eee. substr_tac. fprops.
ufi d H0. rwi inc_diagonal_rw H0. ee.
assert (J (P x) (Q x) = x). aw. wri H2 H3. wr H3.
assert (related r (P x) (P x)). order_tac.
inter2tac. aw.
assert (is_graph r). fprops.
assert (sub d r). wr H0. red. ir. inter2tac.
assert (sub (compose_graph d r) (compose_graph r r)).
app composition_increasing. uf d. fprops.
assert (sub (compose_graph r r) r). red in H. ee.
rwi idempotent_graph_transitive H4. am. am.
ee. app preorder_prop1. am.
ir. ee. red.
assert (is_graph r). wr H. app composition_is_graph.
ee. red. ee. am. ir. red.
assert (inc (J y y) (identity_g (substrate r))). rw inc_pair_diagonal. au.
wri H0 H3. inter2tac.
rw idempotent_graph_transitive. rw H. fprops. am.
red. ee. am. uf related. ir.
assert (inc (J x y) (opposite_order r)). aw.
assert (inc (J x y) (identity_g (substrate r))). wr H0.
inter2tac. awi H5. ee. am.
Qed.
Lemma preorder_is_preorder: forall r,
preorder r -> preorder_r (related r).
Proof. ir. red. red in H. ee. red. red in H0. ee. am. red.
ir. red in H. ee.
assert (inc x (substrate r)). substr_tac. app H2.
assert (inc y (substrate r)). substr_tac. app H2.
Qed.
Lemma opposite_is_preorder1: forall r,
preorder r -> preorder (opposite_order r).
Proof. ir. nin H. red. assert (is_graph (opposite_order r)). fprops.
assert (sub (substrate (opposite_order r)) (substrate r)). red. ir.
rwi inc_substrate_rw H2. rw inc_substrate_rw.
nin H2; nin H2; awi H2; [ right | left ] ;ex_tac. nin H; am. am.
split. split. am. ir. red. aw. cp (H2 _ H3). nin H. app H5.
split. am. ir. red in H3; red in H4. awi H3. awi H4.
red in H0; ee. red. aw. app (H5 _ _ _ H4 H3).
Qed.
Lemma equivalence_preorder: forall r,
preorder_r r ->
equivalence_r (fun x y => r x y & r y x).
Proof. ir. red. ee. red. ir. intuition. red. ir. red in H. ee. red in H.
app (H _ _ _ H0 H1). app (H _ _ _ H2 H3).
Qed.
Lemma compatible_equivalence_preorder: forall r,
let s := (fun x y => r x y & r y x) in
preorder_r r -> forall x y x' y', r x y -> s x x' -> s y y' -> r x' y'.
Proof. ir. ufi s H1; ufi s H2. ee. red in H. ee. red in H. ee.
pose (H _ _ _ H4 H0). app (H _ _ _ r0 H2).
Qed.
Equivalence relation associated to a preorder
Definition equivalence_associated_o r:= intersection2 r (opposite_order r).
Lemma equivalence_preorder1: forall r,
preorder r ->
is_equivalence (equivalence_associated_o r).
Proof. ir. uf equivalence_associated_o.
assert(is_graph r). app preorder_graph.
assert(is_graph (opposite_order r)). fprops.
cp (inter2_is_graph2 H1(x:=r)).
app symmetric_transitive_equivalence. red. ee. am. uf related. ir.
nin (intersection2_both H3). inter2tac. awi H5. am. aw.
red. ee. am. uf related. ir.
nin (intersection2_both H3). nin (intersection2_both H4).
red in H. ee. red in H9;ee. ufi related H9.
inter2tac. app (H10 _ _ _ H5 H7).
aw. awi H6. awi H8. app (H10 _ _ _ H8 H6).
Qed.
Lemma substrate_equivalence_associated_o: forall r,
preorder r ->
substrate (equivalence_associated_o r) = substrate r.
Proof. ir. cp (equivalence_preorder1 H).
set_extens. cp (reflexivity_e H0 H1).
ufi related H2. ufi equivalence_associated_o H2.
cp (intersection2_first H2). substr_tac.
red in H. ee. red in H. ee. cp (H3 _ H1). red in H4.
assert (inc (J x x) (equivalence_associated_o r)).
uf equivalence_associated_o. inter2tac. rw inverse_graph_rw.
ee. fprops. aw. am. substr_tac.
Qed.
Lemma compatible_equivalence_pre_order: forall r,
let s := (fun x y => r x y & r y x) in
preorder_r r -> forall x y x' y', r x y -> s x x' -> s y y' -> r x' y'.
Proof. ir. ufi s H1; ufi s H2. ee. red in H. ee. red in H. ee.
pose (H _ _ _ H4 H0). app (H _ _ _ r0 H2).
Qed.
Lemma compatible_equivalence_preorder1: forall r u v x y,
preorder r -> related r x y ->
related (equivalence_associated_o r) x u ->
related (equivalence_associated_o r) y v->
related r u v.
Proof. uf related. uf equivalence_associated_o. ir.
nin (intersection2_both H1). awi H4.
nin (intersection2_both H2). awi H6.
red in H. ee. red in H7. ee.
cp (H8 _ _ _ H4 H0). app (H8 _ _ _ H9 H5).
Qed.
Lemma preorder_prop: forall g,
is_graph g ->
preorder g = (sub (identity_g (substrate g)) g & sub (compose_graph g g) g).
Proof. ir. app iff_eq. ir. red in H0. ee. red. ir. rwi inc_diagonal_rw H2. ee.
assert (J (P x) (Q x) = x). aw. wr H5. wr H4.
red in H0. ee. app H6. wrr idempotent_graph_transitive.
ir. ee. red. ee. red. ee. am. ir. uf related. red in H0. app H0.
rw inc_diagonal_rw. aw. fprops. rww idempotent_graph_transitive.
Qed.
Lemma preorder_prop2: forall g,
preorder g -> compose_graph g g = g.
Proof. ir. assert (is_graph g). app preorder_graph. rwi (preorder_prop H0) H.
ee. app preorder_prop1.
Qed.
Lemma preorder_reflexivity: forall r a,
preorder r -> inc a (substrate r) = related r a a.
Proof. ir. red in H. ee. red in H. ee. app iff_eq. ee. app H1.
ir. substr_tac.
Qed.
Compare with
fun_on_quotients
Definition order_associated (r:Set) :=
let s := (graph(canon_proj (equivalence_associated_o r))) in
compose_graph (compose_graph s r) (opposite_order s).
Lemma order_associated_graph: forall r,
is_graph (order_associated r).
Proof. ir. uf order_associated. app composition_is_graph.
Qed.
Lemma compose3_related: forall s r u v,
related (compose_graph (compose_graph s r) (opposite_order s)) u v =
exists x, exists y, related s x u & related s y v & related r x y.
Proof. ir. rw compose_related. app iff_eq. ir. nin H. ee.
awi H0. bwi H. exists x. nin H0. exists x0. intuition.
ir. nin H. nin H. ee.
exists x. ee. bw. aw. exists x0. auto.
Qed.
Lemma order_associated_related1: forall r u v,
preorder r->
related (order_associated r) u v =
( inc u (quotient (equivalence_associated_o r)) &
inc v (quotient (equivalence_associated_o r)) &
exists x, exists y, inc x u & inc y v & related r x y).
Proof. ir. set (s:= equivalence_associated_o r).
set (p:= graph (canon_proj s)).
uf order_associated. fold s. fold p.
assert(is_equivalence s). uf s. app equivalence_preorder1.
rw compose3_related. app iff_eq. ir. nin H1. nin H1. nin H1. nin H2.
ufi p H1. ufi p H2. red in H1. red in H2.
assert (is_function (canon_proj s)). app canon_proj_function.
pose (inc_pr1graph_source H4 H1). awi i.
pose (inc_pr1graph_source H4 H2). awi i0.
assert (u = W x (canon_proj s)). sy. app W_pr. rwi canon_proj_W H5.
assert (v = W x0 (canon_proj s)). sy. app W_pr. rwi canon_proj_W H6.
ee. rw H5. gprops. rw H6. gprops.
exists x. exists x0. ee. rw H5. app inc_itself_class.
rw H6. app inc_itself_class. am. am. am. am. am.
ir. nin H1. nin H2. nin H3. nin H3. ee. exists x. exists x0. ee.
uf p. red. rw related_graph_canon_proj. am. am.
app (inc_in_quotient_substrate H0 H3 H1). am.
uf p. red. rw related_graph_canon_proj. am. am.
app (inc_in_quotient_substrate H0 H4 H2). am. am.
Qed.
Lemma order_associated_related2: forall r u v,
preorder r->
related (order_associated r) u v =
( inc u (quotient (equivalence_associated_o r)) &
inc v (quotient (equivalence_associated_o r)) &
forall x y, inc x u -> inc y v -> related r x y).
Proof. ir. rww order_associated_related1.
set (s:= equivalence_associated_o r).
assert(is_equivalence s). uf s. app equivalence_preorder1.
app iff_eq. ir. eee. nin H3; nin H3. ee. ir.
assert (related s x x1). rww in_class_related. exists u. ee.
wrr inc_quotient. am. am. ufi s H8.
assert (related s x0 y). rww in_class_related. exists v. ee.
wrr inc_quotient. am. am. ufi s H9.
app (compatible_equivalence_preorder1 H H5 H8 H9).
ir. eee. nin (non_empty_in_quotient H0 H1).
nin (non_empty_in_quotient H0 H2). exists y. exists y0. au.
Qed.
Lemma order_associated_substrate: forall r,
preorder r-> substrate (order_associated r) =
(quotient (equivalence_associated_o r)).
Proof. ir.
assert(Ha:is_equivalence (equivalence_associated_o r)).
app equivalence_preorder1.
set_extens. rwi inc_substrate_rw H0. nin H0. nin H0.
assert (related (order_associated r) x x0). red; am.
rwi order_associated_related2 H1. ee. am. am. nin H0.
assert (related (order_associated r) x0 x). red; am.
rwi order_associated_related2 H1. ee. am. am.
app order_associated_graph.
assert (related (order_associated r) x x).
rw order_associated_related2. eee. ir.
assert (related (equivalence_associated_o r) x0 y). rw in_class_related.
exists x. eee. wr inc_quotient. am. am. am.
ufi equivalence_associated_o H3. red; red in H3. inter2tac.
am. substr_tac.
Qed.
Lemma order_associated_order: forall r,
preorder r-> order (order_associated r).
Proof. ir.
assert (is_graph (order_associated r)). app order_associated_graph.
assert(Ha:is_equivalence (equivalence_associated_o r)).
app equivalence_preorder1.
red. ee; split;tv. ir. rwi order_associated_substrate H1.
rw order_associated_related2. eee. ir.
assert (related (equivalence_associated_o r) x y0). rw in_class_related.
exists y. ee. wr inc_quotient. am. am. am. am. am.
ufi equivalence_associated_o H4. red; red in H4. inter2tac. am. am.
ir. rwi order_associated_related2 H1.
rwi order_associated_related2 H2. ee.
rw order_associated_related2. eee. ir.
nin (non_empty_in_quotient Ha H5). red in H. ee. red in H10. ee.
apply H11 with y1. app H6. app H4. am. am. am.
intros x y. do 2 rww order_associated_related2. ir. ee.
nin (non_empty_in_quotient Ha H1). nin (non_empty_in_quotient Ha H2).
cp (H6 _ _ H7 H8). cp (H4 _ _ H8 H7).
assert (related (equivalence_associated_o r) y0 y1).
uf related. uf equivalence_associated_o. inter2tac. aw.
rwi inc_quotient H1. rwi inc_quotient H2.
assert (inc y0 y). rwi is_class_rw H2. ee. rw (H13 y1 y0 H8). equiv_tac. am.
nin (class_dichot H1 H2). am. elim (nondisjoint H7 H12 H13). am. am.
Qed.
Lemma order_associated_pr: forall r,
preorder r ->
order_associated r = image_by_fun (
ext_to_prod(canon_proj (equivalence_associated_o r))
(canon_proj (equivalence_associated_o r))) r.
Proof. ir. set (s:= equivalence_associated_o r).
assert(Ha:is_equivalence s). uf s. app equivalence_preorder1.
assert (Hc:substrate s = substrate r). uf s.
rww substrate_equivalence_associated_o.
assert (Hb:is_function (ext_to_prod (canon_proj s) (canon_proj s))).
app ext_to_prod_function. app canon_proj_function. app canon_proj_function.
rw graph_exten. ir. rw order_associated_related2. fold s.
uf related. uf image_by_fun. app iff_eq. ir. ee.
aw. exists (J (rep u) (rep v)). ee. app H2.
app (inc_rep_itself Ha H0). app (inc_rep_itself Ha H1).
uf related.
assert (class s (rep u) =u). app class_rep.
assert (class s (rep v) =v). app class_rep.
assert (J u v = J (class s (rep u)) (class s (rep v))). rw H3; rw H4. tv.
wri ext_to_prod_rel_W H5. rw H5. app W_pr3. uf ext_to_prod. aw.
ee. fprops. fprops. fprops. am. am. fprops. fprops.
ir. awi H0. nin H0. nin H0.
ufi related H1. pose (W_pr Hb H1). assert (is_pair x). nin H. nin H. app H.
assert (J (P x) (Q x) = x). aw. wri H3 e.
assert (inc (P x) (substrate s)). rw Hc. substr_tac.
assert (inc (Q x) (substrate s)). rw Hc. substr_tac.
rwi ext_to_prod_rel_W e. cp (pr1_def e). cp (pr2_def e).
ee. wr H6. gprops. wr H7. gprops.
ir. assert (inc u (quotient (equivalence_associated_o r))). wr H6. gprops.
assert (inc v (quotient (equivalence_associated_o r))). wr H7. gprops.
assert (related (order_associated r) u v).
rw order_associated_related1. eee. exists (P x).
exists (Q x). ee. wr H6. app inc_itself_class.
wr H7. app inc_itself_class. red. ue. am.
rwi order_associated_related2 H12. ee. app H14. am. am. am. am.
am. fprops. app order_associated_graph.
red. ir. ufi image_by_fun H0. awi H0. nin H0. ee.
cp (inc_pr2graph_target Hb H1). ufi ext_to_prod H2. awi H2. eee.
Qed.
Same axioms as in Bourbaki
Definition order_axioms (r s:Set) :=
(forall x y z, gle r x y -> gle r y z -> gle r x z) &
(forall x y, gle r x y -> gle r y x -> x = y) &
(forall x y, gle r x y -> (inc x s & inc y s)) &
(forall x, gle r x x = inc x s) &
is_graph r.
Lemma axioms_of_order: forall r,
order r = (order_axioms r (substrate r)).
Proof. ir. uf order_axioms. app iff_eq. ir. ee. ir. order_tac.
ir. order_tac. ir. ee; order_tac. ir. sy. app order_reflexivity. fprops.
ir. ee. ufi gle H2. red; ee;red; eee. ir. rww H2.
Qed.
Lemma le_pr: forall r x y,
inc x (substrate r) ->
order r -> gle r x y = (glt r x y \/ x = y).
Proof. ir. uf glt. app iff_eq. ir. nin (equal_or_not x y). ir. au.
left. au. ir. nin H1. eee. wr H1. order_tac.
Qed.
Order morphisms and isomorphisms.
In the second definition we do not assume the function surjective
Definition order_isomorphism f r r':=
(order r) & (order r') &
(bijective f) & (substrate r = source f) & (substrate r' = target f) &
(forall x y, inc x (source f) -> inc y (source f) ->
gle r x y = gle r' (W x f) (W y f)).
Definition order_morphism f r r':=
(order r) & (order r') &
(injective f) & (substrate r = source f) & (substrate r' = target f) &
(forall x y, inc x (source f) -> inc y (source f) ->
gle r x y = gle r' (W x f) (W y f)).
Order induced by
r on a
Definition induced_order (r a:Set):=
intersection2 r (coarse a).
Lemma relation_induced_order: forall r a,
is_graph r -> is_graph (induced_order r a).
Proof. ir. uf induced_order. ap (inter2_is_graph1 H (y:=coarse a)).
Qed.
Lemma related_induced_order: forall r a x y, inc x a -> inc y a ->
gle (induced_order r a) x y = gle r x y.
Proof. ir. uf gle. uf related. uf induced_order. app iff_eq. ir. inter2tac.
ir. inter2tac. uf coarse. fprops.
Qed.
Lemma related_induced_order1: forall r a x y,
gle (induced_order r a) x y -> gle r x y.
Proof. ir. ufi induced_order H. red in H. red in H. red. red. inter2tac.
Qed.
Lemma related_induced_order2: forall r a x y,
glt (induced_order r a) x y -> glt r x y.
Proof. ir. nin H. split. app (related_induced_order1 H). am.
Qed.
Lemma related_induced_order3: forall r a x y,
gle (induced_order r a) x y -> (inc x a & inc y a).
Proof. uf induced_order. ir. red in H. red in H. cp (intersection2_second H).
ufi coarse H0. awi H0. eee.
Qed.
Lemma related_induced_order4: forall r a x y,
glt(induced_order r a) x y -> (inc x a & inc y a).
Proof. ir. nin H. app (related_induced_order3 H).
Qed.
Hint Rewrite related_induced_order : aw.
Lemma substrate_induced_order1: forall r a,
is_reflexive r ->
sub a (substrate r) -> substrate (induced_order r a) = a.
Proof. ir. assert (is_graph (induced_order r a)).
app relation_induced_order. red in H; eee.
uf induced_order. uf coarse. set_extens.
rwi inc_substrate_rw H2.
nin H2; nin H2; cp (intersection2_second H2); awi H3; eee. am.
apply inc_arg1_substrate with x. red. inter2tac.
cp (H0 _ H2). rwii reflexive_inc_substrate H3. fprops.
Qed.
Lemma substrate_induced_order :forall r a,
order r ->
sub a (substrate r) -> substrate (induced_order r a) = a.
Proof. ir. app substrate_induced_order1. red in H;eee. Qed.
Hint Rewrite substrate_induced_order : aw.
Lemma reflexive_induced_order: forall r a,
sub a (substrate r) ->
is_reflexive r -> is_reflexive (induced_order r a).
Proof. ir. red. ee. red in H0; ee. app relation_induced_order. ir.
assert (inc y a). rwi substrate_induced_order1 H1. am. am. am.
assert (inc y (substrate r)). app H. aw. red in H0; ee. app H4.
Qed.
Lemma transitive_induced_order: forall r a,
sub a (substrate r) ->
is_transitive r -> is_transitive (induced_order r a).
Proof. ir. nin H0. red. split. app relation_induced_order.
ir. unfold related in *. unfold induced_order in *.
nin (intersection2_both H2). nin (intersection2_both H3).
app intersection2_inc. app (H1 _ _ _ H4 H6). unfold coarse in *.
awi H5; awi H7. eee.
Qed.
Lemma preorder_induced_order: forall r a,
sub a (substrate r) ->
preorder r -> preorder (induced_order r a).
Proof. ir. nin H0. split.
app reflexive_induced_order. app transitive_induced_order.
Qed.
Lemma order_induced_order: forall r a,
sub a (substrate r) ->
order r -> order (induced_order r a).
Proof. ir. assert (preorder (induced_order r a)).
app preorder_induced_order. app order_preorder. nin H1. red. eee.
red. ee. nin H1;am. uf related. uf induced_order. ir. ee.
cp (intersection2_first H3). cp (intersection2_first H4). order_tac.
Qed.
Hint Resolve order_induced_order: fprops.
Lemma induced_order_substrate: forall r,
order r ->
induced_order r (substrate r) = r.
Proof. ir. uf induced_order. wr intersection2_sub.
app sub_graph_coarse_substrate. fprops.
Qed.
Lemma opposite_induced: forall r x, order r ->
induced_order (opposite_order r) x = opposite_order (induced_order r x).
Proof. ir. uf induced_order. uf opposite_order. uf inverse_graph.
assert (is_graph r). fprops. cp (inter2_is_graph1 H0 (y:=coarse x)).
uf coarse. set_extens.
nin (intersection2_both H2). Ztac. clear H3.
Ztac. awi H5. aw. ee. am. exists (Q x0). app intersection2_inc.
awi H4. aw. eee. exists (P x0).
app intersection2_inc. awi H4. aw. eee.
am. am. am. app intersection2_inc. awi H4. aw.
aw. eee. Ztac. clear H2. awi H3. ee.
nin (intersection2_both H4). awi H7.
app intersection2_inc. Ztac. aw. ee. am. nin H3. exists (Q x0). am.
exists (P x0). am. ee. aw. fprops. am. am. am.
Qed.
Example 1. The function that associates to a partial function its graph.
Is an isomorphism for extends and inclusion
Definition set_of_fgraphs (x y :Set):=
(Zo(powerset (product x y)) (fun z => functional_graph z)).
Definition graph_of_function (x y:Set):=
BL graph (set_of_sub_functions x y)
(set_of_fgraphs x y).
Lemma graph_of_function_sub: forall x y z,
inc z (set_of_sub_functions x y) -> sub (graph z) (product x y).
Proof. ir. bwi H. ee. nin H. nin H. red in H3.
apply (@sub_trans _ _ (product x y) H3).
app product_monotone. rw H1. fprops.
Qed.
Lemma set_of_graphs_pr: forall x y z,
inc z (set_of_sub_functions x y) -> inc (graph z) (set_of_fgraphs x y).
Proof. ir. uf set_of_fgraphs. Ztac. app powerset_inc. app graph_of_function_sub.
bwi H. nin H. nin H. nin H1. wri is_functional H1. eee.
Qed.
Lemma graph_of_function_axioms: forall x y,
transf_axioms(fun g => (graph g)) (set_of_sub_functions x y)
(set_of_fgraphs x y).
Proof. ir. red. ir. app set_of_graphs_pr.
Qed.
Lemma graph_of_function_fonction: forall x y,
is_function (graph_of_function x y).
Proof. ir. uf graph_of_function. ap bl_function. app graph_of_function_axioms.
Qed.
Lemma graph_of_function_W: forall x y f,
inc f (set_of_sub_functions x y) -> W f (graph_of_function x y) = graph f.
Proof. ir. uf graph_of_function. aw. app graph_of_function_axioms.
Qed.
Lemma graph_of_function_bijective: forall x y,
bijective (graph_of_function x y).
Proof. ir. uf graph_of_function. app bl_bijective.
app graph_of_function_axioms. ir. bwi H. bwi H0. ee.
app function_exten1. ue. ir. ufi set_of_fgraphs H. Ztac.
awi H0. assert (is_graph y0). red. ir. set (H0 _ H2). awi i; eee.
exists (corresp (domain y0) y y0). bw. aw. eee.
app is_function_pr. wr is_functional. eee.
red. ir. awi H3. nin H3. set (H0 _ H3). awi i. eee. am.
red. ir. awi H3. nin H3. set (H0 _ H3). awi i. eee. am.
Qed.
Lemma graph_of_function_isomorphism: forall x y,
order_isomorphism (graph_of_function x y)
(opposite_order (extension_order x y))
(inclusion_suborder (set_of_fgraphs x y)).
Proof. ir. cp (extension_is_order x y).
assert (Ha:set_of_sub_functions x y = source (graph_of_function x y)).
uf graph_of_function. aw. red. wr Ha. ee; aw;fprops.
app graph_of_function_bijective.
uf graph_of_function. aw. ir.
rww graph_of_function_W. rww graph_of_function_W.
rw extension_order_pr2. aw.
ap iff_eq; ir; eee; try app set_of_graphs_pr.
Qed.
Example 2. The mapping that associates to a partition the graph of
the equivalence is an order isomorphism
Definition graph_of_partition x :=
BL(fun y => partition_relation_set y x)
(set_of_partition_set x)(powerset (coarse x)).
Lemma gop_axioms: forall x,
transf_axioms (fun y => partition_relation_set y x)
(set_of_partition_set x) (powerset (coarse x)).
Proof. ir. red. ir. rwi set_of_partition_rw H. app powerset_inc.
app sub_partition_relation_set_coarse.
Qed.
Lemma gop_W: forall x y,
partition y x ->
W y (graph_of_partition x) = partition_relation_set y x.
Proof. ir. uf graph_of_partition. aw. app gop_axioms. rww set_of_partition_rw.
Qed.
Lemma gop_morphism: forall x,
order_morphism (graph_of_partition x) (coarser x)
(opposite_order (inclusion_order (coarse x))).
Proof. ir. assert (order (inclusion_order (coarse x))). app inclusion_is_order.
assert (is_graph (inclusion_order (coarse x))). fprops.
assert (Hd:source (graph_of_partition x) = (set_of_partition_set x)).
uf graph_of_partition. aw.
assert (Ha:order (coarser x)). app coarser_order.
red. rw Hd. ee. am. app opposite_is_order. uf graph_of_partition.
app bl_injective. app gop_axioms. intros u v.
do 2 rw set_of_partition_rw. ir.
app (order_antisymmetry (coarser_order x) (a:=u) (b:=v)).
wrr partition_relation_set_order. rw H3. fprops.
wrr partition_relation_set_order. rw H3. fprops.
rww coarser_substrate. uf graph_of_partition. aw.
uf gle. intros a b. do 2 rww set_of_partition_rw. ir.
wrr partition_relation_set_order.
rww gop_W. rww gop_W. rw inverse_graph_pr2. aw.
app iff_eq. ir. ee;try app sub_partition_relation_set_coarse. am.
ir. eee.
Qed.
Example 3: Compare preorder relations
Definition set_of_preorders x :=
Zo (powerset (coarse x))(fun z => substrate z = x & preorder z).
Lemma set_of_preorders_rw: forall x z,
inc z (set_of_preorders x) = (substrate z = x & preorder z).
Proof. ir. uf set_of_preorders. app iff_eq. ir. Ztac. am. ir. Ztac. ee.
app powerset_inc. wr H. app sub_graph_coarse_substrate. app preorder_graph.
Qed.
Definition coarser_preorder x :=
inclusion_suborder (set_of_preorders x).
Lemma coarser_preorder_order: forall x,
order (coarser_preorder x).
Proof. ir. uf coarser_preorder. app subinclusion_is_order.
Qed.
Lemma coarser_preorder_substrate: forall x,
substrate (coarser_preorder x) = set_of_preorders x.
Proof. ir. uf coarser_preorder. app substrate_subinclusion_order.
Qed.
Lemma coarser_preorder_related: forall x u v,
related (coarser_preorder x) u v =
(preorder u & preorder v & substrate u = x & substrate v = x & sub u v).
Proof. ir. uf coarser_preorder. rw subinclusion_order_rw.
do 2 rw set_of_preorders_rw. ap iff_eq; ir; intuition.
Qed.
Lemma coarser_preorder_related1: forall x u v,
related (coarser_preorder x) u v =
(preorder u & preorder v & substrate u = x & substrate v = x &
forall a b, inc a x -> inc b x -> related u a b -> related v a b).
Proof. ir. rw coarser_preorder_related. ap iff_eq. ir. eee.
ir. uf related. ufi related H6. app H3.
ir. eee. assert (is_graph u). app preorder_graph.
red. ir. assert (is_pair x0). app H4.
assert (J (P x0) (Q x0) = x0). aw.
wri H7 H5. assert (inc (P x0) x). wr H1. substr_tac.
assert (inc (Q x0) x). wr H1. substr_tac.
ufi related H3. wr H7. ap (H3 _ _ H8 H9 H5).
Qed.
If g is a family of orders, it induces an order of the product of f,
the family of susbtrates of g
Definition fam_of_substrates g :=
L (domain g) (fun i => substrate (V i g)).
Definition prod_of_substrates g := productb (fam_of_substrates g).
Definition product_order_r (g:Set): EEP :=
fun x x' => forall i, inc i (domain g) -> gle (V i g) (V i x) (V i x').
Definition product_order g :=
graph_on (product_order_r g)(prod_of_substrates g).
Definition product_order_axioms g:=
fgraph g & (forall i, inc i (domain g) -> order (V i g)).
Lemma prod_of_substrates_rw: forall g x,
product_order_axioms g ->
(inc x (prod_of_substrates g) = (fgraph x & domain x = domain g &
forall i, inc i (domain g) -> inc (V i x) (substrate (V i g)))).
Proof. ir. nin H. uf prod_of_substrates. uf fam_of_substrates. aw. bw.
ap iff_eq; ir; eee. rwi H2 H3. ir. set (H3 _ H4). bwi i0. am. am.
ir. rwi H2 H4. bw. app H3. gprops.
Qed.
Hint Rewrite prod_of_substrates_rw : aw.
Lemma product_order_order: forall g,
product_order_axioms g -> order (product_order g).
Proof. ir. assert (Ha: fgraph (fam_of_substrates g)).
uf fam_of_substrates. gprops.
uf product_order. uf product_order_r. assert (Hb:=H). nin H.
app order_from_rel1.
red. ir. set (H1 _ H3). set (H2 _ H3). set (H0 _ H3). order_tac.
uf prod_of_substrates. ir. ap (productb_exten Ha H1 H2).
uf fam_of_substrates. bw. ir.
set (H3 _ H5). set (H4 _ H5). set (H0 _ H5). order_tac.
ir. set (H0 _ H2). order_tac. awii H1. ee. app H4.
Qed.
Lemma product_order_related: forall g x x',
product_order_axioms g ->
gle (product_order g) x x' =
(inc x (prod_of_substrates g) & inc x' (prod_of_substrates g) &
forall i, inc i (domain g) -> gle (V i g) (V i x)(V i x')).
Proof. ir. uf product_order. uf gle. uf related. rw graph_on_rw0. app iff_eq.
Qed.
Hint Rewrite product_order_related : bw.
Hint Resolve product_order_order: fprops.
Lemma product_order_substrate: forall g,
product_order_axioms g -> substrate (product_order g) = prod_of_substrates g.
Proof. ir. uf product_order. app substrate_graph_on.
ir. red. ir. nin H. set (H2 _ H1). order_tac. awi H0. ee. app H4. split; am.
Qed.
Hint Rewrite product_order_substrate : aw.
Lemma product_order_def: forall g,
let f := fam_of_substrates g in
product_order_axioms g ->
image_by_fun (prod_of_products_canon f f) (product_order g)= (productb g).
Proof. ir. assert (Hc: domain f = domain g). uf f. uf fam_of_substrates. bw.
assert (Hf: fgraph g). nin H; am.
set (F:= corresp (domain f) (range f) f).
assert (fgraph f). uf f. uf fam_of_substrates. gprops.
assert(is_function F). uf F. red in H. ee. app is_function_pr. fprops.
assert(graph F = f). uf F. aw.
assert (is_function (prod_of_products_canon f f)).
cp (popc_bijection H1 H1 (refl_equal (source F))). wr H2. fct_tac.
assert (Ha:=product_order_order H).
assert (sub (product_order g) (source (prod_of_products_canon f f))).
uf prod_of_products_canon. aw. assert (is_graph (product_order g)).
fprops. cp (sub_graph_coarse_substrate H4).
rwi (product_order_substrate H) H5. am.
set_extens. awii H5. nin H5. ee. wri H2 H6. rwii popc_W H6. wr H6.
assert (gle (product_order g) (P x0) (Q x0)).
assert (is_pair x0). nin Ha. nin H7. app H7. red. red. aw.
rwii product_order_related H7. ee. set (t := P x0) in *.
uf prod_of_function. aw. awii H7. ee. gprops. bw. bw. ir. bw. app H9. ue.
ufi prod_of_products_canon H4. awi H4. rw H2. app H4.
aw. set (x1 := L (domain g) (fun i => P (V i x))).
set (x2:= (L (domain g) (fun i => Q (V i x)))).
assert (Hd:=product_order_related x1 x2 H). ufi related Hd.
assert (inc x1 (prod_of_substrates g)). uf x1. aw. ee. gprops. bw. ir. bw.
app inc_pr1_substrate. awi H5. ee. app H8. ue. am.
assert (inc x2 (prod_of_substrates g)). uf x2. aw. ee. gprops. bw. ir. bw.
app inc_pr2_substrate. awi H5. ee. app H9. ue. am.
assert (He: forall i, inc i (domain g) -> is_pair (V i x)).
ir. awi H5. ee. nin H. set (H11 _ H8). rwi H9 H10. set (H10 _ H8).
assert (is_graph (V i g)). fprops. app H12. am.
exists (J x1 x2). split. ufi gle Hd. ufi related Hd. rww Hd. eee.
ir. uf x1. uf x2. bw. aw. awi H5. ee. app H10. ue. am. app He.
assert (Hb:source F = domain f). uf F. aw.
wr H2. rww popc_W. aw. sy. uf prod_of_function. awi H5.
ee. app fgraph_exten. gprops. uf x1. bw.
ir. rwi H8 H10. uf x1. uf x2. bw. aw. app He. am. rw H2. fprops.
Qed.
Order on graphs of functions
x->y,
induced by an order g on the target.
This is a special case of product order.
Definition graph_order_r (x g:Set): EEP :=
fun z z' => forall i, inc i x -> gle g (V i z) (V i z').
Definition cst_graph x y:= L x (fun _ => y).
Definition graph_order x y g :=
graph_on (graph_order_r x g) (set_of_gfunctions x y).
Lemma product_order_axioms_x:forall x g, order g ->
product_order_axioms (cst_graph x g).
Proof. ir. red. uf cst_graph. ee. gprops. bw. ir. bw.
Qed.
Lemma cst_graph_pr: forall x y,
productb (cst_graph x y) = set_of_gfunctions x y.
Proof. ir. assert (x = domain (cst_graph x y)). uf cst_graph. bw.
rw H. wr product_eq_graphset. wrr H. uf cst_graph. gprops. wr H.
uf cst_graph. ir. bw.
Qed.
Lemma graph_order_r_pr: forall x g z z',
graph_order_r x g z z' =
product_order_r (cst_graph x g) z z'.
Proof. ir. assert (domain (cst_graph x g) = x). uf cst_graph. bw.
uf product_order_r. rw H. uf cst_graph. app iff_eq. ir. bw. app H0.
red. ir. set (H0 _ H1). bwi g0. am. am.
Qed.
Lemma graph_order_pr1:forall x y g, substrate g = y ->
(set_of_gfunctions x y) = prod_of_substrates (cst_graph x g).
Proof. ir. wr cst_graph_pr. uf prod_of_substrates. uf fam_of_substrates.
uf cst_graph. bw. app uneq. app L_exten1. ir. bw. sy; am.
Qed.
Lemma graph_order_pr:forall x y g, substrate g = y ->
graph_order x y g = product_order (cst_graph x g).
Proof. ir. assert (graph_order_r x g = product_order_r (cst_graph x g)).
app arrow_extensionality. ir. app arrow_extensionality.
ir. app (graph_order_r_pr). uf graph_order.
uf product_order. rw H0. rww (graph_order_pr1 x H).
Qed.
Lemma graph_order_order: forall x y g, order g -> substrate g = y ->
order (graph_order x y g).
Proof. ir. rww graph_order_pr. app product_order_order.
app product_order_axioms_x.
Qed.
Lemma graph_order_substrate: forall x y g, order g -> substrate g = y ->
substrate (graph_order x y g) = set_of_gfunctions x y.
Proof. ir. rww graph_order_pr. rw product_order_substrate.
wrr (graph_order_pr1 x H0). app product_order_axioms_x.
Qed.
Order on functions
x->y, induced by an order r on the target
Definition function_order_r x y r f g :=
is_function f & is_function g & source f = x & target f = y
& source g =x & target g = y &
forall i, inc i x -> gle r (W i f) (W i g).
Definition function_order x y r :=
graph_on(fun u v => function_order_r x y r u v)
(set_of_functions x y).
Lemma function_order_reflexive: forall x y r u,
order r -> substrate r = y ->
inc u (set_of_functions x y) -> gle (function_order x y r) u u.
Proof. ir. red. red. uf function_order. uf graph_on. Ztac. fprops.
aw. rwi set_of_functions_rw H1. red. eee. ir. order_tac. rw H0. wr H3.
app inc_W_target. ue.
Qed.
Lemma function_order_substrate: forall x y r,
order r -> substrate r = y ->
substrate (function_order x y r) = set_of_functions x y.
Proof. ir. assert (is_graph (function_order x y r)).
uf function_order. app graph_on_graph. ee. set_extens.
rw set_of_functions_rw.
rwi inc_substrate_rw H2. nin H2; nin H2; ufi function_order H2;
ufi graph_on H2; Ztac; awi H3; eee. am.
assert (inc (J x0 x0) (function_order x y r)). app function_order_reflexive.
substr_tac.
Qed.
Lemma function_order_pr:forall x y r f f',
order r -> substrate r = y ->
gle (function_order x y r) f f' =
(inc f (set_of_functions x y) &
inc f' (set_of_functions x y) &
forall i, inc i x -> gle r (W i f) (W i f')).
Proof. ir. uf gle. uf related. uf function_order. uf graph_on. app iff_eq. ir.
Ztac. awi H2. ee. aw. au. aw; au. red in H3. ee. awi H15. am.
ir. ee. Ztac. fprops. red. awi H1. awi H2. aw. eee.
Qed.
Lemma function_order_order: forall x y r,
order r -> substrate r = y -> order (function_order x y r).
Proof. ir. red. assert (is_graph (function_order x y r)).
uf function_order. app graph_on_graph. ee; split;tv.
rw function_order_substrate. ir. app function_order_reflexive. am. am.
uf related. uf function_order. uf graph_on. ir. order_tac.
awi H4. awi H6. ee. Ztac. aw. eee.
unfold function_order_r in H5, H7 |- *. awi H5; awi H7; aw. eee.
ir. cp (H29 _ H30). cp (H23 _ H30). order_tac.
uf related. uf function_order. uf graph_on. ir. order_tac.
awi H4. awi H5. awi H7. ee. unfold function_order_r in H5, H7. ee.
app function_exten. ue. ue. ir. rwi H19 H24.
cp (H23 _ H24). cp (H17 _ H24). order_tac.
Qed.
The mapping that associates to a function its graph is an isomorphism for the two orders defined above
Lemma function_order_isomorphism: forall x y r,
order r -> substrate r = y ->
order_isomorphism (BL graph (set_of_functions x y)(set_of_gfunctions x y))
(function_order x y r)(graph_order x y r).
Proof. ir. red. ee. app function_order_order. app graph_order_order.
app graph_bijective. rww function_order_substrate. aw. aw.
rww graph_order_substrate. aw. ir.
cp (graph_axioms (x:=x) (y:=y)). aw.
rww function_order_pr. uf W. simpl.
uf gle. uf graph_order. uf graph_on. uf graph_on. uf graph_order_r.
uf related. app iff_eq. ir. Ztac. fprops. aw. intuition.
ir. Ztac. eee. awi H6. am.
Qed.
Special case of a product of 2 orders
Definition product2_order f g:=
graph_on (fun x x' => gle f (P x) (P x') & gle g (Q x) (Q x'))
(product (substrate f)(substrate g)).
Lemma product2_order_pr: forall f g x x',
gle (product2_order f g) x x' =
(inc x (product (substrate f)(substrate g)) &
inc x' (product (substrate f)(substrate g)) &
gle f (P x) (P x') & gle g (Q x) (Q x')).
Proof. ir. uf product2_order. uf graph_on. uf gle. uf related.
uf graph_on. ap iff_eq; ir. Ztac. rwi product_inc_rw H0. awi H1. eee.
rwi pr1_pair H3. am. rwi pr2_pair H4. am.
eee. Ztac. fprops. rw pr1_pair. rw pr2_pair. eee.
Qed.
Lemma product2_order_preorder_substrate: forall f g,
preorder f -> preorder g -> substrate (product2_order f g) =
product (substrate f) (substrate g).
Proof. ir. uf product2_order. app substrate_graph_on.
ir. awi H1. ee. nin H. nin H. app H5. nin H0. nin H0. app H5.
Qed.
Lemma product2_order_substrate: forall f g,
order f -> order g -> substrate (product2_order f g) =
product (substrate f) (substrate g).
Proof. ir. app product2_order_preorder_substrate. app order_preorder.
app order_preorder.
Qed.
Lemma product2_order_preorder: forall f g,
preorder f -> preorder g -> preorder (product2_order f g).
Proof. ir. uf product2_order. app preorder_from_rel.
split. red. ir. eee. nin H. nin H5. app (H6 _ _ _ H1 H2).
nin H0. nin H5. app (H6 _ _ _ H4 H3).
red. ir. nin H. nin H. nin H0. nin H0. nin H1. red in H1. red in H6.
ee. app H3. substr_tac. app H5. substr_tac.
app H3. substr_tac. app H5. substr_tac.
Qed.
Lemma product2_order_order: forall f g,
order f -> order g -> order (product2_order f g).
Proof. ir. assert (preorder (product2_order f g)).
app product2_order_preorder. app order_preorder. app order_preorder.
nin H1. red. eee. red. split. nin H1. am. intros x y.
rw product2_order_pr. rw product2_order_pr. ir. eee.
app pair_extensionality. awi H3; eee. awi H8; eee.
order_tac. order_tac.
Qed.
Definition increasing_fun f r r':=
is_function f & order r & order r' & substrate r = source f
& substrate r' = target f &
forall x y, gle r x y -> gle r' (W x f) (W y f).
Definition decreasing_fun f r r':=
is_function f & order r & order r' & substrate r = source f
& substrate r' = target f &
forall x y, gle r x y -> gge r' (W x f) (W y f).
Definition monotone_fun f r r':=
increasing_fun f r r' \/ decreasing_fun f r r'.
Lemma opposite_gle: forall r x y, order r ->
gle (opposite_order r) x y = gle r y x.
Proof. ir. uf gle. uf related. aw.
Qed.
Lemma opposite_gge: forall r x y, order r ->
gge (opposite_order r) x y = gle r x y.
Proof. ir. uf gge. aw. uf gle. uf related. aw.
Qed.
Hint Rewrite opposite_gle opposite_gge: aw.
Monotonicity and opposite order
Lemma increasing_fun_reva : forall f r r',
increasing_fun f r r' -> decreasing_fun f r (opposite_order r').
Proof. uf increasing_fun; uf decreasing_fun. ir. eee. aw.
red. ir. aw. app H4.
Qed.
Lemma increasing_fun_revb : forall f r r',
increasing_fun f r r' -> decreasing_fun f (opposite_order r) r'.
Proof. uf increasing_fun; uf decreasing_fun. ir. eee. aw.
red. ir. awi H5. red. app H4. am.
Qed.
Lemma decreasing_fun_reva : forall f r r',
decreasing_fun f r r' -> increasing_fun f r (opposite_order r').
Proof. uf increasing_fun; uf decreasing_fun. ir. eee. aw.
red. ir. aw. app H4.
Qed.
Lemma decreasing_fun_revb : forall f r r',
decreasing_fun f r r' -> increasing_fun f (opposite_order r) r'.
Proof. uf increasing_fun; uf decreasing_fun. ir. eee. aw.
red. ir. awi H5. app H4. am.
Qed.
Lemma monotone_fun_reva : forall f r r',
monotone_fun f r r' -> monotone_fun f r (opposite_order r').
Proof. uf monotone_fun. ir. nin H. right. app increasing_fun_reva.
left. app decreasing_fun_reva.
Qed.
Lemma monotone_fun_revb : forall f r r',
monotone_fun f r r' -> monotone_fun f (opposite_order r) r'.
Proof. uf monotone_fun. ir. nin H. right. app increasing_fun_revb.
left. app decreasing_fun_revb.
Qed.
Strict monotone functions
Definition strict_increasing_fun f r r':=
is_function f & order r & order r' & substrate r = source f
& substrate r' = target f &
forall x y, glt r x y -> glt r' (W x f) (W y f).
Definition strict_decreasing_fun f r r':=
is_function f & order r & order r' & substrate r = source f
& substrate r' = target f &
forall x y, glt r x y -> ggt r' (W x f) (W y f).
Definition strict_monotone_fun f r r':=
strict_increasing_fun f r r' \/ strict_decreasing_fun f r r'.
Lemma glt_inva: forall r x y,
order r -> glt r x y = ggt (opposite_order r) x y.
Proof. ir. uf ggt; uf glt. aw.
Qed.
Lemma ggt_inva: forall r x y,
order r -> ggt r x y = glt (opposite_order r) x y.
Proof. ir. uf ggt; uf glt. aw.
Qed.
Lemma ggt_invb: forall r x y,
ggt r x y = glt r y x.
Proof. ir. uf ggt; uf glt. uf gge. app iff_eq. ir. eee. ir. eee.
Qed.
Lemma strict_increasing_fun_reva : forall f r r',
strict_increasing_fun f r r' -> strict_decreasing_fun f r (opposite_order r').
Proof. uf strict_increasing_fun; uf strict_decreasing_fun. ir. eee.
aw. ir. wr glt_inva. app H4. am.
Qed.
Lemma strict_increasing_fun_revb : forall f r r',
strict_increasing_fun f r r' -> strict_decreasing_fun f (opposite_order r) r'.
Proof. uf strict_increasing_fun; uf strict_decreasing_fun. ir. eee.
aw. ir. wrii ggt_inva H5. rwii ggt_invb H5. rww ggt_invb. app H4.
Qed.
Lemma strict_decreasing_fun_reva : forall f r r',
strict_decreasing_fun f r r' -> strict_increasing_fun f r (opposite_order r').
Proof. uf strict_increasing_fun; uf strict_decreasing_fun. ir. eee.
aw. ir. wrr ggt_inva. app H4.
Qed.
Lemma strict_decreasing_fun_revb : forall f r r',
strict_decreasing_fun f r r' -> strict_increasing_fun f (opposite_order r) r'.
Proof. uf strict_increasing_fun; uf strict_decreasing_fun. ir. eee.
aw. ir. wrii ggt_inva H5. rwii ggt_invb H5. wrr ggt_invb. app H4.
Qed.
Lemma strict_monotone_fun_reva : forall f r r',
strict_monotone_fun f r r' -> strict_monotone_fun f r (opposite_order r').
Proof. uf strict_monotone_fun. ir. nin H. right. app strict_increasing_fun_reva.
left. app strict_decreasing_fun_reva.
Qed.
Lemma strict_monotone_fun_revb : forall f r r',
strict_monotone_fun f r r' -> strict_monotone_fun f (opposite_order r) r'.
Proof. uf strict_monotone_fun. ir. nin H. right. app strict_increasing_fun_revb.
left. app strict_decreasing_fun_revb.
Qed.
Example of monotone functions
Lemma constant_fun_increasing: forall f r r',
order r -> order r' -> substrate r = source f ->
substrate r' = target f -> is_constant_function f ->
increasing_fun f r r'.
Proof. ir. red. red in H3. eee. ir.
assert (inc x (source f)). wr H1. order_tac.
assert (inc y (source f)). wr H1. order_tac.
rw (H4 _ _ H6 H7). order_tac. ue.
Qed.
Lemma constant_fun_decreasing: forall f r r',
order r -> order r' -> substrate r = source f ->
substrate r' = target f -> is_constant_function f ->
decreasing_fun f r r'.
Proof. ir. red. red in H3. eee. red. ir.
assert (inc x (source f)). wr H1. order_tac.
assert (inc y (source f)). wr H1. order_tac.
rw (H4 _ _ H6 H7). order_tac. ue.
Qed.
Lemma identity_increasing_decreasing : forall x,
let r := identity_g x in
(increasing_fun (identity x) r r &decreasing_fun (identity x) r r).
Proof. ir. cp (diagonal_order x). cp (diagonal_substrate x).
cp (identity_function x).
split. red. eee. aw. aw. red. simpl. ir. srw. wr H0. fold r. order_tac.
wr H0. fold r. order_tac.
red. eee. aw. aw. ir. ufi r H2. red in H2. red in H2. awi H2. nin H2. wr H3.
srw. red. red. red. uf r. aw. au.
Qed.
Lemma complementary_decreasing: forall E,
strict_decreasing_fun(BL (fun X => complement E X)(powerset E)(powerset E))
(inclusion_order E) (inclusion_order E).
Proof. ir. red. set (r:=inclusion_order E). assert(order r). uf r. fprops.
aw. aw.
assert(substrate r = powerset E). uf r. aw.
assert (transf_axioms (fun X => complement E X)
(powerset E) (powerset E)). red. intro c. rw powerset_inc_rw. ir.
rw powerset_inc_rw. app sub_complement. eee. app bl_function.
red. ir. ufi r H2. nin H2. awi H2. nin H2; nin H4.
assert (inc x (powerset E)). aw.
assert (inc y (powerset E)). aw. uf r. uf gge. aw.
ee. app sub_complement. app sub_complement. red. ir. srw. srwi H8.
ee. am. dneg. app H5. dneg. cp (f_equal (complement E) H8). srwi H9; am.
Qed.
Definition set_of_majorants1 x r:=
Zo (substrate r)(fun y => gle r x y).
Lemma set_of_majorants1_pr: forall x y r,
order r -> inc x (substrate r) -> inc y (substrate r) ->
(gle r x y = sub (set_of_majorants1 y r) (set_of_majorants1 x r)).
Proof. ir. uf set_of_majorants1. app iff_eq. ir. red. ir. Ztac.
clear H3. Ztac. order_tac.
ir. assert (inc y (Zo (substrate r) (fun y0 => related r y y0))).
Ztac. order_tac. cp (H2 _ H3). clear H3. Ztac. am.
Qed.
Lemma set_of_majorants1_decreasing: forall r,
order r ->
strict_decreasing_fun(BL (fun x=> (set_of_majorants1 x r))
(substrate r)(powerset (substrate r))) r (inclusion_order (substrate r)).
Proof. red. ir. bw. aw. set (E:= substrate r).
assert (order (inclusion_order E)). fprops.
assert (substrate (inclusion_order E) = powerset E). aw.
assert (transf_axioms (fun x => set_of_majorants1 x r) E (powerset E)).
red. ir. app powerset_inc. red. ir. ufi set_of_majorants1 H3. Ztac. am.
eee. app bl_function. ir. uf ggt. uf gge.
assert (inc x E). uf E. order_tac. assert (inc y E). uf E. order_tac.
aw. nin H3. split. ee. app powerset_sub. app H2. app powerset_sub. app H2.
rwii set_of_majorants1_pr H3. dneg.
assert (gle r y x). rww set_of_majorants1_pr. rw H7. fprops. order_tac.
Qed.
Lemma strict_increasing_from_injective: forall f r r',
injective f -> increasing_fun f r r' -> strict_increasing_fun f r r'.
Proof. ir. red. red in H0. nin H0. eee. ir.
red in H6; ee. red. ee. app H5. dneg. nin H. app H9. wr H3. order_tac.
wr H3. order_tac.
Qed.
Lemma strict_decreasing_from_injective: forall f r r',
injective f ->decreasing_fun f r r' -> strict_decreasing_fun f r r'.
Proof. ir. red. red in H0. nin H0. eee. ir.
red in H6; ee. red. ee. app H5. dneg. nin H. app H9. wr H3. order_tac.
wr H3. order_tac.
Qed.
Lemma strict_monotone_from_injective: forall f r r',
injective f -> monotone_fun f r r' -> strict_monotone_fun f r r'.
Proof. ir. red in H0. red. nin H0. left. app strict_increasing_from_injective.
right. app strict_decreasing_from_injective.
Qed.
Lemma order_isomorphism_increasing: forall f r r',
order_isomorphism f r r' ->
strict_increasing_fun f r r'.
Proof. ir. red in H. ee. red in H1. ee. app strict_increasing_from_injective.
red. eee. fct_tac. red. ir. wrr H4. wr H2. order_tac. wr H2. order_tac.
Qed.
Lemma order_morphism_increasing: forall f r r',
order_morphism f r r' ->
strict_increasing_fun f r r'.
Proof. ir. red in H. ee. app strict_increasing_from_injective.
red. eee. fct_tac. red. ir. wrr H4. wr H2. order_tac. wr H2. order_tac.
Qed.
Lemma order_isomorphism_pr: forall f r r',
order r -> order r' ->
bijective f -> substrate r = source f -> substrate r' = target f ->
(order_isomorphism f r r' =
(increasing_fun f r r' & increasing_fun (inverse_fun f) r' r)).
Proof. ir. uf order_isomorphism. cp (bijective_inv_function H1).
assert (Ha:source f = target (inverse_fun f)). uf inverse_fun. aw.
assert (Hb:target f = source (inverse_fun f)). uf inverse_fun. aw.
app iff_eq. ir. ee. red. ir. eee. fct_tac.
red. ir. wrr H10. wr H8. order_tac. wr H8. order_tac. red. eee.
ir. rwi Ha H10. assert (inc x (target f)). wr H3. order_tac.
assert (inc y (target f)). wr H3. order_tac.
rww H10; try app inc_W_target.
wr (W_inverse H7 H12 (refl_equal (W x (inverse_fun f)))).
wrr (W_inverse H7 H13 (refl_equal (W y (inverse_fun f)))). ue. ue.
ir. eee. ir. red in H5; red in H6; ee.
app iff_eq. ir. app H18. ir. rw (W_inverse2 H1 H7 (refl_equal (W x f))).
rw (W_inverse2 H1 H8 (refl_equal (W y f))). ee.
app H13;simpl; app inc_W_target.
Qed.
Theorem decreasing_composition: forall u v r r',
decreasing_fun u r r' -> decreasing_fun v r' r ->
(forall x, inc x (substrate r) -> gle r (W (W x u) v) x) ->
(forall x', inc x' (substrate r') -> gle r' (W (W x' v) u) x') ->
(compose u (compose v u) = u & compose v (compose u v) = v).
Proof. ir. red in H; red in H0. ee.
assert (composable v u). red. eee.
assert (is_function (compose v u)). fct_tac.
assert (composable u (compose v u)). red. eee. aw. ue.
app function_exten. fct_tac. aw. aw. aw.
ir. aw.
wri H10 H16. cp (H1 _ H16). cp (H12 _ _ H17).
assert (inc (W x u) (substrate r')). rw H11. app inc_W_target. ue.
cp (H2 _ H19). red in H18. order_tac. aw.
assert (composable u v). red. eee.
assert (is_function (compose u v)). fct_tac. aw.
assert (composable v (compose u v)). red. eee. aw. ue.
app function_exten. fct_tac. aw. aw. aw.
ir. aw.
wri H5 H16. cp (H2 _ H16). cp (H7 _ _ H17).
assert (inc (W x v) (substrate r)). rw H6. app inc_W_target. ue.
cp (H1 _ H19). red in H18. order_tac.
Qed.
Lemma order_isomorphism_opposite: forall g r r',
order_isomorphism g r r' ->
order_isomorphism g (opposite_order r) (opposite_order r').
Proof. uf order_isomorphism. ir. eee. aw. aw. ir. aw. app H4.
Qed.
Definition maximal_element r a:=
inc a (substrate r) & forall x, gle r a x -> x = a.
Definition minimal_element r a:=
inc a (substrate r) & forall x, gle r x a -> x = a.
Lemma maximal_element_opp: forall r a,
order r -> maximal_element r a -> minimal_element (opposite_order r) a.
Proof. uf maximal_element. ir. nin H0. red. aw.
split. am. ir. app H1. awi H2. am. am.
Qed.
Lemma minimal_element_opp: forall r a,
order r -> minimal_element r a -> maximal_element (opposite_order r) a.
Proof. ir. red in H0; nin H0. red. aw. split. am.
ir. app H1. awi H2. am. am.
Qed.
Lemma maximal_opposite: forall r x,
order r -> maximal_element (opposite_order r) x = minimal_element r x.
Proof. ir. app iff_eq. assert (order (opposite_order r)). fprops.
ir. cp (maximal_element_opp H0 H1).
ufi opposite_order H2. rwi inverse_graph_involutive H2. am. fprops.
ir. app minimal_element_opp.
Qed.
Lemma singleton_pr: forall a b,
(a = singleton b) = (inc b a & forall u, inc u a -> u = b).
Proof. ir. ap iff_eq; ir. rw H. eee. ir. db_tac.
ee. set_extens. rw (H0 _ H1). fprops. db_tac.
Qed.
Lemma minimal_inclusion: forall E y,
let F:= complement (powerset E) (singleton emptyset) in
inc y F -> (minimal_element (inclusion_suborder F) y = is_singleton y).
Proof. ir. assert (Ha: forall x, inc x F = (sub x E & nonempty x)).
ir. uf F. srw. aw. ap iff_eq; ir; eee.
nin (emptyset_dichot x). contradiction. am. nin H1. red. ir. rwi H2 H1.
elim (emptyset_pr H1).
app iff_eq. ir. nin H0. awi H0. rwi Ha H0. nin H0. nin H2.
assert (inc (singleton y0) F). rw Ha. ee. app sub_singleton. app H0.
app nonempty_singleton. assert (singleton y0 = y). app H1. aw. aw.
intuition. app sub_singleton. exists y0. sy;tv.
ir. red. aw. split. am. ir. awi H1. ee. app extensionality.
rwi is_singleton_rw H0. nin H0. red. ir.
rwi Ha H1. nin H1. nin H6. rww (H4 _ _ H5 (H3 _ H6)).
Qed.
Maximal partial function for extension order are total functions
Lemma maximal_prolongation: forall E F x,
nonempty F -> inc x (set_of_sub_functions E F) ->
maximal_element (opposite_order (extension_order E F)) x = (source x = E).
Proof. ir. rw maximal_opposite.
app iff_eq. ir. nin H1. bwi H0. ee.
app extensionality. red. ir. ex_middle. nin H.
assert (gle (extension_order E F) (tack_on_f x x0 y) x).
rww extension_order_pr1. eee. bw.
eee. uf tack_on_f. aw. red. ir. nin (tack_on_or H7). app H3. ue.
uf tack_on_f. aw. rw H4. set_extens. rwi tack_on_inc H7. nin H7. am.
rw H7. am. fprops. bw. eee. uf tack_on_f. aw. fprops.
wr (H2 _ H7). uf tack_on_f. aw. au.
ir. red. aw. split. am. ir. rwi extension_order_rw H2. ee. bwi H2. bwi H3.
eee. sy; app function_exten. cp (source_extends H4). app extensionality. ue.
ue. ir. ap (W_extends H4 H9). fprops.
Qed.
Definition greatest_element r a:=
inc a (substrate r) & forall x, inc x (substrate r) -> gle r x a.
Definition least_element r a:=
inc a (substrate r) & forall x, inc x (substrate r) -> gle r a x.
Lemma unique_greatest: forall a b r,
order r -> greatest_element r a -> greatest_element r b -> a = b.
Proof. ir. nin H0. nin H1. ap (order_antisymmetry H (H3 _ H0) (H2 _ H1)).
Qed.
Lemma unique_least: forall a b r,
order r -> least_element r a -> least_element r b -> a = b.
Proof. ir. nin H0. nin H1. ap (order_antisymmetry H (H2 _ H1) (H3 _ H0)).
Qed.
Definition the_least_element r:=
choose (fun x=> least_element r x).
Lemma the_least_element_pr: forall r,
order r -> (exists u, least_element r u) ->
least_element r (the_least_element r).
Proof. ir. uf the_least_element. app choose_pr.
Qed.
Definition the_greatest_element r:=
choose (fun x=> greatest_element r x).
Lemma the_greatest_element_pr: forall r,
order r -> (exists u, greatest_element r u) ->
greatest_element r (the_greatest_element r).
Proof. ir. uf the_greatest_element. app choose_pr.
Qed.
Lemma the_least_element_pr2: forall r x, order r ->
least_element r x -> the_least_element r = x.
Proof. ir. assert (exists u, least_element r u). exists x. am.
cp (the_least_element_pr H H1). ap (unique_least H H2 H0).
Qed.
Lemma the_greatest_element_pr2: forall r x, order r ->
greatest_element r x -> the_greatest_element r = x.
Proof. ir. assert (exists u, greatest_element r u). exists x. am.
cp (the_greatest_element_pr H H1). ap (unique_greatest H H2 H0).
Qed.
Lemma greatest_induced: forall r s x, order r ->
sub s (substrate r) -> inc x s ->
greatest_element r x ->
the_greatest_element r = the_greatest_element (induced_order r s).
Proof. ir. rw (the_greatest_element_pr2 H H2). sy. app the_greatest_element_pr2.
fprops. red. aw. split. am. ir. nin H2. aw. app H4. app H0.
Qed.
Lemma least_induced: forall r s x, order r ->
sub s (substrate r) -> inc x s ->
least_element r x ->
the_least_element r = the_least_element (induced_order r s).
Proof. ir. rw (the_least_element_pr2 H H2). sy. app the_least_element_pr2.
fprops. red. aw. split. am. ir. nin H2. aw. app H4. app H0.
Qed.
Lemma least_not_greatest: forall r x , order r ->
least_element r x -> greatest_element r x ->
is_singleton (substrate r).
Proof. ir. red. exists x. nin H0. nin H1. rw singleton_pr. split. am.
ir. cp (H2 _ H4). cp (H3 _ H4). order_tac.
Qed.
Lemma greatest_reverse: forall a r,
order r -> greatest_element r a -> least_element (opposite_order r) a.
Proof. ir. red. aw. nin H0. split. am. ir. aw. app H1.
Qed.
Lemma least_reverse: forall a r,
order r -> least_element r a -> greatest_element (opposite_order r) a.
Proof. ir. red. aw. nin H0. split. am. ir. aw. app H1.
Qed.
Lemma the_least_reverse: forall r, order r ->
(exists a, greatest_element r a) ->
the_least_element (opposite_order r) = the_greatest_element r.
Proof. ir. cp (the_greatest_element_pr H H0).
cp (greatest_reverse H H1). app the_least_element_pr2. fprops.
Qed.
Lemma greatest_maximal: forall a r,
order r -> greatest_element r a -> maximal_element r a.
Proof. ir. nin H0. red. split. am. ir.
assert (inc x (substrate r)). order_tac. set (H1 _ H3). order_tac.
Qed.
Lemma least_minimal: forall a r,
order r -> least_element r a -> minimal_element r a.
Proof. ir. nin H0. red. split. am. ir.
assert (inc x (substrate r)). order_tac. set (H1 _ H3). order_tac.
Qed.
Lemma greatest_unique_maximal: forall a b r,
greatest_element r a -> maximal_element r b -> a = b.
Proof. uf greatest_element; uf maximal_element. ir. ee. app H1. app H2.
Qed.
Lemma least_unique_minimal: forall a b r,
least_element r a -> minimal_element r b -> a = b.
Proof. uf least_element; uf minimal_element. ir. ee. app H1. app H2.
Qed.
Lemma least_is_intersection: forall s a,
least_element (inclusion_suborder s) a ->
nonempty s -> a = intersection s.
Proof. ir. red in H. awi H. nin H.
set_extens. app intersection_inc. ir. cp (H1 _ H3).
awi H4. ee. app H6. apply intersection_forall with s. am. am.
Qed.
Lemma greatest_is_union: forall s a,
greatest_element (inclusion_suborder s) a -> a = union s.
Proof. ir. red in H. awi H. nin H.
set_extens. union_tac.
nin (union_exists H1). ee. cp (H0 _ H3). awi H4. ee. app H6.
Qed.
Lemma intersection_is_least: forall s,
inc (intersection s) s ->
least_element (inclusion_suborder s) (intersection s) .
Proof. ir. red. aw. split. am. ir. aw. eee. app intersection_sub.
Qed.
Lemma union_is_greatest: forall s,
inc (union s) s -> greatest_element (inclusion_suborder s) (union s).
Proof. ir. red. aw. split. am. ir. aw. eee. app union_sub.
Qed.
Lemma emptyset_is_least: forall E,
least_element (inclusion_order E) emptyset.
Proof. ir. red. aw. split.
ap emptyset_sub_any. ir. aw. split. ap emptyset_sub_any.
split. app powerset_sub. ap emptyset_sub_any.
Qed.
Lemma wholeset_is_greatest: forall E,
greatest_element (inclusion_order E) E.
Proof. ir. red. aw. split. fprops.
ir. aw. split. app powerset_sub. split. fprops. app powerset_sub.
Qed.
Definition empty_function_tg F := BL (fun x => x) emptyset F.
Lemma empty_function_tg_function: forall F,
is_function (empty_function_tg F).
Proof. ir. uf empty_function_tg. app bl_function. red. ir.
elim (emptyset_pr H).
Qed.
Lemma least_prolongation: forall E F,
least_element (opposite_order (extension_order E F))
(empty_function_tg F).
Proof. red. ir. assert (set_of_sub_functions E F =
substrate (opposite_order (extension_order E F))). aw. fprops. wr H.
assert (inc (empty_function_tg F) (set_of_sub_functions E F)). bw.
uf empty_function_tg. aw. eee. app empty_function_tg_function.
ap emptyset_sub_any.
ee. am. ir. rw opposite_gle. rw extension_order_pr1. eee.
uf empty_function_tg. uf BL. aw. red. ir. ufi L H2. awi H2. nin H2. nin H2.
elim (emptyset_pr H2). fprops.
Qed.
Lemma greatest_prolongation: forall E F x,
greatest_element (opposite_order (extension_order E F)) x ->
nonempty E -> small_set F.
Proof. ir. nin (emptyset_dichot F). rw H1. red. ir. elim (emptyset_pr H2).
set (r:= opposite_order (extension_order E F)).
assert (order (extension_order E F)). fprops.
assert (order r). uf r. fprops.
assert (forall u (Ha:inc u F), x = constant_function E F u Ha).
ir. set (f:=constant_function E F u Ha).
assert (source f = E). uf f. uf constant_function. aw.
assert (inc f (set_of_sub_functions E F)). bw. eee. uf f.
app constant_function_fun. uf f. uf constant_function. aw.
wri (maximal_prolongation H1 H5) H4. ap (greatest_unique_maximal H H4).
red. ir. cp (H4 _ H5). rwi (H4 _ H6) H7.
nin H0. cp (f_equal (fun f=> W y f) H7). simpl in H8.
do 2 rwi constant_W H8. sy; am. am. am. am.
Qed.
Lemma least_equivalence: forall r,
is_reflexive r -> sub (identity_g (substrate r)) r.
Proof. ir. red. ir. rwi inc_diagonal_rw H0. nin H0. nin H1. red in H. ee.
cp (H3 _ H1). red in H4. assert (J (P x) (Q x) = x). app pair_recov.
wri H2 H5. wrr H5.
Qed.
Lemma order_transportation: forall f r,
let r':= image_by_fun (ext_to_prod f f) r in
bijective f -> order r -> substrate r = source f ->
(order r' & substrate r' = target f).
Proof. ir. set (E:= source f).
assert (is_function f). app bij_is_function.
assert (is_function (ext_to_prod f f)). app ext_to_prod_function.
assert (forall z,inc z r' = (exists x, exists y, inc x E & inc y E &
inc (J x y) r & z = J(W x f)(W y f))).
ir. uf r'. app iff_eq. ir. ufi image_by_fun H4. awi H4. nin H4. nin H4.
cp (W_pr H3 H5). assert (J (P x) (Q x) = x). aw. assert (is_graph r).
fprops. app H7. wri H7 H6.
assert (inc (P x) (substrate r)). substr_tac. rwi H1 H8.
assert (inc (Q x) (substrate r)). substr_tac. rwi H1 H9.
rwii ext_to_prod_W H6. exists (P x). exists (Q x). split. am.
split. am. split. rww H7. sy. am.
ir. nin H4. nin H4. ee. uf image_by_fun. aw. ex_tac.
assert (inc x (source f)). wr H1. substr_tac.
assert (inc x0 (source f)). wr H1. substr_tac.
assert (inc (J x x0) (source (ext_to_prod f f))). uf ext_to_prod. aw. eee.
assert (z = W (J x x0) (ext_to_prod f f)). rww ext_to_prod_W.
rw H11. graph_tac.
assert(is_graph r'). red. ir. rwi H4 H5. nin H5; nin H5; ee. rw H8. fprops.
assert(substrate r' = target f). set_extens. ufi substrate H6.
nin (union2_or H6); awii H7; nin H7; rwi H4 H7; nin H7; nin H7; ee.
rw (pr1_def H10). app inc_W_target.
rw (pr2_def H10). app inc_W_target.
red in H. ee. cp (surjective_pr2 H7 H6). nin H8. nin H8.
assert (inc (J x x) r'). rw H4. exists x0. exists x0. split. am. split. am.
split. wri H1 H8. change (gle r x0 x0). order_tac. rww H9. substr_tac.
split. red. ee; split; tv.
ir. rwi H6 H7. red in H. ee.
cp (surjective_pr2 H8 H7). nin H9. nin H9. red. rw H4. exists x. exists x.
split. am. split. am. split. change (gle r x x). order_tac. ue. ue.
ir. red. red in H7; red in H8.
rwi H4 H7; rwi H4 H8. nin H7;nin H7; nin H8; nin H8; ee. rw H4.
exists x0. exists x3. eee. assert (x1 = x2).
cp (pr1_def H11). rwi (pr2_def H14) H15. nin H. nin H. app H17.
rwi H15 H13. app (order_transitivity H0 H13 H10).
rw (pr2_def H11). inter2tac.
ir. red in H7; red in H8.
rwi H4 H7; rwi H4 H8. nin H7;nin H7; nin H8; nin H8; ee.
cp (pr1_def H14). cp (pr2_def H14). cp (pr1_def H11).
cp (pr2_def H11). nin H. nin H. assert (x0 = x3). app H20. ue.
assert (x1 = x2). app H20. ue. rwi H21 H13; rwi H22 H13. rw H17; rw H18.
rw (order_antisymmetry H0 H13 H10). tv. am.
Qed.
Any ordered set can be extended by adjoining a greatest element
Definition order_with_greatest r a :=
union2 r (product (tack_on (substrate r) a) (singleton a)).
Lemma order_with_greatest_pr: forall r a,
let r':=order_with_greatest r a in
order r -> ~ (inc a (substrate r)) ->
(order r' & substrate r' = tack_on (substrate r) a &
r = intersection2 r' (coarse (substrate r)) & greatest_element r' a).
Proof. ir. set (E:=substrate r). ufi order_with_greatest r'. fold E in r'.
assert (Ha:sub r (coarse E)). uf E. app sub_graph_coarse_substrate. fprops.
assert (is_graph r'). uf r'. app union2_is_graph. fprops. red. ir.
awi H1. eee.
assert (substrate r'=tack_on E a).
set_extens. ufi substrate H2. aw. nin (union2_or H2); awii H3; nin H3;
ufi r' H3; nin (union2_or H3);
try (cp (Ha _ H4); ufi coarse H5; awi H5; eee); awi H4; ee; au.
assert (inc (J x x) r'). rwi tack_on_inc H2. uf r'. nin H2.
app union2_first. order_tac.
app union2_second. rw H2. aw. eee. substr_tac.
assert (order r'). red; ee; split;tv. rw H2. uf r'. ir.
nin (tack_on_or H3). red. app union2_first. order_tac.
rw H4. red. ir. app union2_second. aw. eee.
uf r'. ir. red in H3; red in H4. red.
nin (union2_or H3). nin (union2_or H4). ap union2_first.
order_tac.
awi H6. ee. rw H8. ap union2_second. cp (Ha _ H5).
ufi coarse H9. awi H9. ee. aw. eee. awi H5. ee.
nin (union2_or H4). elim H0. wr H7. substr_tac.
awi H8. ee. app union2_second. aw. fprops.
uf r'. ir. red in H3; red in H4.
nin (union2_or H3). nin (union2_or H4). apply (order_antisymmetry H H5 H6).
awi H6. ee. elim H0. wr H8. substr_tac.
awi H5. ee. nin (union2_or H4). elim H0. wr H7. substr_tac.
awi H8. eee. eee.
uf r'. set_extens. app intersection2_inc. inter2tac. app Ha.
nin (intersection2_both H4). ufi coarse H6. awi H6. nin (union2_or H5).
am. awi H7. ee. rwi H9 H11. elim H0. am.
red. split. rw H2. rw tack_on_inc. right. tv. rw H2. ir.
red. red. uf r'. app union2_second. app product_pair_inc. fprops.
Qed.
Theorem adjoin_greatest: forall r a E,
order r -> substrate r = E -> ~ (inc a E) ->
exists_unique (fun r' => order r' & substrate r' = tack_on E a &
r = intersection2 r' (coarse E) & greatest_element r' a).
Proof. ir. set(E':=tack_on E a).
set(r':= union2 r (product E' (singleton a))). red. split.
exists (order_with_greatest r a). wri H0 H1.
cp (order_with_greatest_pr H H1). uf E'. wr H0. am.
ir. ee.
set_extens. assert (is_pair x0). assert (is_graph x). fprops. app H11.
assert(inc (P x0) E'). wr H7. substr_tac.
assert(inc (Q x0) E'). wr H7. substr_tac.
ufi E' H12. ufi E' H13. nin (union2_or H12). nin (union2_or H13).
assert (inc x0 r). rw H8. app intersection2_inc. uf coarse.
app product_inc. rwi H5 H16. inter2tac.
red in H6. nin H6. assert (J (P x0) (Q x0) = x0). aw. wr H17.
rw (singleton_eq H15). app H16. rwi tack_on_inc H12. nin H12.
assert (inc (J (P x0) (P x0)) r). order_tac. ue. ue.
rwi H5 H18. cp (intersection2_first H18). wr H4. substr_tac.
rw H12. am. red in H9; ee.
assert (inc (Q x0) (substrate x)). substr_tac.
cp (H15 _ H16). red in H17.
assert (J (P x0) (Q x0) = x0). aw. wri H18 H10. wr H18. red in H17.
rwi (singleton_eq H14) H10. wr (order_antisymmetry H2 H10 H17).
rw (singleton_eq H14). red in H6. ee. order_tac.
assert (is_pair x0). assert (is_graph y). fprops. app H11.
assert(inc (P x0) E'). wr H4. substr_tac.
assert(inc (Q x0) E'). wr H4. substr_tac.
ufi E' H12. ufi E' H13. nin (union2_or H12). nin (union2_or H13).
assert (inc x0 r). rw H5. app intersection2_inc. uf coarse.
app product_inc. rwi H8 H16. inter2tac.
red in H9. nin H9. assert (J (P x0) (Q x0) = x0). app pair_recov. wr H17.
rw (singleton_eq H15). app H16. rwi tack_on_inc H12. nin H12.
assert (inc (J (P x0) (P x0)) r). order_tac. ue.
rwi H8 H18. cp (intersection2_first H18). substr_tac. rw H12. am.
assert (inc (Q x0) (substrate y)). substr_tac.
assert (J (P x0) (Q x0) = x0). aw. awi H14. red in H6. ee.
cp (H17 _ H15). red in H18. wri H16 H10. rwi H14 H10.
wr H16. wr (order_antisymmetry H3 H10 H18). rw H14. order_tac.
red in H9. ee. am.
Qed.
A set A is cofinal if every element of E is bounded by an element of A
Definition cofinal_set r a :=
sub a (substrate r) &
(forall x, inc x (substrate r) -> exists y, inc y a & gle r x y).
Definition coinitial_set r a :=
sub a (substrate r) &
(forall x, inc x (substrate r) -> exists y, inc y a & gle r y x).
Lemma exists_greatest_cofinal: forall r,
(exists x, greatest_element r x) =
(exists a, cofinal_set r a & is_singleton a).
Proof. ir. app iff_eq. ir. nin H. exists (singleton x). split. red.
red in H. ee. red. ir. db_tac. ir. ex_tac.
exists x. tv. ir. nin H. nin H. nin H0. red in H. ee.
exists x0. red. split. app H. rw H0. fprops. ir. cp (H1 _ H2). nin H3.
nin H3. rwi H0 H3. rwi (singleton_eq H3) H4. am.
Qed.
Lemma exists_least_coinitial: forall r,
(exists x, least_element r x) =
(exists a, coinitial_set r a & is_singleton a).
Proof. ir. app iff_eq. ir. nin H. exists (singleton x). split. red.
red in H. ee. red. ir. rww (singleton_eq H1). ir. ex_tac.
exists x. tv. ir. nin H. nin H. nin H0. red in H. ee.
exists x0. red. split. app H. rw H0. fprops. ir. cp (H1 _ H2). nin H3.
nin H3. rwi H0 H3. rwi (singleton_eq H3) H4. am.
Qed.
Definition upper_bound r X x :=
inc x (substrate r) & forall y, inc y X -> gle r y x.
Definition lower_bound r X x :=
inc x (substrate r) & forall y, inc y X -> gle r x y.
Lemma opposite_upper_bound: forall x X r, order r ->
upper_bound r X x = lower_bound (opposite_order r) X x.
Proof. ir. uf upper_bound. uf lower_bound. aw.
app iff_eq. ir. ee. am. ir. aw. app H1.
ir. ee. am. ir. cp (H1 _ H2). awi H3. am. am.
Qed.
Lemma opposite_lower_bound: forall x X r, order r ->
lower_bound r X x = upper_bound (opposite_order r) X x.
Proof. ir. uf upper_bound. uf lower_bound. aw.
app iff_eq. ir. ee. am. ir. aw. app H1.
ir. ee. am. ir. cp (H1 _ H2). awi H3. am. am.
Qed.
Lemma smaller_lower_bound: forall x y X r, preorder r ->
lower_bound r X x -> gle r y x -> lower_bound r X y.
Proof. uf lower_bound. ir. ee. red in H1. substr_tac. ir.
cp (H2 _ H3). red in H. ee. red in H5. ee. app (H6 _ _ _ H1 H4).
Qed.
Lemma greater_upper_bound: forall x y X r, preorder r ->
upper_bound r X x -> gle r x y -> upper_bound r X y.
Proof. uf upper_bound. ir. ee. red in H1. substr_tac. ir.
red in H. ee. red in H4. ee. app (H5 _ _ _ (H2 _ H3) H1).
Qed.
Lemma sub_lower_bound: forall x X Y r,
lower_bound r X x -> sub Y X-> lower_bound r Y x.
Proof. uf lower_bound. ir. ee. am. ir. app H1. app H0.
Qed.
Lemma sub_upper_bound: forall x X Y r,
upper_bound r X x -> sub Y X -> upper_bound r Y x.
Proof. uf upper_bound. ir. ee. am. ir. app H1. app H0.
Qed.
Lemma least_element_pr: forall X r, order r -> sub X (substrate r) ->
(exists a, least_element (induced_order r X) a) =
(exists x, lower_bound r X x & inc x X).
Proof. uf lower_bound. uf least_element. ir. aw.
app iff_eq. ir. nin H1. nin H1. exists x. split. split. app H0. ir.
cp (H2 _ H3). awii H4. am.
ir. nin H1. ee. ex_tac. ir. aw. app H3.
Qed.
Lemma greatest_element_pr: forall X r, order r -> sub X (substrate r) ->
(exists a, greatest_element (induced_order r X) a) =
(exists x, upper_bound r X x & inc x X).
Proof. uf upper_bound. uf greatest_element. ir. aw.
app iff_eq. ir. nin H1. nin H1. exists x. split. split. app H0. ir.
cp (H2 _ H3). awii H4. am.
ir. nin H1. ee. ex_tac. ir. aw. app H3.
Qed.
A set can be bounded above, below, or both
Definition bounded_above r X := exists x, upper_bound r X x.
Definition bounded_below r X := exists x, lower_bound r X x.
Definition bounded_both r X := bounded_above r X & bounded_below r X.
Lemma bounded_above_sub: forall X Y r,
sub Y X -> bounded_above r X -> bounded_above r Y.
Proof. ir. red in H0. nin H0. red. exists x. app (sub_upper_bound H0 H).
Qed.
Lemma bounded_below_sub: forall X Y r,
sub Y X -> bounded_below r X -> bounded_below r Y.
Proof. ir. red in H0. nin H0. red. exists x. app (sub_lower_bound H0 H).
Qed.
Lemma bounded_both_sub: forall X Y r,
sub Y X ->bounded_both r X -> bounded_both r Y.
Proof. uf bounded_both. ir. ee.
app (bounded_above_sub H H0). app (bounded_below_sub H H1).
Qed.
Lemma singleton_bounded:forall x r,
is_singleton x -> order r -> sub x (substrate r) -> bounded_both r x.
Proof. red. ir. nin H. assert (inc x0 (substrate r)). rwi H H1. app H1.
fprops. assert (gle r x0 x0). order_tac.
split; red; ir; exists x0; split;tv; ir;rwi H H4; db_tac.
Qed.
Definition greatest_lower_bound r X x :=
greatest_element (induced_order r (Zo (substrate r)
(fun z => lower_bound r X z))) x.
Definition least_upper_bound r X x :=
least_element (induced_order r (Zo (substrate r)
(fun z => upper_bound r X z))) x.
Lemma greatest_lower_bound_pr: forall r X x,
order r -> sub X (substrate r) ->
greatest_lower_bound r X x = (lower_bound r X x
& forall z, lower_bound r X z -> gle r z x).
Proof. ir. uf greatest_lower_bound. uf greatest_element.
set (T:= (Zo (substrate r) (fun z => lower_bound r X z))). aw.
app iff_eq. ir. ee. ufi T H1. Ztac. am.
ir. assert (inc z T). uf T. Ztac. red in H3. ee. am. cp (H2 _ H4).
red in H5. awi H5. am. am. am.
ir. assert (inc x T). ee. uf T. Ztac. red in H1. ee. am. split. am.
ir. aw. ee. app H4. ufi T H3. Ztac. am. uf T. app Z_sub.
Qed.
Lemma least_upper_bound_pr: forall r X x,
order r -> sub X (substrate r) ->
least_upper_bound r X x = (upper_bound r X x
& forall z, upper_bound r X z -> gle r x z).
Proof. ir. uf least_upper_bound. uf least_element. aw.
set (T:= (Zo (substrate r) (fun z => upper_bound r X z))).
app iff_eq. ir. ee. ufi T H1. Ztac. am.
ir. assert (inc z T). uf T. Ztac. red in H3. ee. am. cp (H2 _ H4).
red in H5. awi H5. am. am. am.
ir. assert (inc x T). ee. uf T. Ztac. red in H1. ee. am. split. am.
ir. aw. ee. app H4. ufi T H3. Ztac. am. app Z_sub.
Qed.
Hint Rewrite greatest_lower_bound_pr least_upper_bound_pr: aw.
Lemma supremum_unique: forall x y X r, order r ->
least_upper_bound r X x -> least_upper_bound r X y -> x = y.
Proof. ir. ufi least_upper_bound H0. ufi least_upper_bound H1.
assert (order (induced_order r
(Zo (substrate r) (fun z => upper_bound r X z)))).
app order_induced_order. app Z_sub.
ap (unique_least H2 H0 H1).
Qed.
Lemma infimum_unique: forall x y X r, order r ->
greatest_lower_bound r X x -> greatest_lower_bound r X y -> x = y.
Proof. ir. ufi greatest_lower_bound H0. ufi greatest_lower_bound H1.
assert (order (induced_order r
(Zo (substrate r) (fun z => lower_bound r X z)))).
app order_induced_order. app Z_sub.
ap (unique_greatest H2 H0 H1).
Qed.
Definition of the supremum or infimum or a set or a pair
Definition supremum r X := choose (fun x=> least_upper_bound r X x).
Definition infimum r X := choose (fun x=> greatest_lower_bound r X x).
Definition sup r x y := supremum r (doubleton x y).
Definition inf r x y := infimum r (doubleton x y).
Definition has_supremum r X :=(exists x, least_upper_bound r X x).
Definition has_infimum r X :=(exists x, greatest_lower_bound r X x).
Lemma supremum_pr1: forall X r,
order r -> sub X (substrate r) -> has_supremum r X ->
least_upper_bound r X (supremum r X).
Proof. ir. uf supremum. app choose_pr.
Qed.
Lemma infimum_pr1: forall X r,
order r -> sub X (substrate r) -> has_infimum r X ->
greatest_lower_bound r X (infimum r X).
Proof. ir. uf infimum. app choose_pr.
Qed.
Hint Resolve supremum_pr1 infimum_pr1: fprops.
Lemma supremum_pr2: forall r X a, order r -> sub X (substrate r) ->
least_upper_bound r X a -> a = supremum r X.
Proof. ir. assert (has_supremum r X). exists a. am.
cp (supremum_pr1 H H0 H2). ap (supremum_unique H H1 H3).
Qed.
Lemma infimum_pr2: forall r X a, order r -> sub X (substrate r) ->
greatest_lower_bound r X a -> a = infimum r X.
Proof. ir. assert (has_infimum r X). exists a. am.
cp (infimum_pr1 H H0 H2). ap (infimum_unique H H1 H3).
Qed.
Lemma inc_supremum_substrate : forall X r,
order r -> sub X (substrate r) -> has_supremum r X ->
inc (supremum r X) (substrate r).
Proof. ir. cp (supremum_pr1 H H0 H1). awi H2. nin H2. nin H2. am. am. am.
Qed.
Lemma inc_infimum_substrate : forall X r,
order r -> sub X (substrate r) -> has_infimum r X ->
inc (infimum r X) (substrate r).
Proof. ir. cp (infimum_pr1 H H0 H1). awi H2. nin H2. nin H2. am. am. am.
Qed.
Lemma supremum_pr: forall X r,
order r -> sub X (substrate r) -> has_supremum r X ->
(upper_bound r X (supremum r X) &
forall z, upper_bound r X z -> gle r (supremum r X) z).
Proof. ir. cp (supremum_pr1 H H0 H1). awi H2. am. am. am.
Qed.
Lemma infimum_pr: forall X r,
order r -> sub X (substrate r) -> has_infimum r X ->
(lower_bound r X (infimum r X) &
forall z, lower_bound r X z -> gle r z (infimum r X)).
Proof. ir. cp (infimum_pr1 H H0 H1). awi H2. am. am. am.
Qed.
Properties of sup and inf of pairs
Lemma sup_pr: forall a b r,
order r -> inc a (substrate r) -> inc b (substrate r)
-> has_supremum r (doubleton a b) ->
(gle r a (sup r a b) & gle r b (sup r a b) &
forall z, gle r a z -> gle r b z -> gle r (sup r a b) z).
Proof. ir. assert (sub (doubleton a b) (substrate r)). app sub_doubleton.
cp (supremum_pr H H3 H2). nin H4. red in H4. nin H4.
split. assert (inc a (doubleton a b)). fprops. app H6.
split. assert (inc b (doubleton a b)). fprops. app H6.
ir. app H5. red. split. ap (inc_arg2_substrate H7).
ir. nin (doubleton_or H9); ue.
Qed.
Lemma inf_pr: forall a b r,
order r -> inc a (substrate r) -> inc b (substrate r)
-> has_infimum r (doubleton a b) ->
(gle r (inf r a b) a & gle r (inf r a b) b&
forall z, gle r z a -> gle r z b -> gle r z (inf r a b)).
Proof. ir. assert (sub (doubleton a b) (substrate r)). app sub_doubleton.
cp (infimum_pr H H3 H2). nin H4. red in H4. nin H4.
split. assert (inc a (doubleton a b)). fprops. app H6.
split. assert (inc b (doubleton a b)). fprops. app H6.
ir. app H5. red. split. ap (inc_arg1_substrate H7).
ir. nin (doubleton_or H9); ue.
Qed.
Lemma least_upper_bound_doubleton: forall r x y z,
order r -> gle r x z -> gle r y z ->
(forall t, gle r x t -> gle r y t -> gle r z t) ->
least_upper_bound r (doubleton x y) z.
Proof. ir. cp (inc_arg1_substrate H0). cp (inc_arg1_substrate H1). aw.
ee. red. ee. order_tac. ir. nin (doubleton_or H5); rww H6.
ir. nin H5. app H2; ap H6; fprops.
red. ir. nin (doubleton_or H5); ue.
Qed.
Lemma greatest_lower_bound_doubleton: forall r x y z,
order r -> gle r z x -> gle r z y ->
(forall t, gle r t x -> gle r t y -> gle r t z) ->
greatest_lower_bound r (doubleton x y) z.
Proof. ir. cp (inc_arg2_substrate H0). cp (inc_arg2_substrate H1). aw.
ee. red. ee. order_tac. ir. nin (doubleton_or H5);ue.
ir. nin H5. app H2; ap H6; fprops.
red. ir. nin (doubleton_or H5); ue.
Qed.
Link between supremum and greatest element
Lemma greatest_is_sup: forall r X a,
order r -> sub X (substrate r) ->
greatest_element (induced_order r X) a -> least_upper_bound r X a.
Proof. ir. red in H1. awi H1. nin H1. aw. split. red. split. app H0. ir.
cp (H2 _ H3). red in H4. awi H4. am. am. am. red. ir.
red in H3. nin H3. app (H4 _ H1). am. am.
Qed.
Lemma least_is_inf: forall r X a,
order r -> sub X (substrate r) ->
least_element (induced_order r X) a -> greatest_lower_bound r X a.
Proof. ir. red in H1. awi H1. nin H1. aw. split. red. split. app H0. ir.
cp (H2 _ H3). red in H4. awi H4. am. am. am. red. ir.
red in H3. nin H3. app (H4 _ H1). am. am.
Qed.
Lemma inf_sup_opp: forall r X a,
order r -> sub X (substrate r) ->
greatest_lower_bound r X a = least_upper_bound (opposite_order r) X a.
Proof. ir. aw. app iff_eq. ir. split. ee. rwi opposite_lower_bound H1. am. am.
ir. aw. wri opposite_lower_bound H2. nin H1. app H3. am.
ir. nin H1. split. rw opposite_lower_bound. am. am. ir. cp (H2 z).
wri opposite_lower_bound H4. cp (H4 H3). awi H5. am. am. am. fprops.
Qed.
Lemma sup_inf_opp: forall r X a,
order r -> sub X (substrate r) ->
least_upper_bound r X a = greatest_lower_bound (opposite_order r) X a.
Proof. ir. rw inf_sup_opp.
assert (opposite_order (opposite_order r) = r). uf opposite_order.
app inverse_graph_involutive. fprops. rww H1. fprops. aw.
Qed.
Supremum and infimum of the empty set
Lemma set_of_lower_bounds_emptyset: forall r ,
Zo (substrate r) (fun z => lower_bound r emptyset z) = substrate r.
Proof. ir. ap extensionality. ap Z_sub. red. ir. Ztac. red. split. am. ir.
elim (emptyset_pr H0).
Qed.
Lemma set_of_upper_bounds_emptyset: forall r ,
Zo (substrate r) (fun z => upper_bound r emptyset z) = substrate r.
Proof. ir. ap extensionality. ap Z_sub. red. ir. Ztac. red. split. am. ir.
elim (emptyset_pr H0).
Qed.
Lemma least_upper_bound_emptyset: forall r x, order r ->
least_upper_bound r emptyset x = least_element r x.
Proof. ir. uf least_upper_bound. rw set_of_upper_bounds_emptyset.
rww induced_order_substrate.
Qed.
Lemma greatest_lower_bound_emptyset: forall r x, order r ->
greatest_lower_bound r emptyset x = greatest_element r x.
Proof. ir. uf greatest_lower_bound. rw set_of_lower_bounds_emptyset.
rww induced_order_substrate.
Qed.
Supremum and infimum for inclusion order
Lemma intersection_is_inf: forall s E, sub s (powerset E) ->
greatest_lower_bound (inclusion_order E) s
(Yo (nonempty s) (intersection s) E).
Proof. ir. assert (order (inclusion_order E)). fprops.
nin (emptyset_dichot s). rw Y_if_not_rw. rw H1.
rw greatest_lower_bound_emptyset. app wholeset_is_greatest. am.
red. ir. nin H2. rwi H1 H2. elim (emptyset_pr H2).
assert (sub (intersection s) E). nin H1. apw sub_trans y.
app intersection_sub. set (H _ H1). awi i. am.
rww Y_if_rw. aw. split. red. aw. split. am. ir. aw.
set (intersection_sub H3). set (H _ H3). awi i. eee.
ir. red in H3. ee. aw. awi H3. eee. red. ir. app intersection_inc.
ir. cp (H4 _ H6). awi H7. ee. app H9.
Qed.
Lemma union_is_sup: forall s E, sub s (powerset E) ->
least_upper_bound (inclusion_order E) s (union s).
Proof. ir. assert (order (inclusion_order E)). app inclusion_is_order.
assert (sub (union s) E). app sub_union. ir. set (H _ H1). awi i. am.
aw. uf upper_bound. split. split. aw. ir. aw.
assert (sub y (union s)). app union_sub. eee. set (H _ H2). awi i. am.
ir. ee. awi H2. aw. eee. red. ir. nin (union_exists H4). nin H5.
set (H3 _ H6). awi g. ee. app H9.
Qed.
Lemma union_is_sup1: forall s F E, sub F (powerset E) ->
sub s F -> inc (union s) F ->
least_upper_bound (inclusion_suborder F) s (union s).
Proof. ir. rw least_upper_bound_pr. split. red. aw. ee. am. ir. aw. ee.
app H0. am. app union_sub. ir. nin H2. awi H2. aw. eee. red. ir.
nin (union_exists H4). nin H5. cp (H3 _ H6). awi H7. ee. app H9.
ap subinclusion_is_order. rw substrate_subinclusion_order. am.
Qed.
Lemma intersection_is_inf1: forall s F E, sub F (powerset E) ->
sub s F -> inc (Yo (nonempty s) (intersection s) E) F ->
greatest_lower_bound (inclusion_suborder F) s
(Yo (nonempty s) (intersection s) E).
Proof. ir. rw greatest_lower_bound_pr. split. red. aw. split. am.
ir. aw. ee. am. app H0. rw Y_if_rw. app intersection_sub. exists y. am.
ir. red in H2. awi H2. ee. aw. eee.
nin (emptyset_dichot s). rw Y_if_not_rw. app powerset_sub. app H.
rw H4. red. ir. nin H5. elim (emptyset_pr H5). rw Y_if_rw.
red. ir. app intersection_inc. ir. cp (H3 _ H6). awi H7. ee. app H9. am.
ap subinclusion_is_order. rw substrate_subinclusion_order. am.
Qed.
Supremum for extension order: is least common extension
Lemma sup_extension_order1: forall E F T f,
sub T (set_of_sub_functions E F) ->
least_upper_bound (opposite_order (extension_order E F)) T f ->
forall u v x, inc u T -> inc v T -> inc x (source u) -> inc x (source v) ->
W x u = W x v.
Proof. ir. assert (order (opposite_order (extension_order E F))). fprops.
assert (sub T (substrate (opposite_order (extension_order E F)))). aw. fprops.
awi H0. nin H0. nin H0.
cp (H8 _ H1). cp (H8 _ H2). rw (extension_order_pr H9 H3).
rw (extension_order_pr H10 H4). tv. fprops. am.
Qed.
Lemma sup_extension_order2: forall E F T,
sub T (set_of_sub_functions E F) ->
(forall u v x, inc u T -> inc v T -> inc x (source u) -> inc x (source v) ->
W x u = W x v) ->
exists x, least_upper_bound (opposite_order (extension_order E F)) T x &
(source x = unionf T source) &
(range (graph x) = unionf T (fun u => (range (graph u))))&
(graph x) = unionf T graph.
Proof. ir. assert (forall i, inc i T -> function_prop i (source i) F). ir.
cp (H _ H1). bwi H2. red. eee.
assert (forall i j, inc i T -> inc j T ->
agrees_on (intersection2 (source i) (source j)) i j). ir. red. ee.
app intersection2sub_first. app intersection2sub_second. ir. app H0.
inter2tac. inter2tac.
nin (extension_covering1 _ _ H1 H2). ee. red in H3; ee.
assert (order (extension_order E F)). fprops.
assert (order (opposite_order (extension_order E F))). fprops.
assert (set_of_sub_functions E F =
substrate (opposite_order (extension_order E F))). aw.
assert (sub T (substrate (opposite_order (extension_order E F)))). aw.
assert (inc x (set_of_sub_functions E F)). bw. ee. am. rw H7. red. ir.
cp (unionf_exists H13). nin H14. nin H14. cp (H _ H14). bwi H16. ee.
app H17. am.
exists x. ee. aw. split. red. wr H11. ee. am. ir. cp (H1 _ H14); ee.
rw extension_order_pr2. eee. red. ir. union_tac.
ir. red in H14. nin H14. wri H11 H14. rw extension_order_pr2. eee.
red. ir. nin (unionf_exists H16). nin H17. set (H15 _ H17).
rwi extension_order_pr2 g. eee. aw. am. am. am.
Qed.
Supremum and infinum of the range of a function
Definition is_sup_fun r f x := least_upper_bound r (image_of_fun f) x.
Definition is_inf_fun r f x := greatest_lower_bound r (image_of_fun f) x.
Lemma is_sup_fun_pr: forall r f x, order r -> substrate r = target f ->
is_function f ->
is_sup_fun r f x = (inc x (target f)
& (forall a, inc a (source f) -> gle r (W a f) x)
& forall z, inc z (target f) -> (forall a, inc a (source f)
-> gle r (W a f) z) -> gle r x z).
Proof. ir. uf is_sup_fun. aw. uf upper_bound. rw H0.
uf image_of_fun. assert (is_graph (graph f)). fprops.
ap iff_eq; ir; ee. am. ir. ap H5. aw. ex_tac. graph_tac.
ir. ap H4. split. am. ir. awi H8. nin H8. nin H8.
red in H9. wr (W_pr H1 H9). app H7. am.
ir. awi H6. nin H6. nin H6. wr (W_pr H1 H7). app H4.
ir. nin H6. ap H5. am. ir. ap H7. aw. ex_tac. graph_tac.
rw H0. app sub_image_target.
Qed.
Lemma is_inf_fun_pr: forall r f x, order r -> substrate r = target f ->
is_function f ->
is_inf_fun r f x = (inc x (target f)
& (forall a, inc a (source f) -> gle r x (W a f))
& forall z, inc z (target f) -> (forall a, inc a (source f)
-> gle r z (W a f)) -> gle r z x).
Proof. ir. uf is_inf_fun. aw. uf lower_bound. rw H0.
uf image_of_fun. assert (is_graph (graph f)). fprops.
ap iff_eq; ir; ee. am. ir. ap H5. aw. ex_tac. graph_tac.
ir. ap H4. split. am. ir. awi H8. nin H8. nin H8.
red in H9. wr (W_pr H1 H9). app H7. am.
ir. awi H6. nin H6. nin H6. wr (W_pr H1 H7). app H4.
ir. nin H6. ap H5. am. ir. ap H7. aw. ex_tac. graph_tac.
rw H0. app sub_image_target.
Qed.
Supremum and infinum of the range of a functional graph
Definition is_sup_graph r f x := least_upper_bound r (range f) x.
Definition is_inf_graph r f x := greatest_lower_bound r (range f) x.
Definition has_sup_graph r f := has_supremum r (range f).
Definition has_inf_graph r f := has_infimum r (range f).
Definition sup_graph r f:= supremum r (range f).
Definition inf_graph r f := infimum r (range f).
Lemma is_sup_graph_pr1: forall r f,
order r -> sub (range f) (substrate r) -> has_sup_graph r f ->
least_upper_bound r (range f) (sup_graph r f).
Proof. uf has_sup_graph. uf sup_graph. uf is_sup_graph. ir. fprops.
Qed.
Lemma is_inf_graph_pr1: forall r f,
order r -> sub (range f) (substrate r) -> has_inf_graph r f ->
greatest_lower_bound r (range f) (inf_graph r f).
Proof. uf has_inf_graph. uf inf_graph. uf is_inf_graph. ir. fprops.
Qed.
Lemma is_sup_graph_pr: forall r f x, order r -> sub (range f) (substrate r) ->
fgraph f ->
is_sup_graph r f x = (inc x (substrate r)
& (forall a, inc a (domain f) -> gle r (V a f) x)
& forall z, inc z (substrate r) -> (forall a, inc a (domain f)
-> gle r (V a f) z) -> gle r x z).
Proof. ir. uf is_sup_graph. aw. uf upper_bound.
assert (is_graph f). red in H1; eee.
ap iff_eq; ir; ee. am. ir. ap H5. fprops.
ir. ap H4. split. am. ir. awi H8. nin H8.
cp (pr2_V H1 H8). awi H9. rw H9. app H7. ex_tac. am. am.
ir. awi H6. nin H6. cp (pr2_V H1 H6). awi H7. rw H7. app H4. ex_tac. am.
ir. nin H6. app H5. ir. ap H7. fprops.
Qed.
Lemma is_inf_graph_pr: forall r f x, order r -> sub (range f) (substrate r) ->
fgraph f ->
is_inf_graph r f x = (inc x (substrate r)
& (forall a, inc a (domain f) -> gle r x (V a f))
& forall z, inc z (substrate r) -> (forall a, inc a (domain f)
-> gle r z (V a f)) -> gle r z x).
Proof. ir. uf is_inf_graph. aw. uf lower_bound.
assert (is_graph f). nin H1; am.
ap iff_eq; ir; ee. am. ir. ap H5. fprops.
ir. ap H4. split. am. ir. awi H8. nin H8.
cp (pr2_V H1 H8). awi H9. rw H9. app H7. ex_tac. am. am.
ir. awi H6. nin H6. cp (pr2_V H1 H6). awi H7. rw H7. app H4. ex_tac. am.
ir. nin H6. ap H5. am. ir. ap H7. fprops.
Qed.
Theorem compare_inf_sup1: forall r A, order r -> sub A (substrate r) ->
has_supremum r A -> has_infimum r A ->
A = emptyset ->
(greatest_element r (infimum r A) & least_element r (supremum r A)).
Proof. ir. cp (supremum_pr1 H H0 H1). cp (infimum_pr1 H H0 H2).
rw H3. split. rwi H3 H5. rwii greatest_lower_bound_emptyset H5.
rwi H3 H4. rwii least_upper_bound_emptyset H4.
Qed.
Theorem compare_inf_sup2: forall r A, order r -> sub A (substrate r) ->
has_supremum r A -> has_infimum r A ->
nonempty A -> gle r (infimum r A) (supremum r A).
Proof. ir. cp (supremum_pr1 H H0 H1). cp (infimum_pr1 H H0 H2).
nin H3. awii H4. nin H4. nin H4. awii H5. nin H5. nin H5.
cp (H7 _ H3). cp (H9 _ H3). order_tac.
Qed.
Theorem sup_increasing: forall r A B, order r -> sub A (substrate r) ->
sub B (substrate r) -> sub A B ->
has_supremum r A -> has_supremum r B->
gle r (supremum r A) (supremum r B).
Proof. ir. cp (supremum_pr1 H H0 H3). cp (supremum_pr1 H H1 H4).
awii H5. awii H6. ee.
assert (upper_bound r A (supremum r B)). red. red in H6. ee. am. ir.
app H9. app H2. app H8.
Qed.
Theorem inf_decreasing: forall r A B, order r -> sub A (substrate r) ->
sub B (substrate r) -> sub A B ->
has_infimum r A -> has_infimum r B ->
gge r (infimum r A) (infimum r B).
Proof. ir. cp (infimum_pr1 H H0 H3). cp (infimum_pr1 H H1 H4).
awii H5. awii H6. ee.
assert(lower_bound r A (infimum r B)). red. red in H6. ee. am. ir.
app H9. app H2. red. app H8.
Qed.
Lemma sup_increasing1: forall r f j,
order r -> fgraph f -> sub (range f) (substrate r) -> sub j (domain f) ->
has_sup_graph r f ->
has_sup_graph r (restr f j) ->
gle r (sup_graph r (restr f j)) (sup_graph r f).
Proof. uf has_sup_graph. uf is_sup_graph. uf sup_graph. ir.
assert (is_graph (restr f j)). cp (restr_fgraph j H0). red in H5; eee.
assert (sub (range (restr f j)) (range f)). red. ir.
awi H6. nin H6. cp (restr_sub H6). aw. ex_tac. fprops. am.
app sup_increasing. apply sub_trans with (range f). am. am.
Qed.
Lemma inf_decreasing1: forall r f j,
order r -> fgraph f -> sub (range f) (substrate r) -> sub j (domain f) ->
has_inf_graph r f -> has_inf_graph r (restr f j) ->
gge r (inf_graph r (restr f j)) (inf_graph r f).
Proof. uf has_inf_graph. uf is_inf_graph. uf inf_graph. ir.
assert (is_graph (restr f j)). cp (restr_fgraph j H0). red in H5; eee.
assert (sub (range (restr f j)) (range f)). red. ir.
awi H6. nin H6. cp (restr_sub H6). aw. ex_tac. nin H0; am. am.
app inf_decreasing. apply sub_trans with (range f). am. am.
Qed.
Lemma sup_increasing2: forall r f f',
order r -> fgraph f -> fgraph f' -> domain f = domain f' ->
sub (range f) (substrate r) -> sub (range f') (substrate r) ->
has_sup_graph r f -> has_sup_graph r f'->
(forall x , inc x (domain f) -> gle r (V x f) (V x f')) ->
gle r (sup_graph r f) (sup_graph r f').
Proof. ir. cp (is_sup_graph_pr1 H H3 H5). cp (is_sup_graph_pr1 H H4 H6).
cp (is_sup_graph_pr (sup_graph r f) H H3 H0).
ufi is_sup_graph H10. rwi H10 H8. clear H10.
cp (is_sup_graph_pr (sup_graph r f') H H4 H1).
ufi is_sup_graph H10. rwi H10 H9. clear H10. ee. ap H13. am. ir.
apply order_transitivity with (V a f'). am. app H7. app H10. wrr H2.
Qed.
Lemma inf_increasing2: forall r f f',
order r -> fgraph f -> fgraph f' -> domain f = domain f' ->
sub (range f) (substrate r) -> sub (range f') (substrate r) ->
has_inf_graph r f ->
has_inf_graph r f'->
(forall x , inc x (domain f) -> gle r (V x f) (V x f')) ->
gle r (inf_graph r f) (inf_graph r f').
Proof. ir. cp (is_inf_graph_pr1 H H3 H5). cp (is_inf_graph_pr1 H H4 H6).
cp (is_inf_graph_pr (inf_graph r f) H H3 H0).
ufi is_inf_graph H10. rwi H10 H8. clear H10.
cp (is_inf_graph_pr (inf_graph r f') H H4 H1).
ufi is_inf_graph H10. rwi H10 H9. clear H10. ee. ap H11. am. ir.
apply order_transitivity with (V a f). am. app H12. rww H2. app H7. rww H2.
Qed.
Associativity of sup and inf
Lemma sup_distributive: forall r f c x,
order r -> fgraph f -> sub (range f) (substrate r) ->
covering c (domain f) ->
(forall l, inc l (domain c) -> has_sup_graph r (restr f (V l c))) ->
is_sup_graph r f x =
is_sup_graph r (L (domain c) (fun l => sup_graph r (restr f (V l c)))) x.
Proof. ir. assert (Hb: is_graph f). fprops.
assert (He:forall a, fgraph (restr f (V a c))). ir. fprops.
assert (Hc:forall a, is_graph (restr f (V a c))). ir. cp (He a). fprops.
assert (Ha:fgraph (L (domain c)
(fun l => sup_graph r (restr f (V l c))))). gprops.
assert (Hd:forall a, (sub (range (restr f (V a c))) (substrate r))).
ir. red. ir. awi H4. nin H4. cp (restr_sub H4). app H1. ex_tac. app Hc.
assert (sub (range (L (domain c) (fun l => sup_graph r (restr f (V l c)))))
(substrate r)). red. ir. bwi H4. nin H4. nin H4.
cp (is_sup_graph_pr1 H (Hd x1) (H3 _ H4)). rwi H5 H6.
awi H6. nin H6. red in H6. nin H6. am. am. app Hd.
app iff_eq. ir. rwii is_sup_graph_pr H5. ee.
rww is_sup_graph_pr. split. am. bw. split. ir. bw.
cp (is_sup_graph_pr1 H (Hd a) (H3 _ H8)). rwi least_upper_bound_pr H9.
nin H9. app H10. red. split. am. ir. awi H11. nin H11. rwi restr_inc_rw H11.
awi H11. nin H11. cp (in_graph_V H0 H11). awi H13. rw (pr2_def H13).
app H6. ex_tac. app Hc. am. app Hd.
ir. red in H2. nin H2. app H7. ir. cp (H10 _ H11). cp (unionb_exists H12).
nin H13. nin H13. cp (H9 _ H13). bwi H15.
apply order_transitivity with (sup_graph r (restr f (V x0 c))). am.
cp (is_sup_graph_pr1 H (Hd x0) (H3 _ H13)). rwi least_upper_bound_pr H16.
nin H16. red in H16. nin H16. app H18. srw.
rw restr_domain. exists a. split. app intersection2_inc. rww restr_ev1.
am. am. fprops. am. am.
ir. rwii is_sup_graph_pr H5. ee. rww is_sup_graph_pr. split. am. split. ir.
bwi H6. bwi H7. red in H2. nin H2. cp (H9 _ H8). nin (unionb_exists H10).
nin H11. cp (H6 _ H11). bwi H13.
apply order_transitivity with (sup_graph r (restr f (V x0 c))). am.
cp (Hd x0). cp (is_sup_graph_pr1 H H14 (H3 _ H11)).
rwi least_upper_bound_pr H15.
nin H15. red in H15. nin H15. app H17. srw. exists a.
rw restr_domain. split. app intersection2_inc. rww restr_ev1. am. am.
am. am. am.
ir. app H7. bw. ir. bw. cp (Hd a).
cp (is_sup_graph_pr1 H H11 (H3 _ H10)). rwi least_upper_bound_pr H12.
nin H12. app H13. red. split. am. ir. awi H14. nin H14. rwi restr_inc_rw H14.
awi H14. nin H14. cp (in_graph_V H0 H14). awi H16. rw (pr2_def H16).
app H9. ex_tac. app Hc. am. am.
Qed.
Lemma inf_distributive: forall r f c x,
order r -> fgraph f -> sub (range f) (substrate r) ->
covering c (domain f) ->
(forall l, inc l (domain c) -> has_inf_graph r (restr f (V l c))) ->
is_inf_graph r f x =
is_inf_graph r (L (domain c) (fun l => inf_graph r (restr f (V l c)))) x.
Proof. ir. assert (Ha:fgraph (L (domain c)
(fun l => inf_graph r (restr f (V l c))))). gprops.
assert (He:forall a, fgraph (restr f (V a c))). ir. fprops.
assert (Hc:forall a, is_graph (restr f (V a c))). ir. cp (He a). fprops.
assert (Hd:forall a, (sub (range (restr f (V a c))) (substrate r))).
ir. red. ir. awi H4. nin H4. cp (restr_sub H4). app H1. nin H0. ex_tac.
app Hc.
assert ( sub (range (L (domain c) (fun l => inf_graph r (restr f (V l c)))))
(substrate r)). red. ir. bwi H4. nin H4. nin H4.
cp (Hd x1). cp (is_inf_graph_pr1 H H6 (H3 _ H4)). rwi H5 H7.
rwi greatest_lower_bound_pr H7. nin H7. red in H7. nin H7. am. am. am.
app iff_eq. ir. rwii is_inf_graph_pr H5. ee.
rww is_inf_graph_pr. split. am. bw. split. ir. bw.
cp (Hd a). cp (is_inf_graph_pr1 H H9 (H3 _ H8)).
rwi greatest_lower_bound_pr H10.
nin H10. app H11. red. split. am. ir. awi H12. nin H12. rwi restr_inc_rw H12.
awi H12. nin H12. cp (in_graph_V H0 H12). awi H14. rw (pr2_def H14).
app H6. nin H0. ex_tac. app Hc. am. am.
ir. red in H2. nin H2. app H7. ir. cp (H10 _ H11). cp (unionb_exists H12).
nin H13. nin H13. cp (H9 _ H13). bwi H15.
apply order_transitivity with (inf_graph r (restr f (V x0 c))). am. am.
cp (Hd x0). cp (is_inf_graph_pr1 H H16 (H3 _ H13)).
rwi greatest_lower_bound_pr H17. nin H17. red in H17. nin H17. app H19.
srw. exists a. rw restr_domain. split. app intersection2_inc. rww restr_ev1.
am. am. am. am.
ir. rwii is_inf_graph_pr H5. ee. rww is_inf_graph_pr. split. am. split. ir.
bwi H6. bwi H7. red in H2. nin H2. cp (H9 _ H8). nin (unionb_exists H10).
nin H11. cp (H6 _ H11). bwi H13.
apply order_transitivity with (inf_graph r (restr f (V x0 c))). am. am.
cp (Hd x0). cp (is_inf_graph_pr1 H H14 (H3 _ H11)).
rwi greatest_lower_bound_pr H15. nin H15. red in H15. nin H15. app H17.
srw. exists a. rw restr_domain. split. app intersection2_inc. rww restr_ev1.
am. am. am. am.
ir. app H7. bw. ir. bw.
cp (Hd a). cp (is_inf_graph_pr1 H H11 (H3 _ H10)).
rwi greatest_lower_bound_pr H12.
nin H12. app H13. red. split. am. ir. awi H14. nin H14. rwi restr_inc_rw H14.
awi H14. nin H14. cp (in_graph_V H0 H14). awi H16. rw (pr2_def H16).
app H9. nin H0. ex_tac. app Hc. am. am.
Qed.
Lemma sup_distributive1: forall r f c,
order r -> fgraph f -> sub (range f) (substrate r) ->
covering c (domain f) ->
(forall l, inc l (domain c) -> has_sup_graph r (restr f (V l c))) ->
has_sup_graph r f =
has_sup_graph r (L (domain c) (fun l => sup_graph r (restr f (V l c)))) .
Proof. ir. ap iff_eq; ir; nin H4; cp (sup_distributive x H H0 H1 H2 H3);
ufi is_sup_graph H5; exists x; [ wrr H5 | rww H5].
Qed.
Lemma inf_distributive1: forall r f c,
order r -> fgraph f -> sub (range f) (substrate r) ->
covering c (domain f) ->
(forall l, inc l (domain c) -> has_inf_graph r (restr f (V l c))) ->
has_inf_graph r f =
has_inf_graph r (L (domain c) (fun l => inf_graph r (restr f (V l c)))) .
Proof. ir. ap iff_eq; ir;nin H4; cp (inf_distributive x H H0 H1 H2 H3);
ufi is_inf_graph H5;exists x; [wrr H5 | rww H5].
Qed.
Theorem sup_distributive2: forall r f c,
order r -> fgraph f -> sub (range f) (substrate r) ->
covering c (domain f) ->
(forall l, inc l (domain c) -> has_sup_graph r (restr f (V l c))) ->
((has_sup_graph r f =
has_sup_graph r (L (domain c) (fun l => sup_graph r (restr f (V l c))))) &
(has_sup_graph r f -> sup_graph r f =
sup_graph r (L (domain c) (fun l => sup_graph r (restr f (V l c)))))).
Proof. ir. split. app sup_distributive1. ir. uf sup_graph.
set (g:= L (domain c) (fun l => sup_graph r (restr f (V l c)))).
cp (is_sup_graph_pr1 H H1 H4).
assert (least_upper_bound r (range f) (supremum r (range f))).
app supremum_pr1.
cp (sup_distributive (sup_graph r f) H H0 H1 H2 H3). ufi is_sup_graph H7.
fold g in H7.
assert(least_upper_bound r (range g) (sup_graph r f)). wrr H7. clear H7.
set (x:= sup_graph r f). fold x in H5; fold x in H8.
cp (supremum_unique H H5 H6). wr H7.
assert (least_upper_bound r (range g) (supremum r (range g))).
app supremum_pr1. red. uf g. ir. bwi H9. nin H9. nin H9.
assert (sub (range (restr f (V x1 c))) (substrate r)).
red. ir. awi H11. nin H11. cp (restr_sub H11). app H1. aw. exists x3. am.
red in H0; eee. cp (restr_fgraph (V x1 c) H0). red in H12; eee.
cp (is_sup_graph_pr1 H H11 (H3 _ H9)). rwi H10 H12.
rwi least_upper_bound_pr H12. nin H12. red in H12. nin H12. am. am. am.
exists x. am. app (supremum_unique H H8 H9).
Qed.
Theorem inf_distributive2: forall r f c,
order r -> fgraph f -> sub (range f) (substrate r) ->
covering c (domain f) ->
(forall l, inc l (domain c) -> has_inf_graph r (restr f (V l c))) ->
((has_inf_graph r f =
has_inf_graph r (L (domain c) (fun l => inf_graph r (restr f (V l c))))) &
(has_inf_graph r f -> inf_graph r f =
inf_graph r (L (domain c) (fun l => inf_graph r (restr f (V l c)))))).
Proof. ir. split. app inf_distributive1. ir.
set (g:= L (domain c) (fun l => inf_graph r (restr f (V l c)))).
uf inf_graph.
cp (is_inf_graph_pr1 H H1 H4).
assert (greatest_lower_bound r (range f) (infimum r (range f))).
app infimum_pr1.
cp (inf_distributive (inf_graph r f) H H0 H1 H2 H3). ufi is_inf_graph H7.
fold g in H7.
assert(greatest_lower_bound r (range g) (inf_graph r f)). wrr H7. clear H7.
set (x:= inf_graph r f). fold x in H5; fold x in H8.
cp (infimum_unique H H5 H6). wr H7.
assert (greatest_lower_bound r (range g) (infimum r (range g))).
app infimum_pr1. red. uf g. ir. bwi H9. nin H9. nin H9.
assert (sub (range (restr f (V x1 c))) (substrate r)).
red. ir. awi H11. nin H11. cp (restr_sub H11). app H1. aw. exists x3. am.
red in H0; eee. cp (restr_fgraph (V x1 c) H0). red in H12; eee.
cp (is_inf_graph_pr1 H H11 (H3 _ H9)). rwi H10 H12.
rwi greatest_lower_bound_pr H12. nin H12. red in H12. nin H12. am. am. am.
exists x. am. app (infimum_unique H H8 H9).
Qed.
Definition partial_fun f x m := restr f (product x (singleton m)).
Lemma sup_distributive3: forall r f x y,
order r -> fgraph f -> sub (range f) (substrate r) ->
domain f = product x y ->
(forall m, inc m y -> has_sup_graph r (partial_fun f x m)) ->
((has_sup_graph r f =
has_sup_graph r (L y (fun m => sup_graph r (partial_fun f x m)))) &
(has_sup_graph r f -> sup_graph r f =
sup_graph r (L y (fun m => sup_graph r (partial_fun f x m))))).
Proof. ir. set (c:= L y (fun m => product x (singleton m))).
assert (covering c (domain f)). red. split. uf c. gprops.
rw H2. red. ir. awi H4. nin H4. nin H5.
apply unionb_inc with (Q x0). uf c. bw. uf c. bw.
app product_inc. fprops.
assert (y = domain c). uf c. bw.
assert (forall m, inc m y -> partial_fun f x m = restr f (V m c)).
ir. uf partial_fun. uf c. bw.
assert (forall l, inc l (domain c) -> has_sup_graph r (restr f (V l c))).
ir. wr H6. app H3. rww H5. rww H5.
assert ( L (domain c) (fun l => sup_graph r (restr f (V l c))) =
L y (fun m : Set => sup_graph r (partial_fun f x m))). wr H5.
app L_exten1. ir. rww H6. wr H8. app sup_distributive2.
Qed.
Lemma inf_distributive3: forall r f x y,
order r -> fgraph f -> sub (range f) (substrate r) ->
domain f = product x y ->
(forall m, inc m y -> has_inf_graph r (partial_fun f x m)) ->
((has_inf_graph r f =
has_inf_graph r (L y (fun m => inf_graph r (partial_fun f x m)))) &
(has_inf_graph r f -> inf_graph r f =
inf_graph r (L y (fun m => inf_graph r (partial_fun f x m))))).
Proof. ir. set (c:= L y (fun m => product x (singleton m))).
assert (covering c (domain f)). red. split. uf c. gprops.
rw H2. red. ir. awi H4. nin H4. nin H5.
apply unionb_inc with (Q x0). uf c. bw. uf c. bw. app product_inc. fprops.
assert (y = domain c). uf c. bw.
assert (forall m, inc m y -> partial_fun f x m = restr f (V m c)).
ir. uf partial_fun. uf c. bw.
assert (forall l, inc l (domain c) -> has_inf_graph r (restr f (V l c))).
ir. wr H6. app H3. rww H5. rww H5.
assert ( L (domain c) (fun l => inf_graph r (restr f (V l c))) =
L y (fun m : Set => inf_graph r (partial_fun f x m))). wr H5.
app L_exten1. ir. rww H6. wr H8. app inf_distributive2.
Qed.
Theorem sup_in_product: forall g A,
let f := fam_of_substrates g in
let Ai:= fun i => (image_by_fun (pr_i f i) A) in
let has_sup :=
forall i, inc i (domain g) -> has_supremum (V i g) (Ai i) in
product_order_axioms g -> sub A (productb f) ->
((has_sup = has_supremum (product_order g) A) &
(has_sup -> supremum (product_order g) A =
L (domain g) (fun i => supremum (V i g) (Ai i)))).
Proof. ir. assert (Ha:product_order_axioms g). am.
red in H. nin H.
assert (Hb: fgraph f). uf f. uf fam_of_substrates. gprops.
assert (Hc: domain f = domain g). uf f. uf fam_of_substrates. bw.
assert (Hd: forall i, inc i (domain g) -> substrate (V i g) = V i f).
ir. uf f. uf fam_of_substrates. bw.
assert (He: forall i, inc i (domain g) -> sub A (source (pr_i f i))).
ir. uf pr_i. aw.
assert (forall i, inc i (domain g) -> sub (Ai i) (substrate (V i g))).
ir. rww Hd. uf Ai. red. ir. awi H3. nin H3. ee.
assert (V i f = target (pr_i f i)). uf pr_i. aw. rw H5. wr H4.
app inc_W_target. app pri_function. ue. app (He _ H2).
app pri_function. ue. uf pr_i. aw.
assert (has_sup -> (forall i, inc i (domain g) ->
least_upper_bound (V i g) (Ai i) (supremum (V i g) (Ai i)))). ir.
app supremum_pr1. app H1. app H2. app H3.
set (mysup:=L (domain g) (fun i : Set => supremum (V i g) (Ai i))).
assert (has_sup -> least_upper_bound (product_order g) A mysup). ir.
assert (inc mysup (productb f)). aw. split. uf mysup.
gprops. uf mysup. split. bw. ue. bw. ir. bw. wrr Hd.
app inc_supremum_substrate. app H1. app H2. app H4.
aw. split. red. split. rww product_order_substrate.
ir. rw product_order_related. split. app H0. split. am. ir.
uf mysup. bw.
nin (supremum_pr (H1 _ H7) (H2 _ H7) (H4 _ H7)). red in H8. ee.
app H10. uf Ai. aw. ex_tac. wri Hc H7. rww (pri_W Hb H7 (H0 _ H6)).
app pri_function. ue. app He. am.
ir. nin H6. aw. rw product_order_related. split. am. split.
rwi product_order_substrate H6. am. am. ir.
assert (is_function (pr_i f i)). app pri_function. ue.
nin (supremum_pr (H1 _ H8) (H2 _ H8) (H4 _ H8)).
uf mysup. bw. app H11. red. split.
awi H6. eee. am. am.
ir. ufi Ai H12. awi H12. nin H12. nin H12. wr H13.
wri Hc H8. rw (pri_W Hb H8 (H0 _ H12)).
cp (H7 _ H12). bwi H14. ee. app H16. ue. am. am. uf pr_i. aw. am.
app product_order_order.
assert (has_sup -> has_supremum (product_order g) A). ir.
exists mysup. app H4.
assert (has_sup -> supremum (product_order g) A = mysup).
ir. assert (order (product_order g)). app product_order_order.
ufi f H0. cp (product_order_substrate Ha) . ufi prod_of_substrates H8.
wri H8 H0. cp (supremum_pr1 H7 H0 (H5 H6)).
cp (H4 H6). ap (supremum_unique H7 H9 H10).
split. app iff_eq. ir. red. nin H7. rwi least_upper_bound_pr H7. nin H7.
ir. red. exists (V i x). rw least_upper_bound_pr.
assert (is_function (pr_i f i)). app pri_function. ue.
split. red in H7. nin H7. awii H7.
red. split. ee. app H13.
ir. ufi Ai H12. awi H12. nin H12. nin H12. wr H13.
wri Hc H9. rw (pri_W Hb H9 (H0 _ H12)). cp (H11 _ H12). bwi H14. ee. app H16.
ue. am. am. uf pr_i. aw.
ir. set (y:= L (domain g) (fun j=> Yo(j=i) z (V j x))).
assert (z = V i y). uf y. bw. rw Y_if_rw. tv. tv.
assert (inc y (productb f)). aw. ee. uf y. gprops.
uf y. bw. ue. uf y. bw. ir. bw. nin (equal_or_not i0 i).
ir. rw Y_if_rw. rw H14. red in H11. ee. wrr Hd. am.
rw Y_if_not_rw. nin H7. awi H7. ee. wrr Hd. app H17. am. am. am.
rw H12. assert (upper_bound (product_order g) A y). red. split.
rw product_order_substrate. am. am. ir. bw. ee.
app H0. am. ir. uf y. bw. nin (equal_or_not i0 i).
ir. rw Y_if_rw. rw H16. red in H11. ee. app H17. uf Ai. aw. ex_tac.
wri Hc H9. wrr (pri_W Hb H9 (H0 _ H14)). uf pr_i. aw. am. ir.
rw Y_if_not_rw. nin H7. set (H17 _ H14). bwi g0. ee. app H20. am. am.
cp (H8 _ H14). bwi H15. eee. am. app H1. app H2.
app product_order_order. rww product_order_substrate. am.
Qed.
Theorem inf_in_product: forall g A,
let f := fam_of_substrates g in
let Ai:= fun i => (image_by_fun (pr_i f i) A) in
let has_inf :=
forall i, inc i (domain g) -> has_infimum (V i g) (Ai i) in
product_order_axioms g -> sub A (productb f) ->
((has_inf = has_infimum (product_order g) A) &
(has_inf -> infimum (product_order g) A =
L (domain g) (fun i => infimum (V i g) (Ai i)))).
Proof. ir. assert (Ha:product_order_axioms g). am.
red in H. nin H.
assert (Hb: fgraph f). uf f. uf fam_of_substrates. gprops.
assert (Hc: domain f = domain g). uf f. uf fam_of_substrates. bw.
assert (Hd: forall i, inc i (domain g) -> substrate (V i g) = V i f).
ir. uf f. uf fam_of_substrates. bw.
assert (He: forall i, inc i (domain g) -> sub A (source (pr_i f i))).
ir. uf pr_i. aw.
assert (forall i, inc i (domain g) -> sub (Ai i) (substrate (V i g))).
ir. rww Hd. uf Ai. red. ir. awi H3. nin H3. ee.
assert (V i f = target (pr_i f i)). uf pr_i. aw. rw H5. wr H4.
app inc_W_target. app pri_function. ue. app (He _ H2).
app pri_function. ue. uf pr_i. aw.
assert (has_inf -> (forall i, inc i (domain g) ->
greatest_lower_bound (V i g) (Ai i) (infimum (V i g) (Ai i)))). ir.
app infimum_pr1. app H1. app H2. app H3.
set (myinf:=L (domain g) (fun i : Set => infimum (V i g) (Ai i))).
assert (has_inf -> greatest_lower_bound (product_order g) A myinf). ir.
assert (inc myinf (productb f)). aw. split. uf myinf.
gprops. uf myinf. split. bw. ue. bw. ir. bw. wrr Hd.
app inc_infimum_substrate. app H1. app H2. app H4. aw.
split. red. split. rww product_order_substrate.
ir. bw. split. am. split. app H0. ir.
uf myinf. bw.
nin (infimum_pr (H1 _ H7) (H2 _ H7) (H4 _ H7)). red in H8. ee.
app H10. uf Ai. aw. ex_tac. wri Hc H7. rww (pri_W Hb H7 (H0 _ H6)).
app pri_function. ue. app He.
ir. nin H6. aw. bw. split.
rwi product_order_substrate H6. am. am. split. am. ir.
assert (is_function (pr_i f i)). app pri_function. ue.
nin (infimum_pr (H1 _ H8) (H2 _ H8) (H4 _ H8)).
uf myinf. bw. app H11. red. split. awi H6. ee. app H13. am. am.
ir. ufi Ai H12. awi H12. nin H12. nin H12. wr H13.
wri Hc H8. rw (pri_W Hb H8 (H0 _ H12)).
cp (H7 _ H12). bwi H14. ee. app H16. ue. am. am. uf pr_i. aw.
app product_order_order.
assert (has_inf -> has_infimum (product_order g) A). ir.
exists myinf. app H4.
assert (has_inf -> infimum (product_order g) A = myinf).
ir. assert (order (product_order g)). app product_order_order.
ufi f H0. cp (product_order_substrate Ha) . ufi prod_of_substrates H8.
wri H8 H0. cp (infimum_pr1 H7 H0 (H5 H6)).
cp (H4 H6). ap (infimum_unique H7 H9 H10).
split. app iff_eq. ir. red. nin H7. awi H7. nin H7.
ir. red. exists (V i x). aw.
assert (is_function (pr_i f i)). app pri_function. ue.
split. red in H7. nin H7. awii H7.
red. split. ee. app H13.
ir. ufi Ai H12. awi H12. nin H12. nin H12. wr H13.
wri Hc H9. rw (pri_W Hb H9 (H0 _ H12)). cp (H11 _ H12). bwi H14. ee. app H16.
ue. am. am. uf pr_i. aw.
ir. set (y:= L (domain g) (fun j=> Yo(j=i) z (V j x))).
assert (z = V i y). uf y. bw. rw Y_if_rw. tv. tv.
assert (inc y (productb f)). aw. ee. uf y. gprops.
uf y. bw. ue. uf y. bw. ir. bw. nin (equal_or_not i0 i).
ir. rw Y_if_rw. rw H14. red in H11. ee. wrr Hd. am.
rw Y_if_not_rw. nin H7. awi H7. ee. wrr Hd. app H17. am. am. am.
rw H12. assert (lower_bound (product_order g) A y). red. split.
rw product_order_substrate. am. am. ir. bw. ee. am.
app H0. ir. uf y. bw. nin (equal_or_not i0 i).
ir. rw Y_if_rw. rw H16. red in H11. ee. app H17. uf Ai. aw. ex_tac.
wri Hc H9. wrr (pri_W Hb H9 (H0 _ H14)). uf pr_i. aw. am. ir.
rw Y_if_not_rw. nin H7. set (H17 _ H14). bwi g0. ee. app H20. am. am.
cp (H8 _ H14). bwi H15. eee. am. app H1. app H2.
app product_order_order. rww product_order_substrate. am.
Qed.
Theorem sup_induced1: forall r A F, order r -> sub F (substrate r) -> sub A F ->
has_supremum r A -> has_supremum (induced_order r F) A ->
gle r (supremum r A) (supremum (induced_order r F) A).
Proof. ir.
assert (order (induced_order r F)). fprops.
assert (sub A (substrate r)). apply sub_trans with F. am. am.
assert (sub A (substrate (induced_order r F))). aw.
cp (supremum_pr1 H H5 H2). cp (supremum_pr1 H4 H6 H3).
set (u:= supremum r A). set (v:=supremum (induced_order r F) A).
fold u in H7. fold v in H8. awi H7; awi H8;try am. ee.
app H10. red. split. red in H8. nin H8. awi H8.
app H0. am. am. ir. red in H8; ee. cp (H12 _ H11). awi H13. am. app H1.
awi H8. am. am. am.
Qed.
Theorem inf_induced1: forall r A F, order r -> sub F (substrate r) -> sub A F ->
has_infimum r A -> has_infimum (induced_order r F) A ->
gge r (infimum r A) (infimum (induced_order r F) A).
Proof. ir. assert (order (induced_order r F)). fprops.
assert (sub A (substrate r)). apply sub_trans with F. am. am.
assert (sub A (substrate (induced_order r F))). aw.
cp (infimum_pr1 H H5 H2). cp (infimum_pr1 H4 H6 H3).
set (u:= infimum r A). set (v:=infimum (induced_order r F) A).
fold u in H7. fold v in H8. awi H7; awi H8; try am. ee.
red. app H10. red. split. red in H8. nin H8. awi H8.
app H0. am. am. ir. red in H8; ee. cp (H12 _ H11).
awi H13. am. awi H8. am. am. am. app H1.
Qed.
Theorem sup_induced2: forall r A F, order r -> sub F (substrate r) -> sub A F ->
has_supremum r A -> inc (supremum r A) F ->
(has_supremum (induced_order r F) A &
supremum r A = supremum (induced_order r F) A).
Proof. ir. assert (order (induced_order r F)). fprops.
assert (sub A (substrate r)). apply sub_trans with F. am. am.
assert (sub A (substrate (induced_order r F))). aw.
cp (supremum_pr1 H H5 H2). set (u:= supremum r A).
assert (least_upper_bound (induced_order r F) A u). awi H7. aw. ee.
red. split. aw. ir. red. aw. red in H7. ee. app H10. app H1.
ir. red in H9. ee. aw. app H8. red. split. awi H9. app H0. am. am. ir.
cp (H10 _ H11). awi H12. am. app H1. awi H9. am. am. am. awi H9. am. am.
am. am. am. split. exists u. am.
assert (has_supremum (induced_order r F) A). exists u. am.
cp (supremum_pr1 H4 H6 H9). ap (supremum_unique H4 H8 H10).
Qed.
Theorem inf_induced2: forall r A F, order r -> sub F (substrate r) -> sub A F ->
has_infimum r A -> inc (infimum r A) F ->
(has_infimum (induced_order r F) A &
infimum r A = infimum (induced_order r F) A).
Proof. ir. assert (order (induced_order r F)). fprops.
assert (sub A (substrate r)). apply sub_trans with F. am. am.
assert (sub A (substrate (induced_order r F))). aw.
cp (infimum_pr1 H H5 H2). set (u:= infimum r A).
assert (greatest_lower_bound (induced_order r F) A u). awi H7. aw. ee.
red. split. aw. ir. red. aw. red in H7. ee. app H10. app H1.
ir. red in H9. ee. aw. app H8. red. split. awi H9. app H0. am. am. ir.
cp (H10 _ H11). awi H12. am. awi H9. am. am. am. app H1.
awi H9. am. am. am. am. am. split. exists u. am.
assert (has_infimum (induced_order r F) A). exists u. am.
cp (infimum_pr1 H4 H6 H9). ap (infimum_unique H4 H8 H10).
Qed.
Definition right_directed r :=
order r & forall x, forall y, inc x (substrate r) -> inc y (substrate r) ->
bounded_above r (doubleton x y).
Definition left_directed r :=
order r & forall x, forall y, inc x (substrate r) -> inc y (substrate r) ->
bounded_below r (doubleton x y).
Lemma right_directed_pr: forall r,
right_directed r = (order r &
forall x, forall y, inc x (substrate r) -> inc y (substrate r) -> exists z,
inc z (substrate r) & gle r x z & gle r y z).
Proof. ir. uf right_directed. ap iff_eq; ir; ee. am. ir. cp (H0 _ _ H1 H2).
red in H3. nin H3. nin H3. ee. exists x0. ee. am. app H4.
fprops. app H4. fprops. am.
ir. cp (H0 _ _ H1 H2). nin H3. exists x0.
ee. red. split. am. ir. nin (doubleton_or H6); rww H7.
Qed.
Lemma left_directed_pr: forall r,
left_directed r = (order r &
forall x, forall y, inc x (substrate r) -> inc y (substrate r) -> exists z,
inc z (substrate r) & gle r z x & gle r z y).
Proof. ir. uf left_directed. ap iff_eq; ir; ee. am. ir. cp (H0 _ _ H1 H2).
red in H3. nin H3. nin H3. ee. exists x0. ee. am. app H4.
fprops. app H4. fprops. am.
ir. cp (H0 _ _ H1 H2). nin H3. exists x0.
ee. red. split. am. ir. nin (doubleton_or H6); rww H7.
Qed.
Lemma greatest_right_directed : forall r, order r ->
(exists a, greatest_element r a ) -> right_directed r.
Proof. ir. nin H0. red in H0. nin H0. rw right_directed_pr. split. am.
ir. exists x. split. am. split; app H1.
Qed.
Lemma least_left_directed : forall r, order r ->
(exists a, least_element r a ) -> left_directed r.
Proof. ir. nin H0. red in H0. nin H0. rw left_directed_pr. split. am.
ir. exists x. split. am. split; app H1.
Qed.
Lemma opposite_right_directed : forall r, is_graph r ->
right_directed r = left_directed(opposite_order r).
Proof. ir. rw right_directed_pr. rw left_directed_pr. app iff_eq. ir.
nin H0. assert (order (opposite_order r)). fprops. aw. split. am.
ir. cp (H1 _ _ H3 H4). nin H5. ee. exists x0. split. am. aw. intuition.
ir. nin H0. assert (order (opposite_order (opposite_order r))). fprops.
ufi opposite_order H2. rwi inverse_graph_involutive H2. awi H1.
split. am. ir. cp (H1 _ _ H3 H4). nin H5. ee. exists x0. split. am.
awi H6. awi H7. intuition. am. am. am. am.
Qed.
Lemma opposite_left_directed : forall r, is_graph r ->
left_directed r = right_directed(opposite_order r).
Proof. ir. sy.
assert (is_graph (opposite_order r)). fprops. rww opposite_right_directed.
rw inverse_graph_involutive. tv. am.
Qed.
Lemma product_right_directed: forall g,
product_order_axioms g ->
(forall i, inc i (domain g) -> right_directed (V i g))
-> right_directed (product_order g).
Proof. intros g. rw right_directed_pr. ir. split. fprops.
ir. set (z:= L (domain g)(fun i => choose (fun w =>
upper_bound (V i g) (doubleton (V i x) (V i y)) w))).
assert (forall i, inc i (domain g) ->
upper_bound (V i g) (doubleton (V i x) (V i y)) (V i z)).
ir. uf z. bw. ap choose_pr. cp (H0 _ H3). red in H4. nin H4. awii H1. awii H2.
ee. cp (H5 _ _ (H9 _ H3) (H7 _ H3)). app H10.
assert (inc z (substrate (product_order g))). aw. ee. uf z. gprops. uf z. bw.
ir. cp (H3 _ H4). nin H5. am.
rwi product_order_substrate H1. rwi product_order_substrate H2.
ex_tac. rwi product_order_substrate H4. bw. eee.
ir. cp (H3 _ H5). nin H6. app H7. fprops.
ir. cp (H3 _ H5). nin H6. app H7. fprops. am. am. am.
Qed.
Lemma product_left_directed: forall g,
product_order_axioms g ->
(forall i, inc i (domain g) -> left_directed (V i g))
-> left_directed (product_order g).
Proof. intros g. rw left_directed_pr. ir. split. fprops.
ir. set (z:= L (domain g)(fun i => choose (fun w =>
lower_bound (V i g) (doubleton (V i x) (V i y)) w))).
assert (forall i, inc i (domain g) ->
lower_bound (V i g) (doubleton (V i x) (V i y)) (V i z)).
ir. uf z. bw. ap choose_pr. cp (H0 _ H3). red in H4. nin H4. awii H1. awii H2.
ee. cp (H5 _ _ (H9 _ H3) (H7 _ H3)). app H10.
assert (inc z (substrate (product_order g))). aw. ee. uf z. gprops. uf z. bw.
ir. cp (H3 _ H4). nin H5. am.
rwi product_order_substrate H1. rwi product_order_substrate H2.
ex_tac. rwi product_order_substrate H4. bw. eee.
ir. cp (H3 _ H5). nin H6. app H7. fprops.
ir. cp (H3 _ H5). nin H6. app H7. fprops. am. am. am.
Qed.
Lemma cofinal_right_directed: forall r A,
right_directed r -> cofinal_set r A -> right_directed (induced_order r A).
Proof. intro r. rw right_directed_pr. ir. red in H0. ee. rw right_directed_pr.
split. fprops. aw. ir.
cp (H0 _ H3). cp (H0 _ H4). cp (H2 _ _ H5 H6). nin H7. ee. cp (H1 _ H7).
nin H10. ee. ex_tac.
split; aw; apply order_transitivity with x0; am.
Qed.
Lemma coinitial_left_directed: forall r A,
left_directed r -> coinitial_set r A -> left_directed (induced_order r A).
Proof. intro r. rw left_directed_pr. ir. red in H0. ee. rw left_directed_pr.
split. fprops. aw. ir.
cp (H0 _ H3). cp (H0 _ H4). cp (H2 _ _ H5 H6). nin H7. ee. cp (H1 _ H7).
nin H10. ee. ex_tac.
split; aw; apply order_transitivity with x0; am.
Qed.
Theorem right_directed_maximal: forall r x,
right_directed r -> maximal_element r x -> greatest_element r x.
Proof. ir. red in H0. ee. red. split. am. rwi right_directed_pr H. ee.
ir. cp (H2 _ _ H0 H3). nin H4. ee. wrr (H1 _ H5).
Qed.
Theorem left_directed_mimimal: forall r x,
left_directed r -> minimal_element r x -> least_element r x.
Proof. ir. red in H0. ee. red. split. am. rwi left_directed_pr H. ee.
ir. cp (H2 _ _ H0 H3). nin H4. ee. wrr (H1 _ H5).
Qed.
Definition lattice r := order r &
forall x, forall y, inc x (substrate r) -> inc y (substrate r) ->
(has_supremum r (doubleton x y) & has_infimum r (doubleton x y)).
Lemma lattice_sup_pr: forall r a b,
lattice r -> inc a (substrate r) -> inc b (substrate r) ->
(gle r a (sup r a b) & gle r b (sup r a b) &
forall z, gle r a z -> gle r b z -> gle r (sup r a b) z).
Proof. ir. red in H. nin H. cp (H2 _ _ H0 H1). app sup_pr. nin H3. am.
Qed.
Lemma lattice_inf_pr: forall r a b,
lattice r -> inc a (substrate r) -> inc b (substrate r) ->
(gle r (inf r a b) a & gle r (inf r a b) b&
forall z, gle r z a -> gle r z b -> gle r z (inf r a b)).
Proof. ir. red in H. nin H. cp (H2 _ _ H0 H1). app inf_pr. nin H3. am.
Qed.
Lemma inf_inclusion: forall A x y, sub x A -> sub y A ->
greatest_lower_bound (inclusion_order A) (doubleton x y) (intersection2 x y).
Proof. ir. assert (sub (doubleton x y) (powerset A)). app sub_doubleton.
app powerset_inc. app powerset_inc.
cp (intersection_is_inf H1). rwi Y_if_rw H2. am. app nonempty_doubleton.
Qed.
Lemma sup_inclusion: forall A x y, sub x A -> sub y A ->
least_upper_bound (inclusion_order A) (doubleton x y) (union2 x y).
Proof. ir. assert (sub (doubleton x y) (powerset A)). app sub_doubleton.
app powerset_inc. app powerset_inc. ap (union_is_sup H1).
Qed.
Lemma powerset_lattice: forall A, lattice (inclusion_order A).
Proof. ir. red. split. ap inclusion_is_order. rw substrate_inclusion_order.
ir. split. exists (union2 x y). app sup_inclusion. app powerset_sub.
app powerset_sub. exists (intersection2 x y). app inf_inclusion.
app powerset_sub. app powerset_sub.
Qed.
Lemma product_lattice: forall g,
product_order_axioms g ->
(forall i, inc i (domain g) -> lattice (V i g))
-> lattice (product_order g).
Proof. ir. red. split. fprops. aw.
ir. assert (sub (doubleton x y) (prod_of_substrates g)). red. ir.
nin (doubleton_or H3). rww H4. rww H4.
set (f := fam_of_substrates g).
assert (Ha: fgraph f). uf f. uf fam_of_substrates. gprops.
assert (Hb: domain f = domain g). uf f. uf fam_of_substrates. bw.
assert (Hc: productb f = prod_of_substrates g). tv.
assert (forall i, inc i (domain g) -> exists u, exists v,
inc u (substrate (V i g)) & inc v (substrate (V i g)) &
(image_by_fun (pr_i f i) (doubleton x y) = doubleton u v)).
ir. cp H1. cp H2. exists (V i x). exists (V i y). awi H1. ee. app H8.
awi H2. ee. app H10. am.
assert (is_function (pr_i f i)). app pri_function. ue.
assert (W x (pr_i f i) = (V i x)). app pri_W. ue.
assert (W y (pr_i f i) = (V i y)). app pri_W. ue.
set_extens. awi H12. nin H12. nin H12. nin (doubleton_or H12). wr H13.
rw H14. rww H10. fprops. wr H13. rw H14. rww H11. fprops. am. red. ir.
uf pr_i. rww bl_source.
nin (doubleton_or H13); rw H14. am. am. aw. nin (doubleton_or H12); rw H13.
exists x. split. fprops. am. exists y. split. fprops. am. uf pr_i. aw. am.
cp (sup_in_product H H3). nin H5. wr H5. split. ir.
cp (H4 _ H7). nin H8. nin H8. ee. fold f. rw H10. cp (H0 _ H7). nin H11.
cp (H12 _ _ H8 H9). nin H13. am.
cp (inf_in_product H H3). nin H7. wr H7. ir.
cp (H4 _ H9). nin H10. nin H10. ee. fold f. rw H12. cp (H0 _ H9). nin H13.
cp (H14 _ _ H10 H11). intuition.
Qed.
Lemma lattice_directed: forall r,
lattice r -> (right_directed r & left_directed r).
Proof. ir. split. red. nin H. ee. am. ir. cp (H0 _ _ H1 H2).
nin H3. nin H3. exists x0. aw. awi H3. nin H3. am. am. app sub_doubleton.
red. nin H. ee. am. ir. cp (H0 _ _ H1 H2).
nin H3. nin H4. exists x0. aw. awi H4. nin H4. am. am. app sub_doubleton.
Qed.
Definition total_order r :=
order r & forall x y, inc x (substrate r) -> inc y (substrate r) ->
(gle r x y \/ gge r x y).
Lemma total_order_pr: forall r,
total_order r =
(compose_graph r r = r &
intersection2 r (opposite_order r) = identity_g(substrate r)&
union2 r (opposite_order r) = coarse (substrate r)).
Proof. ir. uf total_order. app iff_eq. ir. nin H. cp H. rwi order_pr H.
eee. set_extens. nin (union2_or H3). assert (is_graph r). fprops.
app (sub_graph_coarse_substrate H5).
assert (order (opposite_order r)). fprops.
assert (substrate (opposite_order r) = substrate r).
app substrate_opposite_order. aw.
assert (is_graph (opposite_order r)). fprops. wr H6.
app (sub_graph_coarse_substrate H7).
ufi coarse H3. awi H3. nin H3. nin H4. nin (H0 _ _ H4 H5).
app union2_first. red in H6. red in H6. assert (J (P x) (Q x) = x). aw.
wrr H7. red in H6. red in H6. assert (J (P x) (Q x) = x). aw.
wrr H7. app union2_second. aw.
ir. nin H. assert (is_graph r). wr H. app composition_is_graph.
assert (order r). rw (order_pr r). intuition. split. am. ir.
nin H0. assert (inc (J x y) (coarse (substrate r))).
uf coarse. app product_pair_inc. wri H5 H6. nin (union2_or H6). left. am.
awi H7. right. am.
Qed.
Lemma total_order_pr1 : forall r x y,
total_order r -> inc x (substrate r) -> inc y (substrate r) ->
(glt r x y \/ ggt r x y \/ x = y).
Proof. ir. nin (equal_or_not x y). ir. auto.
ir. nin H. uf ggt;uf glt. nin (H3 _ _ H0 H1); auto.
Qed.
Lemma total_order_pr2 : forall r x y,
total_order r -> inc x (substrate r) -> inc y (substrate r) ->
(glt r x y \/ gle r y x).
Proof. ir. red in H. ee. cp (H2 _ _ H0 H1).
nin (equal_or_not x y). right. rw H4. order_tac. uf glt.
nin H3; auto.
Qed.
Lemma total_order_sub : forall r x,
total_order r -> sub x (substrate r) -> total_order (induced_order r x).
Proof. ir. red in H. ee. red. split. fprops. aw.
ir. uf gge. aw. ufi gge H1. ufi gle H1. app H1. app H0. app H0.
Qed.
Lemma total_order_small : forall r,
order r -> small_set(substrate r) -> total_order r.
Proof. ir. red. split. am. ir. red in H0. left. rw (H0 _ _ H1 H2). order_tac.
Qed.
Lemma total_order_conterexample:
~ (total_order (inclusion_order two_points)).
Proof. ir. red. ir. red in H. ee. rwi substrate_inclusion_order H0.
assert (inc (singleton TPa) (powerset two_points)). app powerset_inc.
red. ir. db_tac.
assert (inc (singleton TPb) (powerset two_points)). app powerset_inc.
red. ir. db_tac. nin (H0 _ _ H1 H2).
rwi inclusion_order_rw H3. ee. red in H5.
assert (inc TPa (singleton TPa)). fprops. cp (H5 _ H6). cp (singleton_eq H7).
elim two_points_distinct. am.
red in H3. rwi inclusion_order_rw H3. ee.
assert (inc TPb (singleton TPb)). fprops. cp (H5 _ H6). cp (singleton_eq H7).
elim two_points_distinctb. am.
Qed.
Lemma total_order_opposite: forall r,
total_order r -> total_order (opposite_order r).
Proof. ir. red. red in H. eee. aw. ir. aw.
nin (H0 _ _ H1 H2); au.
Qed.
If x is smaller than y, the pair has a supremum and an infimum
Lemma sup_comparable: forall r x y, gle r x y ->
order r -> least_upper_bound r (doubleton x y) y.
Proof. ir. red in H. assert (inc x (substrate r)). substr_tac.
assert (inc y (substrate r)). substr_tac.
aw. split. red.
split. am. ir. nin (doubleton_or H3). rww H4. rw H4. order_tac.
ir. red in H3. nin H3. app H4. fprops. app sub_doubleton.
Qed.
Lemma inf_comparable: forall r x y, gle r x y ->
order r -> greatest_lower_bound r (doubleton x y) x.
Proof. ir. red in H. assert (inc x (substrate r)). substr_tac.
assert (inc y (substrate r)). substr_tac. aw. split. red.
split. am. ir. nin (doubleton_or H3). rww H4. order_tac. ue.
ir. red in H3. nin H3. app H4. fprops. app sub_doubleton.
Qed.
Lemma inf_comparable1: forall r x y, order r -> gle r x y ->
inf r x y = x.
Proof. ir. cp (inf_comparable H0 H).
assert (has_infimum r (doubleton x y)). exists x. am.
uf inf. assert (sub (doubleton x y) (substrate r)). red. ir.
nin (doubleton_or H3). rw H4. app (inc_arg1_substrate H0).
rw H4. app (inc_arg2_substrate H0). cp (infimum_pr1 H H3 H2).
app (infimum_unique H H4 H1).
Qed.
Lemma sup_comparable1: forall r x y, order r -> gle r x y ->
sup r x y = y.
Proof. ir. cp (sup_comparable H0 H).
assert (has_supremum r (doubleton x y)). exists y. am.
uf inf. assert (sub (doubleton x y) (substrate r)). red. ir.
nin (doubleton_or H3). rw H4. app (inc_arg1_substrate H0).
rw H4. app (inc_arg2_substrate H0). cp (supremum_pr1 H H3 H2).
app (supremum_unique H H4 H1).
Qed.
Lemma total_order_lattice: forall r,
total_order r -> lattice r.
Proof. ir. red in H. ee. red. split. am. ir. nin (H0 _ _ H1 H2).
split. exists y. app sup_comparable. exists x. app inf_comparable.
rw doubleton_symm.
split. exists x. app sup_comparable. exists y. app inf_comparable.
Qed.
Lemma total_order_directed: forall r,
total_order r -> (right_directed r & left_directed r).
Proof. ir. app lattice_directed. app total_order_lattice. Qed.
Theorem total_order_monotone_injective: forall f r r',
total_order r -> strict_monotone_fun f r r' -> injective f.
Proof. ir. nin H0; red in H0; ee; red; split. am. ir.
wri H3 H6; wri H3 H7. nin (total_order_pr1 H H6 H7).
nin (H5 _ _ H9). contradiction. nin H9.
assert (glt r y x). red in H9. red. intuition. nin (H5 _ _ H10).
symmetry in H8. contradiction. am. am.
ir. wri H3 H6; wri H3 H7. nin (total_order_pr1 H H6 H7).
nin (H5 _ _ H9). contradiction. nin H9. assert (glt r y x). red in H9.
red. intuition. nin (H5 _ _ H10). symmetry in H8. contradiction. am.
Qed.
Lemma increasing_fun_from_strict: forall f r r',
strict_increasing_fun f r r' -> increasing_fun f r r'.
Proof. ir. red in H. red. eee. ir. nin (equal_or_not x y). rw H6. order_tac.
rw H3. assert (inc y (source f)). wr H2. order_tac. fprops.
ir. assert (glt r x y). split;am. nin (H4 _ _ H7). am.
Qed.
Lemma decreasing_fun_from_strict: forall f r r',
strict_decreasing_fun f r r' -> decreasing_fun f r r'.
Proof. ir. red in H. red. eee. ir. nin (equal_or_not x y). rw H6.
red. order_tac. rw H3. assert (inc y (source f)). wr H2. order_tac. fprops.
ir. assert (glt r x y). split;am. nin (H4 _ _ H7). am.
Qed.
Theorem total_order_increasing_morphism: forall f r r',
total_order r -> strict_increasing_fun f r r' -> order_morphism f r r'.
Proof. ir. red. assert (injective f).
apply total_order_monotone_injective with r r'. am. red. left. am.
cp (increasing_fun_from_strict H0).
red in H0. eee. red in H7. ir. red in H. ee.
red in H2. ee. clear H2; clear H11; clear H12; clear H13; clear H14.
rwi H5 H10. nin (H10 _ _ H8 H9). app iff_eq. ir. app H15. red in H2.
app iff_eq. ir. assert (x=y). order_tac. wr H12. order_tac.
rw H6. app inc_W_target. ir. cp (H15 _ _ H2).
assert (W x f = W y f). order_tac. red in H1;ee. rw (H14 _ _ H8 H9 H13).
order_tac. rww H5.
Qed.
Theorem sup_in_total_order:forall r X x, total_order r -> sub X (substrate r)->
least_upper_bound r X x = (upper_bound r X x &
(forall y, glt r y x -> exists z, inc z X & glt r y z & gle r z x)).
Proof. ir. assert (Ha: order r). nin H; am. app iff_eq.
ir. awi H1. ee. am. ir.
assert (~ (upper_bound r X y)). red. ir. cp (H2 _ H4). order_tac.
ufi upper_bound H4. assert (inc y (substrate r)). order_tac.
assert (exists z, inc z X & glt r y z).
app exists_proof. red. ir. elim H4. split. am. ir.
assert (inc y0 (substrate r)). app H0. nin (total_order_pr2 H H5 H8).
elim (H6 y0). intuition. am. nin H6. exists x0. eee.
red in H1. ee. app H8. am. am.
ir. ee. red. red. aw. split. Ztac. red in H1. ee.
am. ir. aw. Ztac. red in H5. ee. assert (inc x (substrate r)).
red in H1. ee. am. nin (total_order_pr2 H H5 H7).
cp (H2 _ H8). nin H9. ee. cp (H6 _ H9). order_tac. am.
Ztac. clear H3. Ztac. red in H1; ee. am. app Z_sub.
Qed.
Theorem inf_in_total_order:forall r X x, total_order r -> sub X (substrate r)->
greatest_lower_bound r X x = (lower_bound r X x &
(forall y, glt r x y -> exists z, inc z X & glt r z y & gle r x z)).
Proof. ir. assert (Ha: order r). nin H; am.
ap iff_eq. ir. awi H1. ee. am. ir.
assert (~ (lower_bound r X y)). red. ir. cp (H2 _ H4). order_tac.
ufi lower_bound H4. assert (inc y (substrate r)). order_tac.
assert (exists z, inc z X & glt r z y).
app exists_proof. red. ir. elim H4. split. am. ir.
assert (inc y0 (substrate r)). app H0. nin (total_order_pr2 H H8 H5).
elim (H6 y0). intuition. am. nin H6. ee. ex_tac. ee. am.
red in H1. eee. am. am.
ir. ee. red. red. aw. split. Ztac. red in H1. ee.
am. ir. aw. Ztac. red in H5. ee. assert (inc x (substrate r)).
red in H1. ee. am. nin (total_order_pr2 H H7 H5).
cp (H2 _ H8). nin H9. ee. cp (H6 _ H9). order_tac. am.
Ztac. clear H3. Ztac. red in H1; ee. am. app Z_sub.
Qed.
Definition interval_oo r a b :=Zo (substrate r)(fun z => glt r a z & glt r z b).
Definition interval_oc r a b :=Zo (substrate r)(fun z => glt r a z & gle r z b).
Definition interval_ou r a := Zo (substrate r)(fun z => glt r a z).
Definition interval_co r a b := Zo(substrate r)(fun z => gle r a z & glt r z b).
Definition interval_cc r a b := Zo(substrate r)(fun z => gle r a z & gle r z b).
Definition interval_cu r a := Zo (substrate r)(fun z => gle r a z).
Definition interval_uo r b := Zo (substrate r) (fun z => glt r z b).
Definition interval_uc r b := Zo (substrate r) (fun z => gle r z b).
Definition interval_uu r := Zo (substrate r) (fun z => True).
Definition is_closed_interval r x := exists a, exists b,
inc a (substrate r) & inc b (substrate r) & gle r a b & x = interval_cc r a b.
Definition is_open_interval r x := exists a, exists b,
inc a (substrate r) & inc b (substrate r) & gle r a b & x = interval_oo r a b.
Definition is_semi_open_interval r x := exists a, exists b,
inc a (substrate r) & inc b (substrate r) & gle r a b &
(x = interval_oc r a b \/ x = interval_co r a b).
Definition is_bounded_interval r x := is_closed_interval r x \/
is_open_interval r x \/ is_semi_open_interval r x.
Definition is_left_unbounded_interval r x :=
exists b, inc b (substrate r) & (x = interval_uc r b \/ x = interval_uo r b).
Definition is_right_unbounded_interval r x :=
exists a, inc a (substrate r) & (x = interval_cu r a \/ x = interval_ou r a).
Definition is_unbounded_interval r x :=
is_left_unbounded_interval r x \/ is_right_unbounded_interval r x \/
x = interval_uu r.
Definition is_interval r x :=
is_bounded_interval r x \/ is_unbounded_interval r x.
Ltac uf_interval :=
uf interval_cc; uf interval_oo; uf interval_co; uf interval_oc;
uf interval_uu; uf interval_uo; uf interval_ou;
uf interval_uc; uf interval_cu.
Lemma the_least_interval: forall r a b, order r ->
gle r a b -> the_least_element (induced_order r (interval_cc r a b)) = a.
Proof. ir. assert (sub (interval_cc r a b) (substrate r)). uf_interval.
app Z_sub. assert(inc a (substrate r)). app (inc_arg1_substrate H0).
assert (inc a (interval_cc r a b)). uf_interval. Ztac. ee.
order_tac. am.
app the_least_element_pr2. app order_induced_order. uf_interval.
red. aw. split. am. ir. aw. Ztac; intuition.
Qed.
Lemma the_greatest_interval: forall r a b, order r ->
gle r a b -> the_greatest_element (induced_order r (interval_cc r a b)) = b.
Proof. ir. assert (sub (interval_cc r a b) (substrate r)). uf_interval.
app Z_sub. assert(inc b (substrate r)). order_tac.
assert (inc b (interval_cc r a b)). uf_interval. Ztac. ee. am. order_tac.
app the_greatest_element_pr2. app order_induced_order. uf_interval.
red. aw. split. am. ir. aw. Ztac; intuition.
Qed.
Lemma nonempty_closed_interval: forall r x,
order r -> is_closed_interval r x -> nonempty x.
Proof. ir. nin H0. nin H0. ee. exists x0. rw H3. uf_interval. Ztac.
split. order_tac. am.
Qed.
Lemma singleton_interval: forall r a,
order r -> inc a (substrate r) -> is_singleton (interval_cc r a a).
Proof. ir. exists a. uf_interval. rw singleton_pr.
split;ir; Ztac; ee; order_tac.
Qed.
Lemma empty_interval: forall r a,
order r -> inc a (substrate r) ->
(empty (interval_co r a a) & empty (interval_oc r a a)&
empty (interval_oo r a a)).
Proof. ir. uf_interval. ee;red; ir; red; ir; Ztac; ee; order_tac.
Qed.
Ltac zztac:=
set_extens; Ztac; ee; match goal with H: inc _ (Zo _ _) |- _ => clear H end.
Ltac zztac2:= uf_interval; set_extens ;
[ match goal with H: inc _ (intersection2 _ _) |- _ =>
nin (intersection2_both H) end ;
match goal with
H1:(inc _ (Zo _ _)), H2 :(inc _ (Zo _ _)) |- _
=> nin (Z_all H1); nin (Z_all H2); clear H1; clear H2; ee
end; Ztac
|
Ztac; match goal with H: inc _ (Zo _ _) |- _ => clear H end;
app intersection2_inc; Ztac; uf glt;ee; try order_tac].
Lemma lattice_inverse: forall r, lattice r -> lattice (opposite_order r).
Proof. ir. red in H. ee. red. split. aw. fprops. aw. ir. cp (H0 _ _ H1 H2).
split. nin H3. nin H4. red. exists x0. wrr inf_sup_opp. app sub_doubleton.
nin H3. nin H3. red. exists x0. wrr sup_inf_opp. app sub_doubleton.
Qed.
Lemma intersection4: forall A B C D,
intersection2 (intersection2 A B) (intersection2 C D)
= intersection2 (intersection2 A C) (intersection2 B D).
Proof. ir. wr intersection2assoc. wr intersection2assoc. app uneq.
rw intersection2assoc. rw intersection2assoc.
rww (intersection2comm B C).
Qed.
Lemma intersection_i1: forall r x,
is_interval r x -> intersection2 x (interval_uu r) = x.
Proof. ir. assert (interval_uu r = substrate r). uf interval_uu.
ap extensionality. app Z_sub. red. ir. Ztac. rw H0.
assert (sub x (substrate r)).
nin H. nin H. nin H. nin H. ee. rw H3. uf_interval. app Z_sub.
nin H. nin H. nin H. nin H. ee. rw H3. uf_interval. app Z_sub.
nin H. nin H. ee. nin H3. rw H3. uf_interval. app Z_sub.
rw H3. uf_interval. app Z_sub.
nin H. nin H. nin H. nin H1. rw H1. uf_interval. app Z_sub.
rw H1. uf_interval. app Z_sub.
nin H. nin H. ee. nin H1. rw H1. uf_interval. app Z_sub.
rw H1. uf_interval. app Z_sub. rw H. rw H0. fprops.
app extensionality. ap intersection2sub_first. red. ir.
app intersection2_inc. app H1.
Qed.
Definition is_lu_interval r x :=
x = interval_uu r \/ is_left_unbounded_interval r x.
Definition is_ru_interval r x :=
x= interval_uu r \/ is_right_unbounded_interval r x.
Lemma intersection_i2: forall r x,
is_interval r x ->
(exists u, exists v, is_lu_interval r u & is_ru_interval r v &
intersection2 u v = x).
Proof. ir. assert (Ha:=H). nin H. nin H. nin H. nin H.
exists (interval_uc r x1). exists (interval_cu r x0). ee. right.
exists x1. au. right. exists x0. au.
rw H2. zztac2. am. am.
nin H. nin H. nin H. exists (interval_uo r x1). exists (interval_ou r x0).
ee. right. exists x1. au. right. exists x0. au.
rw H2. zztac2. nin H5; am. nin H3; am.
nin H. nin H. ee. nin H2.
exists (interval_uc r x1). exists (interval_ou r x0).
ee. right. exists x1. au. right. exists x0. au.
rw H2. zztac2. am. nin H3; am.
exists (interval_uo r x1). exists (interval_cu r x0).
ee. right. exists x1. au. right. exists x0. au.
rw H2. zztac2. nin H5; am. nin H5; am.
nin H. exists x; exists (interval_uu r). ee. red; au. red; au.
app intersection_i1. exists (interval_uu r). exists x. ee. left; tv.
nin H. right; tv. left; tv. rw intersection2comm. app intersection_i1.
Qed.
Lemma intersection_i3: forall r x y, lattice r ->
is_left_unbounded_interval r x -> is_left_unbounded_interval r y ->
is_left_unbounded_interval r (intersection2 x y).
Proof. ir. nin H0. nin H1. ee. cp (lattice_inf_pr H H0 H1). ee.
red in H. ee. clear H7.
set (u:=inf r x0 x1). red. exists u. split. order_tac.
nin H3; rw H3. nin H2; rw H2. left. zztac2.
nin (p_or_not_p (glt r u x1)). left. zztac2. nin H14. app H6.
red. ir. rwi H8 H10; order_tac. right; zztac2. split. nin H14;app H6.
red. ir. elim H7. wrr H9. nin H10; order_tac. nin H10; order_tac.
red. ir. rwi H8 H10. order_tac.
nin H2; rw H2. nin (p_or_not_p (glt r u x0)). left. zztac2. nin H12;app H6.
red. ir. wri H8 H7. order_tac. right. zztac2. split. nin H12; app H6.
red. ir. rwi H9 H12; contradiction. nin H10; order_tac. red. ir.
rwi H8 H10. order_tac. nin H10; order_tac.
nin (p_or_not_p (glt r u x0 & glt r u x1)). left. zztac2.
nin H12; nin H14; app H6. red. ir. rwi H11 H10; order_tac.
red. ir. rwi H11 H10; order_tac.
right. zztac2. split. nin H12; nin H14; app H6. red. ir. elim H7.
wr H9. intuition. nin H10; order_tac. red. ir. rwi H8 H10; order_tac.
nin H10; order_tac. red. ir. rwi H8 H10; order_tac.
Qed.
Theorem intersection_interval: forall r x y,
lattice r -> is_interval r x -> is_interval r y ->
is_interval r (intersection2 x y).
Proof. ir. cp (intersection_i2 H0). cp (intersection_i2 H1).
nin H2. nin H2. nin H3. nin H3. ee. wr H7; wr H5. rw intersection4.
assert (is_lu_interval r (intersection2 x0 x2)). nin H2. rw H2.
rw intersection2comm. rww intersection_i1. right. red. red in H3. intuition.
nin H3. rw H3. rww intersection_i1. red. right; am. right. left. am.
right. app intersection_i3.
assert (is_ru_interval r (intersection2 x1 x3)). nin H6. rw H6.
rw intersection2comm. rww intersection_i1. right. red. red in H4. intuition.
nin H4. rw H4. rww intersection_i1. red. right; am. right. right. left. am.
right. cp H. red in H. ee. clear H10.
assert (Ha: forall a, interval_cu r a = interval_uc (opposite_order r) a).
ir. uf_interval. aw. zztac. Ztac. aw. awii H12. Ztac.
assert (Hb: forall a, interval_ou r a = interval_uo (opposite_order r) a).
ir. uf_interval. uf glt. aw. zztac. aw. intuition. awii H12. int.
assert (is_left_unbounded_interval (opposite_order r) x1).
nin H6. nin H6. exists x4. split. aw. nin H10. wrr Ha.
left. am. right. wrr Hb.
assert (is_left_unbounded_interval (opposite_order r) x3).
nin H4. nin H4. exists x4. split. aw. nin H11. wrr Ha.
left. am. right. wrr Hb.
assert (lattice (opposite_order r)). app lattice_inverse.
cp (intersection_i3 H12 H10 H11). nin H13. ee. awi H13. wri Ha H14.
wri Hb H14. exists x4. split. am. am. am.
nin H8. rw H8. assert (is_interval r (intersection2 x1 x3)). right.
red in H9. red. intuition. rw intersection2comm. rww intersection_i1.
nin H9. rw H9. assert (is_interval r (intersection2 x0 x2)). right.
red. intuition. rww intersection_i1.
left. nin H8. nin H9. ee. nin H. clear H12.
nin (p_or_not_p (gle r x5 x4)). ir. nin H11;rw H11. nin H10; rw H10.
left. exists x5. exists x4. eee. zztac2. am. am.
right. right. exists x5. exists x4. eee. left. zztac2.
am. nin H13; am.
nin H10; rw H10. right. right. exists x5. exists x4. eee.
right. zztac2. nin H15; am. nin H15; am.
right. left. exists x5. exists x4. ee. am. am. am. zztac2. nin H15; am.
nin H13; am.
assert (empty (intersection2 (intersection2 x0 x2) (intersection2 x1 x3))).
red. ir. red. ir. elim H12.
assert (gle r y0 x4). cp (intersection2_first H13). nin H11. rwi H11 H14.
ufi interval_uc H14. Ztac. am. rwi H11 H14.
ufi interval_uo H14. Ztac. red in H16. ee. am.
assert (gle r x5 y0). cp (intersection2_second H13). nin H10. rwi H10 H15.
ufi interval_cu H15. Ztac. am. rwi H10 H15.
ufi interval_ou H15. Ztac. nin H17; am. order_tac.
cp (empty_interval H H8). ee. red. right. left.
exists x4. exists x4. ee. am. am. order_tac.
set_extens. elim (H13 x6). am. elim (H16 x6). am.
Qed.
End Border.
Export Border.