|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.19 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.
|
