matita/matita/lib/formal_topology/o-formal_topologies.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basics/core_notation/fintersects_2.ma".
  16 include "basics/core_notation/downarrow_1.ma".
  17 include "formal_topology/o-basic_topologies.ma".
  18 (*
  19 (*
  20 (*
  21 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
  22  intros; constructor 1;
  23   [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
  24     intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
  25     split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
  26   | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
  27     try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
  28 qed.
  29
  30 interpretation "downarrow" 'downarrow a = (fun_1 ?? (downarrow ?) a).
  31
  32 definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
  33  intros; constructor 1;
  34   [ apply (λU,V. ↓U ∩ ↓V);
  35   | intros; apply (.= (†H)‡(†H1)); apply refl1]
  36 qed.
  37
  38 interpretation "ffintersects" 'fintersects U V = (fun1 ??? (ffintersects ?) U V).
  39 *)
  40
  41 record formal_topology: Type ≝
  42  { bt:> OBTop;
  43    converges: ∀U,V: bt. oA bt (U ↓ V) = (oA ? U ∧ oA ? V)
  44  }.
  45
  46 (*
  47
  48 definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
  49  intros; constructor 1;
  50   [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
  51   | intros; apply (.= (†H)‡(†H1)); apply refl1]
  52 qed.
  53
  54 interpretation "ffintersects'" 'fintersects U V = (fun1 ??? (ffintersects' ?) U V).
  55 *)
  56 record formal_map (S,T: formal_topology) : Type ≝
  57  { cr:> continuous_relation_setoid S T;
  58    C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
  59    C2: extS ?? cr T = S
  60  }.
  61
  62 definition formal_map_setoid: formal_topology → formal_topology → setoid1.
  63  intros (S T); constructor 1;
  64   [ apply (formal_map S T);
  65   | constructor 1;
  66      [ apply (λf,f1: formal_map S T.f=f1);
  67      | simplify; intros 1; apply refl1
  68      | simplify; intros 2; apply sym1
  69      | simplify; intros 3; apply trans1]]
  70 qed.
  71
  72 axiom C1':
  73  ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
  74   extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
  75
  76 definition formal_map_composition:
  77  ∀o1,o2,o3: formal_topology.
  78   binary_morphism1
  79    (formal_map_setoid o1 o2)
  80    (formal_map_setoid o2 o3)
  81    (formal_map_setoid o1 o3).
  82  intros; constructor 1;
  83   [ intros; whd in c c1; constructor 1;
  84      [ apply (comp1 BTop ??? c c1);
  85      | intros;
  86        apply (.= (extS_com ??? c c1 ?));
  87        apply (.= †(C1 ?????));
  88        apply (.= (C1' ?????));
  89        apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
  90        apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
  91        apply (.= (extS_singleton ????)‡(extS_singleton ????));
  92        apply refl1;
  93      | apply (.= (extS_com ??? c c1 ?));
  94        apply (.= (†(C2 ???)));
  95        apply (.= (C2 ???));
  96        apply refl1;]
  97   | intros; simplify;
  98     change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
  99     apply prop1; assumption]
 100 qed.
 101 *)
 102 *)