1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_pairs_to_o-basic_pairs.ma".
16 include "o-basic_pairs_to_o-basic_topologies.ma".
17 include "basic_pairs.ma".
18 include "basic_topologies.ma".
20 definition basic_topology_of_basic_pair: basic_pair → basic_topology.
22 letin obp ≝ (o_basic_pair_of_basic_pair bp);
23 letin obt ≝ (o_basic_topology_of_o_basic_pair obp);
28 | apply (oA_is_saturation obt);
29 | apply (oJ_is_reduction obt);
30 | apply (Ocompatibility obt); ]
33 definition continuous_relation_of_relation_pair:
34 ∀BP1,BP2.relation_pair BP1 BP2 →
35 continuous_relation (basic_topology_of_basic_pair BP1) (basic_topology_of_basic_pair BP2).
37 letin orp ≝ (o_relation_pair_of_relation_pair ?? rp);
38 letin ocr ≝ (o_continuous_relation_of_o_relation_pair ?? orp);
41 | apply (Oreduced ?? ocr);
42 | apply (Osaturated ?? ocr); ]