|
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
¤ Dauer der Verarbeitung: 0.16 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.
|
