|
%------------------------------------------------------------------------------
% Metric spaces definition file
%
% Authors: David Lester, Manchester University & NIA
% Anthony Narkawicz, NASA Langley
% Ricky Butler, NASA Langley
%
% Version 1.0 5/12/04 Initial Version
% Version 1.1 8/18/09
%------------------------------------------------------------------------------
metric_spaces[T:TYPE+,d:[T,T->nnreal]]: THEORY
BEGIN
ASSUMING IMPORTING metric_spaces_def[T,d]
% metric_zero : ASSUMPTION FORALL (x,y: T): d(x,y) = 0 IFF x = y
% metric_symmetric: ASSUMPTION FORALL (x,y: T): d(x,y) = d(y,x)
% metric_triangle : ASSUMPTION FORALL (x,y,z: T): d(x,z) <= d(x,y) + d(y,z)
fullset_metric_space: ASSUMPTION metric_space?[T,d](fullset[T])
ENDASSUMING
IMPORTING prelude_sets_aux
AUTO_REWRITE+ member
AUTO_REWRITE+ complement_complement
AUTO_REWRITE+ Complement_Complement
metric_space: TYPE+ = set[T]
r: VAR posreal
x,y,z: VAR T
S,U: VAR set[T]
ball(x,r): set[T] = {y | d(x,y) < r}
interior_point?(x,S): bool = EXISTS r: subset?(ball(x,r),S)
interior(S): set[T] = {x:T | interior_point?(x,S) and S(x)}
open?(S): bool = interior(S) = S
open_in?(S,U): bool = (FORALL (s: (S)): EXISTS r: subset?(intersection(ball(s,r),U),S))
AND subset?(S,U)
closed_in?(S,U): bool = open_in?(intersection(complement(S),U),U) AND subset?(S,U)
closed?(S): bool = open?(complement(S))
adherent_point?(x,S): bool = FORALL r: nonempty?(intersection(S,ball(x,r)))
limit_point?(S)(x): bool = adherent_point?(x,S) AND NOT member(x,S)
metric_closure(S): set[T] = {x:T | adherent_point?(x,S)}
open_set: TYPE = (open?)
closed_set: TYPE = (closed?)
open_set_is_set: JUDGEMENT open_set SUBTYPE_OF set[T]
closed_set_is_set: JUDGEMENT closed_set SUBTYPE_OF set[T]
X: VAR metric_space
A,B: VAR set[T]
% Mundane properties of open and closed sets
open_emptyset: LEMMA open?(emptyset)
closed_emptyset: LEMMA closed?(emptyset)
complement_open: LEMMA open?(A) IFF closed?(complement(A))
complement_closed: LEMMA closed?(A) IFF open?(complement(A))
open_fullset: LEMMA open?(fullset)
closed_fullset: LEMMA closed?(fullset)
open_in_fullset: LEMMA open?(A) IFF open_in?(A,fullset[T])
closed_in_fullset: LEMMA closed?(A) IFF closed_in?(A,fullset[T])
ball_open: LEMMA open?(ball(x, r))
Complement_open: LEMMA FORALL (XS:set[open_set]):
every(closed?)(Complement(XS))
Complement_closed: LEMMA FORALL (XS:set[closed_set]):
every(open?)(Complement(XS))
subset_is_metric_space: LEMMA subset?(S,X) IMPLIES metric_space?(S)
% Apostol 3.35a (1) (equivalent to Apostol 3.7 (generalized))
% The union of any _collection_ of open sets is open
open_Union_open: THEOREM FORALL (XS:set[open_set]): open?(Union(XS))
% Apostol 3.35a (2) (equivalent to Apostol 3.8 (generalized))
% The intersection of any _finite_set_ of open sets is open
open_Intersection_open: THEOREM
FORALL (FS:finite_set[open_set]): open?(Intersection(FS))
% Apostol 3.35b (1) (equivalent to Apostol 3.7 (generalized))
% The union of any _finite_set_ of closed sets is closed
closed_Union_closed: THEOREM
FORALL (FS:finite_set[closed_set]): closed?(Union(FS))
% Apostol 3.35b (2) (equivalent to Apostol 3.8 (generalized))
% The union of any _collection_ of closed sets is closed
closed_Intersection_closed: THEOREM
FORALL (XS:set[closed_set]): closed?(Intersection(XS))
% Apostol 3.36a
open_closed_difference: LEMMA FORALL (A:open_set,B:closed_set):
open?(difference(A,B))
% Apostol 3.36b
closed_open_difference: LEMMA FORALL (A:open_set,B:closed_set):
closed?(difference(B,A))
% Apostol Theorem 3.33
open_def: THEOREM subset?(S,X) AND subset?(A,S) IMPLIES
(open?(A) IFF (EXISTS B: subset?(B,S) AND open?(B) AND A = intersection(B,S)))
END metric_spaces
¤ Dauer der Verarbeitung: 0.1 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.
|
