|
derivative_inverse [ T1, T2: TYPE FROM real ]: THEORY
%------------------------------------------------------------------------------
%
% Derivative of Inverse
%
% Author: David Lester (Manchester University)
%
%------------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def
connected_domain1 : ASSUMPTION connected?[T1]
not_one_element1 : ASSUMPTION not_one_element?[T1]
connected_domain2 : ASSUMPTION connected?[T2]
not_one_element2 : ASSUMPTION not_one_element?[T2]
ENDASSUMING
deriv_domain1: LEMMA deriv_domain?[T1]
deriv_domain2: LEMMA deriv_domain?[T2]
IMPORTING derivatives, derivative_props, % derivatives_more,
chain_rule, inverse_continuous_functions,
lim_of_functions, composition_continuous
F: VAR [T1 -> T2]
G: VAR [T2 -> T1]
f: VAR [T1 -> nzreal] % WAS: {nzx:nzreal| T2_pred(1/nzx)}]
x: VAR T2
inverse_derivable: LEMMA
derivable?[T1](F) AND bijective?[T1,T2](F) AND deriv[T1](F) = f
AND inverse?[T1,T2](G,F) IMPLIES derivable?[T2](G,x)
inverse_derivable_fun: LEMMA
derivable?[T1](F) AND bijective?[T1,T2](F) AND deriv[T1](F) = f
AND inverse?[T1,T2](G,F) IMPLIES derivable?[T2](G)
deriv_inverse_fun: LEMMA derivable?[T1](F) AND deriv[T1](F) = f
AND bijective?[T1,T2](F) AND inverse?[T1,T2](G,F)
IMPLIES deriv[T2](G) = (LAMBDA (x:T2): 1/f(G(x)))
deriv_inverse: LEMMA derivable?[T1](F) AND deriv[T1](F) = f
AND bijective?[T1,T2](F) AND inverse?[T1,T2](G,F)
IMPLIES derivable?[T1](F) AND
deriv[T2](G) = (LAMBDA (x:T2): 1/f(G(x)))
END derivative_inverse
¤ Dauer der Verarbeitung: 0.21 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.
|
