Impressum topology.pvs

%------------------------------------------------------------------------------
% Topology
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            8/10/04  Initial Version
%     Version 1.1            1/11/06  Basis material moved to basis.pvs
%     Version 1.2            6/8/06   open/closed defs & Type Judgements added
%------------------------------------------------------------------------------

topology[T:TYPE, (IMPORTING topology_def[T]) S:topology]: THEORY

BEGIN

  IMPORTING prelude_sets_aux[T],
            topology_prelim[T]

  AUTO_REWRITE+  member

  x:       VAR T
  A,B:     VAR set[T]

  open?(A)   : bool = member(A,S)
  closed?(A) : bool = member(complement(A),S)
  clopen?(A) : bool = closed?(A) AND open?(A)
  compact?(A): bool = compact_subset?(S,A)

  open_set:   TYPE+ = (open?)   CONTAINING emptyset[T]
  closed_set: TYPE+ = (closed?) CONTAINING emptyset[T]
  clopen_set: TYPE+ = (clopen?) CONTAINING emptyset[T]

  open:    TYPE+ = (open?)    CONTAINING emptyset[T]
  closed:  TYPE+ = (closed?)  CONTAINING emptyset[T]
  clopen:  TYPE+ = (clopen?)  CONTAINING emptyset[T]
  compact: TYPE+ = (compact?) CONTAINING emptyset[T]

  open_set_is_open:     JUDGEMENT open_set   SUBTYPE_OF open
  closed_set_is_closed: JUDGEMENT closed_set SUBTYPE_OF closed
  clopen_set_is_open:   JUDGEMENT clopen_set SUBTYPE_OF open
  clopen_set_is_closed: JUDGEMENT clopen_set SUBTYPE_OF closed
  open_is_open_set:     JUDGEMENT open       SUBTYPE_OF open_set
  closed_is_closed_set: JUDGEMENT closed     SUBTYPE_OF closed_set
  clopen_is_open_set:   JUDGEMENT clopen     SUBTYPE_OF open_set
  clopen_is_closed_set: JUDGEMENT clopen     SUBTYPE_OF closed_set

  U,U1,U2: VAR open
  V,V1,V2: VAR closed
  C1,C2:   VAR compact
  Y,Y1,Y2: VAR setofsets[T]

  interior_point?(x,A): bool = EXISTS U: subset?(U,A) AND member(x,U)
  neighbourhood?(A,x) : bool = interior_point?(x,A)
  adherent_point?(x,A): bool = FORALL U: neighbourhood?(U,x) =>
                                         nonempty?(intersection(U,A))
  limit_point?(x,A)   : bool = adherent_point?(x,A) AND NOT member(x,A)

  interior(A)         : set[T] = {x:(A) | interior_point?(x,A)}
  Cl(A)               : set[T] = {x | adherent_point?(x,A)}
  derived_set(A)      : set[T] = {x | limit_point?(x,A)}

  open_complement:     LEMMA open?(complement(A))   IFF closed?(A)
  closed_complement:   LEMMA closed?(complement(A)) IFF open?(A)

  open_emptyset:       LEMMA open?(emptyset[T])
  open_fullset:        LEMMA open?(fullset[T])
  open_Union:          LEMMA every(open?,Y) => open?(Union(Y))
  open_union:          LEMMA open?(union(U1,U2))
  open_intersection:   LEMMA open?(intersection(U1,U2))
  open_Intersection:   LEMMA is_finite(Y) AND every(open?,Y) =>
                             open?(Intersection(Y))
  closed_emptyset:     LEMMA closed?(emptyset[T])
  closed_fullset:      LEMMA closed?(fullset[T])
  closed_Intersection: LEMMA every(closed?,Y) => closed?(Intersection(Y))
  closed_intersection: LEMMA closed?(intersection(V1,V2))
  closed_union:        LEMMA closed?(union(V1,V2))
  closed_Union:        LEMMA is_finite(Y) AND every(closed?,Y) =>
                             closed?(Union(Y))

  complement_open_is_closed: JUDGEMENT complement(U)       HAS_TYPE closed
  complement_closed_is_open: JUDGEMENT complement(V)       HAS_TYPE open

  emptyset_is_open:          JUDGEMENT emptyset[T]         HAS_TYPE open
  fullset_is_open:           JUDGEMENT fullset[T]          HAS_TYPE open
  union_is_open:             JUDGEMENT union(U1,U2)        HAS_TYPE open
  intersection_is_open:      JUDGEMENT intersection(U1,U2) HAS_TYPE open

  emptyset_is_closed:        JUDGEMENT emptyset[T]         HAS_TYPE closed
  fullset_is_closed:         JUDGEMENT fullset[T]          HAS_TYPE closed
  union_is_closed:           JUDGEMENT union(V1,V2)        HAS_TYPE closed
  intersection_is_closed:    JUDGEMENT intersection(V1,V2) HAS_TYPE closed

  emptyset_is_clopen:          JUDGEMENT emptyset[T]       HAS_TYPE clopen
  fullset_is_clopen:           JUDGEMENT fullset[T]        HAS_TYPE clopen

  t: VAR topology[T]

  indiscrete_subset: LEMMA subset?(indiscrete_topology,t)
  discrete_subset:   LEMMA subset?(t,discrete_topology)

  open_def:          LEMMA open?(A) IFF FORALL (x:(A)): neighbourhood?(A,x)
  neighbourhood_intersection: LEMMA neighbourhood?(A,x) AND neighbourhood?(B,x)
                                    => neighbourhood?(intersection(A,B),x)
  neighbourhood_subset: LEMMA neighbourhood?(A,x) AND subset?(A,B) =>
                              neighbourhood?(B,x)
  Cl_split1:      LEMMA union(derived_set(A),A) = Cl(A)
  Cl_split2:      LEMMA disjoint?(derived_set(A),A)

  subset_of_Cl    : LEMMA subset?(A,Cl(A))                            % 3.7.15a
  Cl_subset       : LEMMA subset?(A,B) => subset?(Cl(A),Cl(B))        % 3.7.15b
  Cl_idempotent   : LEMMA Cl(Cl(A)) = Cl(A)                           % 3.7.15c
  eq_Cl_is_closed : LEMMA A = Cl(A) IFF closed?(A)
  Cl_closed       : LEMMA closed?(Cl(A))                              % 3.7.15d
  Cl_subset_closed: LEMMA subset?(A,V) => subset?(Cl(A),V)
  Cl_union        : LEMMA Cl(union(A,B)) = union(Cl(A),Cl(B))
  Cl_Union        : LEMMA is_finite(Y) => Cl(Union(Y)) = Union(image(Cl,Y))
                                                                      % 3.7.18
  Cl_Intersection: LEMMA subset?(Cl(Intersection(Y)),Intersection(image(Cl,Y)))
                                                                      % 3.7.17

  open_difference  : LEMMA open?(difference(U,V))
  closed_difference: LEMMA closed?(difference(V,U))

  Cl_is_closed:               JUDGEMENT Cl(A)           HAS_TYPE closed
  open_diff_closed_is_open:   JUDGEMENT difference(U,V) HAS_TYPE open
  closed_diff_open_is_closed: JUDGEMENT difference(V,U) HAS_TYPE closed

  emptyset_is_compact:        JUDGEMENT emptyset[T]         HAS_TYPE compact
  singleton_is_compact:       JUDGEMENT singleton(x)        HAS_TYPE compact
  union_is_compact:           JUDGEMENT union(C1,C2)        HAS_TYPE compact
  finite_is_compact:          JUDGEMENT finite_set[T]     SUBTYPE_OF compact

  compact_Union: LEMMA is_finite(Y) AND every(compact?,Y) => compact?(Union(Y))

  compact_def: LEMMA
     compact_space?(S) IFF
     FORALL Y: (every(closed?,Y)    AND
                (FORALL Y1: subset?(Y1,Y) AND is_finite(Y1) =>
                                   nonempty?(Intersection(Y1)))) =>
               nonempty?(Intersection(Y))

END topology