continuous_functions_props[ T : TYPEFROM 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
¤ 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.0.0Bemerkung:
(vorverarbeitet)
¤
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.
