|
interval_minmax[T: TYPE FROM real]: THEORY
%----------------------------------------------------------------------------
%
%----------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING continuity_interval, reals@intervals_real
f: VAR [T -> real]
x,y,a,b: VAR T
fun_cont_on(a:T,b:{x:T|a<x}): TYPE = {f |
(FORALL (x: closed_interval(a,b)):
continuous?(restrict[T,closed_interval(a,b),real](f),x))}
min_x(a:T,b:{x:T|a<x}, f: fun_cont_on(a,b)):
{mx: T | a <= mx AND mx <= b AND
(FORALL (x: T): a <= x AND x <= b IMPLIES
f(mx) <= f(x))}
max_x(a:T,b:{x:T|a<x}, f: fun_cont_on(a,b)):
{mx: T | a <= mx AND mx <= b AND
(FORALL (x: T): a <= x AND x <= b IMPLIES
f(mx) >= f(x))}
END interval_minmax
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
