matita/contribs/dama/dama/classical_pointwise/topology.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
  16
  17 include "classical_pointwise/sets.ma".
  18
  19 record is_topology (X) (A: set X) (O: set (set X)) : Prop  ≝
  20  { top_subset: ∀B. B ∈ O → B ⊆ A;
  21    top_empty: ∅︀ ∈ O;
  22    top_full: A ∈ O;
  23    top_intersection: ∀B,C. B ∈ O → C ∈ O → B ∩ C ∈ O;
  24    top_countable_union:
  25      ∀B.(∀i.(B \sub i) ∈ O) → (∪ \sub i (B \sub i)) ∈ O
  26  }.
  27
  28 record topological_space : Type ≝
  29  { top_carrier:> Type;
  30    top_domain:> set top_carrier;
  31    O: set (set top_carrier);
  32    top_is_topological_space:> is_topology ? top_domain O
  33  }.
  34
  35 (*definition is_continuous_map ≝
  36  λX,Y: topological_space.λf: X → Y.
  37   ∀V. V ∈ O Y → (f \sup -1) V ∈ O X.*)
  38 definition is_continuous_map ≝
  39  λX,Y: topological_space.λf: X → Y.
  40   ∀V. V ∈ O Y → inverse_image ? ? f V ∈ O X.
  41
  42 record continuous_map (X,Y: topological_space) : Type ≝
  43  { cm_f:> X → Y;
  44    cm_is_continuous_map: is_continuous_map ? ? cm_f
  45  }.