Definition of formal_topologies.

diff --git a/helm/software/matita/library/formal_topology/formal_topologies.ma b/helm/software/matita/library/formal_topology/formal_topologies.ma
new file mode 100644 (file)
index 0000000..e29ba16
--- /dev/null
+++ b/helm/software/matita/library/formal_topology/formal_topologies.ma
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "formal_topology/basic_topologies.ma".
+
+definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).
+
+coercion btop_carr.
+
+definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o.
+
+coercion btop_carr'.
+
+definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
+ intros; constructor 1;
+  [ apply (λU:Ω \sup S.{a | ∃b. b ∈ U ∧ a ∈ A ? (singleton ? b)});
+    intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
+    split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
+  | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
+    try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
+qed.
+
+interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
+
+definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
+ intros; constructor 1;
+  [ apply (λU,V. ↓U ∩ ↓V);
+  | intros; apply (.= (†H)‡(†H1)); apply refl1]
+qed.
+
+interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
+
+record formal_topology : Type ≝
+ { bt:> BTop;
+   converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
+ }.
\ No newline at end of file