|
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
continuous_functions,
reals@real_fun_preds
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 : AXIOM a <= b AND g(a) <= x AND x <= g(b) IMPLIES
EXISTS c : a <= c AND c <= b AND g(c) = x
intermediate2 : AXIOM 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 : AXIOM 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 : AXIOM 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
[ zur Elbe Produktseite wechseln0.4Quellennavigators
Analyse erneut starten
]
|
