|
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)
¤
|
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.
|
