|
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
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 : LEMMA a <= b AND g(a) <= x AND x <= g(b) IMPLIES
EXISTS c : a <= c AND c <= b AND g(c) = x
intermediate2 : LEMMA 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 : LEMMA 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 : LEMMA 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.21 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.
|
