| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 64 kB |
|
Nach dem Mausklick ist die Projektion eines vierdimensionalen Würfels zu sehen unif_cont_fun.pvs Sprache: PVS |
|||||||||
|
unif_cont_fun [ T : TYPE FROM real ] : THEORY
%---------------------------------------------------------------------------- % % Additions made by Ricky W. Butler NASA Langley % %---------------------------------------------------------------------------- BEGIN ASSUMING IMPORTING deriv_domain_def connected_domain : ASSUMPTION connected?[T] not_one_element : ASSUMPTION not_one_element?[T] ENDASSUMING IMPORTING continuous_functions[T], convergence_sequences f, f1, f2 : VAR [T -> real] g : VAR [T -> nzreal] u : VAR real x, x0 : VAR T epsi, delta : VAR posreal %%% E : VAR { S : setof[real] | subset?(S, T_pred) } E : VAR setof[T] uniformly_continuous?(f, E) : bool = FORALL (epsi: posreal): EXISTS (delta: posreal): FORALL (x,y: (E)): abs(x-y) < delta IMPLIES abs(f(x) - f(y)) < epsi P3: VAR [real,real,posnat -> bool] getem_scaf4: LEMMA (FORALL (n: posnat): EXISTS (x,y: real): P3(x,y,n)) IMPLIES (EXISTS (XX,YY: [posnat -> real]): FORALL (k: posnat): P3(XX(k),YY(k),k)) a,b,c: VAR T unif_cont_interval: LEMMA a < b IMPLIES LET D = {xx:T | a <= xx AND xx <= b} IN continuous_on?(f,D) IMPLIES uniformly_continuous?(f,D) END unif_cont_fun ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28