Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: cross_metric_real_fun.pvs Sprache: PVS

Original von: PVS^©

%---------------------------------------------------------------------------------------------------------
%
%       One-Variable Uniform Continuity of Real Valued Functions on Product Metric Spaces
%
%       Author: Anthony Narkawicz, NASA Langley
%
%
%       Version 1.0                     August 27, 2009
%
%---------------------------------------------------------------------------------------------------------

cross_metric_real_fun[T1:Type+,d1:[T1,T1->nnreal],
                  T2:Type+,d2:[T2,T2->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])

    ENDASSUMING

  IMPORTING real_metric_space,cross_metric_uniform_continuity[T1,d1,T2,d2,real,real_dist], continuity_ms[T2,d2,real,real_dist], real_fun_on_compact_sets[T1,d1]

  X: VAR set[T1]
  Y: VAR set[T2]
  f: VAR [[T1,T2] -> real]

  % If X is compact, then the function unif_min_first(f,X) = (LAMBDA (t: T2) = min({r: real | EXISTS (x: (X)): r = f(x,t)}))
  % is continuous.

  IMPORTING reals@bounded_reals[real]

  % The main TCC:

  curried_min_exists: LEMMA nonempty?(X) AND continuous?(f,fullset[[(X),(Y)]]) AND compact?(X)
     IMPLIES (FORALL (t: T2): Y(t) IMPLIES
         nonempty?[real]({r: real | EXISTS (x: (X)): r = f(x, t)}) AND
          below_bounded[real]({r: real | EXISTS (x: (X)): r = f(x, t)}) AND
           ext[real]({r: real | EXISTS (x: (X)): r = f(x, t)})(inf[real]({r: real | EXISTS (x: (X)): r = f(x, t)}))
    AND (EXISTS (x: (X)): FORALL (y: (X)): f(x,t) <= f(y,t)))

  curried_min_is_cont: THEOREM (compact?(X) AND continuous?(f,fullset[[(X),(Y)]]) AND nonempty?(X)) IMPLIES
           LET unif_min_first(t: T2): real = IF Y(t) THEN min({r: real | EXISTS (x: (X)): r = f(x,t)}) ELSE 0 ENDIF
         IN  continuous?(unif_min_first,Y)



END cross_metric_real_fun

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.