-include "o-basic_pairs.ma".
-(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
-definition o_basic_pair_of_basic_pair: cic:/matita/formal_topology/basic_pairs/basic_pair.ind#xpointer(1/1) → basic_pair.
- intro;
- constructor 1;
- [ apply (SUBSETS (concr b));
- | apply (SUBSETS (form b));
- | apply (orelation_of_relation ?? (rel b)); ]
-qed.
-
-definition o_relation_pair_of_relation_pair:
- ∀BP1,BP2.cic:/matita/formal_topology/basic_pairs/relation_pair.ind#xpointer(1/1) BP1 BP2 →
- relation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2).
- intros;
- constructor 1;
- [ apply (orelation_of_relation ?? (r \sub \c));
- | apply (orelation_of_relation ?? (r \sub \f));
- |
- ]
-qed.
-