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_topologies.ma".
16 include "o-basic_topologies.ma".
17 include "relations_to_o-algebra.ma".
19 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
20 definition o_basic_topology_of_basic_topology: cic:/matita/formal_topology/basic_topologies/basic_topology.ind#xpointer(1/1) → basic_topology.
23 [ apply (SUBSETS (carrbt b));
26 | apply (A_is_saturation b);
27 | apply (J_is_reduction b);
28 | apply (compatibility b); ]
31 definition o_relation_pair_of_relation_pair:
32 ∀S,T.cic:/matita/formal_topology/basic_topologies/continuous_relation.ind#xpointer(1/1) S T →
33 continuous_relation (o_basic_topology_of_basic_topology S) (o_basic_topology_of_basic_topology T).
36 [ apply (orelation_of_relation ?? (cont_rel ?? c));
37 | apply (reduced ?? c);
38 | apply (saturated ?? c); ]