|
continuity_interval [ a : real, b : {x : real | a <= x }] : THEORY
%-----------------------------------------------------------------
% continuous functions on a closed interval
%-----------------------------------------------------------------
BEGIN
%-----------------------------
% Interval [a, b] as a type
%-----------------------------
x : VAR real
J : NONEMPTY_TYPE = { x | a <= x AND x <= b}
f : VAR [J -> real]
u : VAR sequence[J]
c : VAR J
n, i : VAR nat
IMPORTING continuity_props
%-----------------------------------------------
% Reformulation of Bolzano/Weirstrass theorem
%-----------------------------------------------
bolz_weier : LEMMA EXISTS c : accumulation(u, c)
%-------------------------------------
% If f is continuous, it is bounded
%-------------------------------------
unbounded_sequence : LEMMA bounded_above?(f) OR
EXISTS u : FORALL n : f(u(n)) > n
bounded_from_above : LEMMA continuous?(f) IMPLIES bounded_above?(f)
bounded_from_below : LEMMA continuous?(f) IMPLIES bounded_below?(f)
%--------------------------------------
% f has a maximum and a minimum in J
%--------------------------------------
max_extraction : LEMMA continuous?(f) IMPLIES
EXISTS u : FORALL n : sup(f) - f(u(n)) < 1/(n+1)
sup_is_reached : LEMMA continuous?(f) IMPLIES EXISTS c : f(c) = sup(f)
maximum_exists : LEMMA continuous?(f) IMPLIES EXISTS c : is_maximum(c, f)
max_pt(f:{f|continuous?(f)}): {xj: J | is_maximum(xj,f)} % ADDED BY RWB
inf_is_reached : LEMMA continuous?(f) IMPLIES EXISTS c : f(c) = inf(f)
minimum_exists : LEMMA continuous?(f) IMPLIES EXISTS c : is_minimum(c, f)
min_pt(f:{f|continuous?(f)}): {xj: J | is_minimum(xj,f)} % ADDED BY RWB
%-------------------------------
% Intermediate value theorem
%-------------------------------
intermediate_value1 : LEMMA continuous?(f) AND f(a) < x AND x < f(b)
IMPLIES EXISTS c : f(c) = x
intermediate_value2 : LEMMA continuous?(f) AND f(a) <= x AND x <= f(b)
IMPLIES EXISTS c : f(c) = x
intermediate_value3 : LEMMA continuous?(f) AND f(b) < x AND x < f(a)
IMPLIES EXISTS c : f(c) = x
intermediate_value4 : LEMMA continuous?(f) AND f(b) <= x AND x <= f(a)
IMPLIES EXISTS c : f(c) = x
END continuity_interval
¤ Dauer der Verarbeitung: 0.19 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.
|
