Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: inverse_continuous_functions.pvs Sprache: PVS

Original von: PVS^©

inverse_continuous_functions [ T1, T2 : NONEMPTY_TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%  More properties of continuous functions [T1 -> T2]
%  Applications of continuity_interval
%----------------------------------------------------------------------------
BEGIN

  ASSUMING

    connected_domain : ASSUMPTION FORALL (x, y : T1), (z : real) :
                                x <= z AND z <= y IMPLIES T1_pred(z)

    % old bug workaround: T1_pred is not correctly expanded
    %  connected_domain : ASSUMPTION
    % FORALL (x, y : T1), (z : real) :
    %     x <= z AND z <= y IMPLIES (EXISTS (u : T1) : z = u)

  ENDASSUMING

  IMPORTING continuous_functions_props


  g : VAR { f : [T1 -> T2] | continuous?(f) }

  %-------------------------------------------------------------
  %  inverse of a continuous, bijective function is continuous
  %-------------------------------------------------------------

  inverse_incr : LEMMA bijective?[T1, T2](g) AND strict_increasing?(g)
                           IMPLIES continuous?(inverse(g))

  inverse_decr : LEMMA bijective?[T1, T2](g) AND strict_decreasing?(g)
                           IMPLIES continuous?(inverse(g))

  inverse_continuous : LEMMA bijective?[T1, T2](g)
                                IMPLIES continuous?(inverse(g))

END inverse_continuous_functions

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