|
restrict2_deriv[T1, T2 : TYPE FROM real] : THEORY
BEGIN
ASSUMING
IMPORTING deriv_domain_def
deriv_domain_T1: ASSUMPTION deriv_domain?[T1]
deriv_domain_T2: ASSUMPTION deriv_domain?[T2]
not_one_element_T1 : ASSUMPTION not_one_element?[T1]
not_one_element_T2 : ASSUMPTION not_one_element?[T2]
sub_domain : ASSUMPTION
FORALL (x : T1) : EXISTS (y : T2) : x = y
ENDASSUMING
IMPORTING derivatives, chain_rule
f : VAR deriv_fun[T2]
a : VAR T1
sub_dom : JUDGEMENT T1 SUBTYPE_OF T2 % FORALL (u : T1) : T2_pred(u)
restrict2(f) : [T1 -> real] = LAMBDA (u : T1) : f(u)
CONVERSION restrict2
restrict2_derivable : LEMMA derivable?[T1](f)
restrict2_deriv : LEMMA deriv(f)(a) = deriv[T1](f)(a)
END restrict2_deriv
¤ Dauer der Verarbeitung: 0.15 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.
|
