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 "formal_topology/basic_topologies.ma".
17 definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).
21 definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o.
25 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
26 intros; constructor 1;
27 [ apply (λU:Ω \sup S.{a | ∃b. b ∈ U ∧ a ∈ A ? (singleton ? b)});
28 intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
29 split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
30 | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
31 try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
34 interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
36 definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
37 intros; constructor 1;
38 [ apply (λU,V. ↓U ∩ ↓V);
39 | intros; apply (.= (†H)‡(†H1)); apply refl1]
42 interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
44 record formal_topology : Type ≝
46 converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V