|
deriv_sigma[T: TYPE FROM real] : THEORY
BEGIN
ASSUMING
IMPORTING analysis@deriv_domain_def
deriv_domain : ASSUMPTION deriv_domain?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
CONVERSION+ singleton
IMPORTING analysis@derivatives[T], reals@sigma_below, deriv_real_vect_def, reals@sigma_below_sub
x,y: VAR T
n: VAR nat
m: VAR posnat
sigma_derivable: LEMMA
FORALL (h: [T -> [Index[m] -> real]]):
(FORALL (i: below[m]): derivable?(LAMBDA (t: T): h(t)(i), y)) IMPLIES
derivable?((LAMBDA (x: T): sigma(0, m - 1, LAMBDA (i: Index[m]): h(x)(i))), y)
deriv_sigma: LEMMA n > 0 IMPLIES
FORALL (h: [T -> [Index[n] -> real]]):
(FORALL (i: below[n]): derivable?(LAMBDA (t: T): h(t)(i), y))
IMPLIES
deriv(LAMBDA (x: T): sigma(0, n - 1, LAMBDA (i: Index[n]): h(x)(i)),y)
= sigma(0, n - 1, LAMBDA (i: Index[n]): deriv(h, y)(i))
END deriv_sigma
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
