integral_mean_value[T: TYPE+ FROM real]: THEORY
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
deriv_domain: LEMMA deriv_domain?[T]
IMPORTING fundamental_theorem[T]
f: VAR [T -> real]
a,b: VAR T
mean_value_integral: LEMMA a < b AND
continuous?(f)
IMPLIES
(EXISTS (c: Open_interval[T](a,b)):
Integral(a,b,f) = f(c)*(b-a) )
mvi_cor1: LEMMA a < b AND
(FORALL (x: Closed_interval[T](a,b)): f(x) > 0) AND
continuous?(f) AND
Integral(a,b,f) = 0
IMPLIES a = b
END integral_mean_value
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.27Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|