|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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
¤ Dauer der Verarbeitung: 0.16 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.
|
