| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 939 B |
|
Quelle composition_continuous.pvs Sprache: PVS |
|||||||||
|
composition_continuous [ T1, T2 : TYPE FROM real ] : THEORY
%---------------------------------------------------------------------------- % Composition of continuous functions % % Author: Bruno Dutertre Royal Holloway & Bedford New College %---------------------------------------------------------------------------- BEGIN IMPORTING continuous_functions, reals@real_fun_props f : VAR [T1 -> T2] g : VAR [T2 -> real] x0 : VAR T1 F : VAR { E : setof[real] | subset?(E, T1_pred) } composition_cont : LEMMA continuous?(f, x0) AND continuous?(g, f(x0)) IMPLIES continuous?(g o f, x0) composition_cont_set : LEMMA continuous_on?(f, F) AND continuous_on?(g, Im(f, F)) IMPLIES continuous_on?(g o f, F) composition_cont_fun : LEMMA continuous?(f) AND continuous?(g) IMPLIES continuous?(g o f) END composition_continuous ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28