|
%------------------------------------------------------------------------------
% Continuity over Metric Spaces
%
% Author: David Lester, Manchester University & NIA
% Anthony Narkawicz, NASA Langley
% Ricky Butler, NASA Langley
%
%
% Version 1.0 5/12/04 Initial Version
%------------------------------------------------------------------------------
continuity_ms[T1:Type+,d1:[T1,T1->nnreal],
T2:Type+,d2:[T2,T2->nnreal]]: THEORY
BEGIN
ASSUMING IMPORTING metric_spaces
fullset_metric_space1: ASSUMPTION metric_space?[T1,d1](fullset[T1])
fullset_metric_space2: ASSUMPTION metric_space?[T2,d2](fullset[T2])
ENDASSUMING
IMPORTING continuity_ms_def[T1,d1,T2,d2], compactness[T1,d1]
X,S: VAR set[T1]
Y,T: VAR set[T2]
% Theorem 4.22a
image_inverse_image: THEOREM FORALL (f:[(S)->(T)]):
subset?(X,S) AND subset?(Y,T) AND
X = inverse_image(f,Y) IMPLIES subset?(image(f,X),Y)
% Theorem 4.22b
inverse_image_image: THEOREM FORALL (f:[(S)->(T)]):
subset?(X,S) AND subset?(Y,T) AND
Y = image(f,X) IMPLIES subset?(X,inverse_image(f,Y))
% Theorem 4.23
continuous_open_sets: THEOREM FORALL (f:[T1->T2]):
continuous?(f,(S)) IFF
(Forall Y: open?[T2,d2](Y) IMPLIES open_in?[T1,d1](intersection(inverse_image(f,Y),S),S))
% Theorem 4.24
continuous_closed_sets: THEOREM FORALL (f:[T1->T2]):
continuous?(f,(S)) IFF
(FORALL Y: closed?[T2,d2](Y) IMPLIES closed_in?[T1,d1](intersection(inverse_image(f,Y),S),S))
END continuity_ms
[ Konzepte0.15Was zu einem Entwurf gehört
Wie die Entwicklung von Software durchgeführt wird
]
|
