%------------------------------------------------------------------------------
% 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