|
metric_space_real_fun[T:TYPE+,d:[T,T->nnreal]]: THEORY
%------------------------------------------------------------------------------
% This Theory Contains Standard Lemmas About Real-Valued Continuous Functions
% On An Arbitrary Metric Space
%
% Authors: Anthony Narkawicz, NASA Langley
%
% Version 1.0 8/31/2009 Initial Version
%------------------------------------------------------------------------------
BEGIN
ASSUMING IMPORTING metric_spaces_def[T,d]
fullset_metric_space: ASSUMPTION metric_space?[T,d](fullset[T])
ENDASSUMING
S: VAR set[T]
IMPORTING real_metric_space, continuity_ms_def[T,d,real,real_dist], reals@abs_lems
f,g: VAR [T -> real]
c: VAR real
scal_continuous: LEMMA continuous?(f,S) IMPLIES continuous?(c* f, S)
neg_continuous: LEMMA continuous?(f,S) IMPLIES continuous?( -f,S)
sum_continuous: LEMMA continuous?(f,S) AND continuous?(g,S) IMPLIES
continuous?(f+g,S)
diff_continuous: LEMMA continuous?(f,S) AND continuous?(g,S) IMPLIES
continuous?(f-g,S)
prod_continuous: LEMMA continuous?(f,S) AND continuous?(g,S) IMPLIES
continuous?(f*g,S)
abs_comp_cont: LEMMA continuous?(f,S) IMPLIES continuous?(abs(f),S)
END metric_space_real_fun
¤ Dauer der Verarbeitung: 0.15 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.
|
