Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: continuous_functions_props.pvs Sprache: PVS

Original von: PVS^©

continuous_functions_props[ T : TYPE FROM real] : THEORY
%--------------------------------------------------------
%  More properties of continuous functions [T1 -> T2]  %
%  Applications of continuity_interval                 %
%--------------------------------------------------------
BEGIN

   ASSUMING

   connected_domain : ASSUMPTION
  FORALL (x, y : T), (z : real) :
      x <= z AND z <= y IMPLIES T_pred(z)

   ENDASSUMING

   IMPORTING % continuity_interval
             continuous_functions,
             reals@real_fun_preds

   f : VAR [T -> real]
   a, b, c, d : VAR T

  % sub_interval : LEMMA
  % FORALL (c : T), (d : {x : T | c <= x}), (u : J[c, d]) : T_pred(u)

  %----------------------------------------
  %  Restriction to a sub-interval of T1
  %----------------------------------------

  % R(f, (c : T), (d : {x : T | c <= x})) : [J[c,d] -> real] =
  % LAMBDA (u : J[c, d]) : f(u)

  %-----------------------------------------------------
  %  If f is continuous, its restriction is continuous
  %-----------------------------------------------------

  g : VAR { f | continuous?(f) }

  % continuous_in_subintervals : LEMMA
  % a <= b IMPLIES continuous?(R(g, a, b))

  %------------------------------
  %  Intermediate value theorem
  %------------------------------

  x, y, z : VAR real

  intermediate1 : AXIOM a <= b AND g(a) <= x AND x <= g(b) IMPLIES
                   EXISTS c : a <= c AND c <= b AND g(c) = x

  intermediate2 : AXIOM a <= b AND g(b) <= x AND x <= g(a) IMPLIES
                   EXISTS c : a <= c AND c <= b AND g(c) = x

  %----------------------------------
  %  Max and minimum in an interval
  %----------------------------------

  max_in_interval : AXIOM a <= b IMPLIES
                    EXISTS c : a <= c AND c <= b AND
              (FORALL d : a <= d AND d <= b IMPLIES g(d) <= g(c))

  min_in_interval : AXIOM a <= b IMPLIES
                    EXISTS c : a <= c AND c <= b AND
              (FORALL d : a <= d AND d <= b IMPLIES g(c) <= g(d))

  %---------------------------------------------------------
  %  Injective, continuous functions are strictly monotone
  %---------------------------------------------------------

  inj_continuous : LEMMA injective?(g) AND a <= b AND b <= c IMPLIES
                     (g(a) <= g(b) AND g(b) <= g(c))
                     OR (g(c) <= g(b) AND g(b) <= g(a))

  inj_monotone   : LEMMA injective?(g) IFF
                     strict_increasing?(g) OR strict_decreasing?(g)

END continuous_functions_props

¤ Dauer der Verarbeitung: 0.12 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.