|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
