Quelle subinterval_deriv.pvs Sprache: PVS

%% subinterval_deriv.pvs

subinterval_deriv : THEORY
BEGIN

  IMPORTING interval_deriv, analysis@deriv_domain

  n : VAR nat

  deriv_domain_Xt: LEMMA FORALL(X:(StrictInterval?)): deriv_domain?[Xt[X]]

  subinterval_deriv : LEMMA
    FORALL(X,Y:(StrictInterval?),f:[Xt[X]->real]):
      Y << X AND
      Diff?(f) IMPLIES
      (Diff?(LAMBDA(x:Xt[Y]):f(x)) AND
       D(LAMBDA(x:Xt[Y]):f(x)) = LAMBDA(x:Xt[Y]):D(f)(x))

  subinterval_derivn : LEMMA
    FORALL(X,Y:(StrictInterval?),f:[Xt[X]->real]):
      Y << X AND
      Diffn?(n)(f) IMPLIES
      (Diffn?(n)(LAMBDA(x:Xt[Y]):f(x)) AND
       Dn(n,LAMBDA(x:Xt[Y]):f(x)) = LAMBDA(x:Xt[Y]):Dn(n,f)(x))


END subinterval_deriv

quality22%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.