Quelle inverse_continuous_functions.pvs
Sprache: 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 : ASSUMPTIONFORALL (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))
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.
