| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle cross_metric_cont.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------------
% % Continuity of functions on product (metric) spaces % % Author: Anthony Narkawicz, NASA Langley % % % Version 1.0 August 19, 2009 % %------------------------------------------------------------------------------- cross_metric_cont[T1:Type+,d1:[T1,T1->nnreal], T2:Type+,d2:[T2,T2->nnreal],T3:TYPE+,d3:[T3,T3->nnreal]]: THEORY BEGIN ASSUMING IMPORTING metric_spaces fullset_metric_space1: ASSUMPTION metric_space?[T1,d1](fullset[T1]) fullset_metric_space2: ASSUMPTION metric_space?[T2,d2](fullset[T2]) fullset_metric_space3: ASSUMPTION metric_space?[T3,d3](fullset[T3]) ENDASSUMING IMPORTING cross_metric_spaces[T1,d1,T2,d2], continuity_ms_def[[T1,T2],d[T1,d1,T2,d uniform_continuity[T1,d1,T3,d3] S: VAR set[[T1,T2]] X: VAR set[T1] Y: VAR set[T2] f: VAR [[T1,T2] -> T3] product_cont_equiv: LEMMA continuous?(f,S) IFF (FORALL (x: (S), epsilon: posreal): EXISTS (delta: posreal): FORALL (y: (S)): (d1(x`1,y`1) <= delta AND d2(x`2,y`2) <= delta) IMPLIES d3(f(x),f(y))<epsilon) product_cont_product_subset: COROLLARY continuous?(f,fullset[[(X),(Y)]]) IFF (FORALL (x: (X), y: (Y), epsilon: posreal): EXISTS (delta: posreal): FORALL (z: (X), w: (Y)): (d1(x,z) <= delta AND d2(y,w) <= delta) IMPLIES d3(f(x,y),f(z,w))<epsilon) % ----------- Uniform Continuity In One Variable --------------- uniformly_continuous_in_first?(f,X,Y): bool = FORALL (y1: (Y), epsilon: posreal): EXISTS (delta: posreal): FORALL (x1,x2: (X), y2: (Y)): (d1(x1,x2) <= delta AND d2(y1,y2) <= delta) IMPLIES d3(f(x1,y1),f(x2,y2))<epsilon uniformly_continuous_in_second?(f,X,Y): bool = FORALL (x1: (X), epsilon: posreal): EXISTS (delta: posreal): FORALL (x2: (X), y1,y2: (Y)): (d1(x1,x2) <= delta AND d2(y1,y2) <= delta) IMPLIES d3(f(x1,y1),f(x2,y2))<epsilon % --------- An Equivalent, Sequence Definition Of Uniform Continuity In One Variable ---- one_variable_unif_cont_sequence: LEMMA NOT uniformly_continuous_in_first?(f,X,Y) IFF EXISTS (epsilon: posreal): EXISTS (y: (Y)): EXISTS (seq: [posint -> [T1,T1,T2]]): FORALL (n: posint): (X(seq(n)`1) AND X(seq(n)`2) AND Y(seq(n)`3) AND d1(seq(n)`1,seq(n)`2) < 1/n AND d2(y,seq(n)`3) < 1/n AND d3(f(seq(n)`1,y),f(seq(n)`2,seq(n)`3)) > epsilon) %--------- This implies that the associated curried function is uniformly continuous ---- curried_is_uniform: LEMMA uniformly_continuous_in_first?(f,X,Y) IMPLIES (FORALL (y: (Y uniformly_continuous?((LAMBDA (t: T1): f(t,y)),X)) END cross_metric_cont ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28