| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle interval_minmax.pvs Sprache: PVS |
|||||||||
|
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.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28