Quelle interm_value_thm.pvs Sprache: unbekannt

interm_value_thm: THEORY
%-----------------------------------------------------------------
% API for Intermediate Value Theorem
%-----------------------------------------------------------------
BEGIN

 IMPORTING continuity_interval, reals@intervals_real

 a,b,x: VAR real

 interm_value1 : LEMMA a real]):
 continuous?(f) AND f(a) < x AND x < f(b)
 IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

 interm_value2 : LEMMA a real]):
 continuous?(f) AND f(a) <= x AND x <= f(b)
 IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

 interm_value3 : LEMMA a real]):
 continuous?(f) AND f(b) < x AND x < f(a)
 IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

 interm_value4 : LEMMA a real]):
 continuous?(f) AND f(b) <= x AND x <= f(a)
 IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

 interm_value5 : LEMMA a real],p,q:closed_interval(a,b)):
 continuous?(f) AND f(p) <= x AND x <= f(q)
 IMPLIES EXISTS (c: closed_interval(a,b)):
 ((p<=c AND c<=q) OR (q<=c AND c<=p)) AND f(c) = x

 f: VAR [real -> real]

 cont_intv : LEMMA a < b AND continuous?(f)
 IMPLIES continuous?(LAMBDA (x: closed_interval(a, b)): f(x))

 cont_intv1: LEMMA a < b AND continuous?[closed_interval[real](a, b)](f)
 IMPLIES continuous?(LAMBDA (x: closed_interval(a, b)): f(x))

 interm_val1 : LEMMA a < b IMPLIES
 continuous?[closed_interval(a,b)](f) AND f(a) < x AND x < f(b)
 IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

 interm_val2 : LEMMA a real]):
 continuous?[closed_interval(a,b)](f) AND f(a) <= x AND x <= f(b)
 IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

 interm_val3 : LEMMA a real]):
 continuous?[closed_interval(a,b)](f) AND f(b) < x AND x < f(a)
 IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

 interm_val4 : LEMMA a real]):
 continuous?[closed_interval(a,b)](f) AND f(b) <= x AND x <= f(a)
 IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

 % ----------------------------------------------------------------------------------

 xl,xu: VAR real

 zeros_interm: LEMMA continuous?(f)
 AND f(xl) = 0 AND f(xu) = 0 AND
 (FORALL (x: open_interval(xl,xu)): f(x) /= 0)
 IMPLIES
 (FORALL (x: open_interval(xl,xu)): f(x) > 0) OR
 (FORALL (x: open_interval(xl,xu)): f(x) < 0)

 % ----------------------------------------------------------------------------------

 IMPORTING reals@connected_set

 ab : VAR Connected

 IntermediateValue : THEOREM
 FORALL (f:[real->real]):
 continuous?(f) AND
 (FORALL (c:(ab)) : f(c) /= 0) IMPLIES
 (FORALL (x,y:(ab)) : f(x)*f(y) > 0)

END interm_value_thm

quality94%

Quelle interm_value_thm.pvs Sprache: unbekannt

[ zur Elbe Produktseite wechseln0.24Quellennavigators Analyse erneut starten ]