helm/software/matita/library/formal_topology/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 "formal_topology/basic_topologies.ma".
  16
  17 definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).
  18
  19 coercion btop_carr.
  20
  21 definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o.
  22
  23 coercion btop_carr'.
  24
  25 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
  26  intros; constructor 1;
  27   [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. 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]
  32 qed.
  33
  34 interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
  35
  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]
  40 qed.
  41
  42 interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
  43
  44 record formal_topology: Type ≝
  45  { bt:> BTop;
  46    converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
  47  }.
  48
  49 definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
  50
  51 coercion bt'.
  52
  53 definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
  54  intros; constructor 1;
  55   [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
  56   | intros; apply (.= (†H)‡(†H1)); apply refl1]
  57 qed.
  58
  59 interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
  60
  61 record formal_map (S,T: formal_topology) : Type ≝
  62  { cr:> continuous_relation S T;
  63    C1: ∀b,c. extS ?? cr (b ↓ c) = (ext ?? cr b) ↓ (ext ?? cr c);
  64    C2: extS ?? cr T = S
  65  }.