Quelle topology_prelim.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Topology prelim file
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Version 1.0            8/7/04   Initial Version
%     Version 1.1            1/12/06  Basis material moved to basis.pvs (DRL)
%------------------------------------------------------------------------------

topology_prelim[T:TYPE]: THEORY

BEGIN

  AUTO_REWRITE+  member

  x,y:   VAR T
  A,B:   VAR set[T]
  S,U,V: VAR setofsets[T]

  topology_empty?(S):       bool = member(emptyset[T],S)
  topology_full?(S):        bool = member(fullset[T], S)
  topology_Union?(S):       bool = FORALL U: subset?(U,S) =>
                                                     member(Union(U),S)
  topology_intersection?(S):bool = FORALL (A,B:(S)):member(intersection(A,B),S)

% The following is Sutherland Definition 3.1.1 (except we've permitted
% the type T to be empty).

  topology?(S):bool = topology_empty?(S) AND topology_full?(S)         AND
                      topology_Union?(S) AND topology_intersection?(S)
                                                                    % Def 3.1.1

  discrete_topology_set  : setofsets[T] = powerset(fullset[T])
  indiscrete_topology_set: setofsets[T] = {A | empty?(A) OR full?(A)}

  discrete_topology_lem  : LEMMA topology?(discrete_topology_set)   % Ex  3.1.4
  indiscrete_topology_lem: LEMMA topology?(indiscrete_topology_set) % Ex  3.1.6

  topology: TYPE+ = (topology?) CONTAINING discrete_topology_set

  discrete_topology  : topology = discrete_topology_set
  indiscrete_topology: topology = indiscrete_topology_set

% We now define some common separation conditions for topologies.
% The important one is T2 (or Hausdorff); motto:
%   "In a Hausdorff Space, every point can be housed off from every
%    other point by disjoint open sets."

  is_T0?(S):bool = FORALL x,y: x /= y => EXISTS (U:(S)):
                          (member(x,U) AND NOT member(y,U)) OR
                          (member(y,U) AND NOT member(x,U))

  is_T1?(S):bool = FORALL x,y: x /= y => EXISTS (U:(S)):
                          (member(x,U) AND NOT member(y,U))

  is_T2?(S):bool = FORALL x,y: x /= y => EXISTS (U,V:(S)):
                          disjoint?(U,V) AND member(x,U) AND member(y,V)

  hausdorff?(S):bool = is_T2?(S)                                    % Def 4.2.1

  T0_space?(S):bool        = topology?(S) AND is_T0?(S)
  T1_space?(S):bool        = topology?(S) AND is_T1?(S)
  T2_space?(S):bool        = topology?(S) AND is_T2?(S)
  hausdorff_space?(S):bool = topology?(S) AND hausdorff?(S)

  T0_topology: TYPE+ = (T0_space?)        CONTAINING discrete_topology
  T1_topology: TYPE+ = (T1_space?)        CONTAINING discrete_topology
  T2_topology: TYPE+ = (T2_space?)        CONTAINING discrete_topology
  hausdorff:   TYPE+ = (hausdorff_space?) CONTAINING discrete_topology

  T0_is_topology:  JUDGEMENT T1_topology SUBTYPE_OF topology
  T1_is_T0:        JUDGEMENT T1_topology SUBTYPE_OF T0_topology
  T2_is_T1:        JUDGEMENT T2_topology SUBTYPE_OF T1_topology
  hausdorff_is_T2: JUDGEMENT hausdorff   SUBTYPE_OF T2_topology
  T2_is_hausdorff: JUDGEMENT T2_topology SUBTYPE_OF hausdorff

% We now define compactness. Motto:
%   "If a city is compact, it can be guarded by a finite number of
%    arbitrarily short-sighted policemen."                  H Weyl.

  cover?(U,A)        : bool = subset?(A,Union(U))                   % Def 5.2.1
  finite_cover?(U,A) : bool = is_finite(U) AND cover?(U,A)          % Def 5.2.1
  subcover?(V,U,A)   : bool = cover?(U,A) AND cover?(V,A) AND
                              subset?(V,U)                          % Def 5.2.1
  open_cover?(U,A,S) : bool = subset?(U,S) AND cover?(U,A)          % Def 5.2.1

  compact_subset?(S,A):bool = FORALL U: open_cover?(U,A,S) =>       % Def 5.2.2
                              EXISTS V: subset?(V,U) AND finite_cover?(V,A)

  compact_space?(S): bool = topology?(S) AND compact_subset?(S,Union(S))

  compact_hausdorff?(S): bool = hausdorff?(S) AND compact_space?(S)

  compact_space:     TYPE+ = (compact_space?) CONTAINING indiscrete_topology
  compact_hausdorff: TYPE  = (compact_hausdorff?)

  compact_space_is_topology: JUDGEMENT compact_space     SUBTYPE_OF topology
  compact_hausdorff_is_topology:
                             JUDGEMENT compact_hausdorff SUBTYPE_OF topology
  compact_hausdorff_is_hausdorff:
                             JUDGEMENT compact_hausdorff SUBTYPE_OF hausdorff
  compact_hausdorff_is_compact_space:
                           JUDGEMENT compact_hausdorff SUBTYPE_OF compact_space

  connected?(S): bool = FORALL (A:(S)): S(complement(A)) =>
                               (A = emptyset[T] OR A = fullset[T])  % Def 6.2.4

  connected_space?(S): bool = topology?(S) AND connected?(S)

  connected_space: TYPE+ = (connected_space?) CONTAINING indiscrete_topology

  connected_space_is_topology: JUDGEMENT connected_space SUBTYPE_OF topology

END topology_prelim

quality81%

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.