| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle derivative_inverse.pvs Sprache: PVS |
|||||||||
|
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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28