|
%------------------------------------------------------------------------------
% The Inverse Of A Continuous Function (on a metric space) is Continuous
%
% Author: Anthony Narkawicz, NASA Langley
%
% Version 1.0 10/27/09 Initial Version
%------------------------------------------------------------------------------
inverse_fun_ms_continuous[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 uniform_continuity[T1,d1,T2,d2], continuity_ms[T2,d2,T1,d1]
image_function_continuous: THEOREM FORALL (f:[T1->T2]):
continuous?(f) AND compact?(fullset[T1]) AND bijective?(f)
IMPLIES
continuous?(inverse(f))
END inverse_fun_ms_continuous
¤ Dauer der Verarbeitung: 0.0 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.
|
