Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig_fnd/ (Beweissystem der NASA Version 6.0.9^©)

Quelle metric_space_real_fun.pvs Sprache: PVS

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

quality97%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.