Quelle  restriction_cont_fun.pvs

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Restriction of continuous functions  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

restriction_cont_fun[T1, T2 : TYPE FROM real] : theory
BEGIN

  ASSUMING

  sub_domain : ASSUMPTION
 FORALL (x : T1) : EXISTS (y : T2) : x = y

  ENDASSUMING

  IMPORTING continuous_functions

  f : VAR [T2 -> real]

  sub_dom : LEMMA FORALL (u : T1) : T2_pred(u)

  restrict2(f) : [T1 -> real] = LAMBDA (u : T1) : f(u)

  CONVERSION restrict2

  restrict_cont_fun : LEMMA
 continuous?(f) IMPLIES continuous?[T1](f) 

END restriction_cont_fun