| products/sources/formale Sprachen/PVS/topology/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: topology.pvs Sprache: PVSOriginal von: 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 ¤ Dauer der Verarbeitung: 0.18 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.Bot Zugriff |
