|
cont_vect3_real: THEORY
%------------------------------------------------------------------------------
% Continuous functions [ Vect3 -> real]
%
% Author: Rick Butler NASA Langley Research Center 2/1/2009
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING limit_vect3_real
f, f1, f2 : VAR [Vect3 -> real]
g : VAR [Vect3 -> nzreal]
u : VAR real
x, x0 : VAR Vect3
epsilon, delta : VAR posreal
n : VAR nat
%--------------------
% Continuity at x0
%--------------------
continuous_vr?(f, x0) : bool =
FORALL epsilon : EXISTS delta : FORALL x :
norm(x - x0) < delta IMPLIES abs(f(x) - f(x0)) < epsilon
continuity_def : LEMMA
continuous_vr?(f, x0) IFF convergence(f, x0, f(x0))
continuity_def2 : LEMMA
continuous_vr?(f, x0) IFF convergent?(f, x0)
%------------------------------------------
% Operations preserving continuity at x0
%------------------------------------------
sum_continuous_vr : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
IMPLIES continuous_vr?(f1 + f2, x0)
diff_continuous_vr : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
IMPLIES continuous_vr?(f1 - f2, x0)
prod_continuous_vr : LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)
IMPLIES continuous_vr?(f1 * f2, x0)
const_continuous_vr: LEMMA continuous_vr?(const_fun(u), x0)
scal_continuous_vr : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(u * f, x0)
neg_continuous_vr : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(- f, x0)
div_continuous_vr : LEMMA continuous_vr?(f, x0) AND continuous_vr?(g, x0)
IMPLIES continuous_vr?(f/g, x0)
inv_continuous_vr : LEMMA continuous_vr?(g, x0) IMPLIES continuous_vr?(1/g, x0)
expt_continuous_vr : LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(f^n, x0)
%---------------------------------
% Continuity of f in its domain
%---------------------------------
continuous_vr?(f): bool = FORALL x0: continuous_vr?(f, x0)
% ------------ Alternate forms and names for convenience ---------------
sum_cont_vr_fun : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
IMPLIES continuous_vr?(f1 + f2)
diff_cont_vr_fun : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
IMPLIES continuous_vr?(f1 - f2)
prod_cont_vr_fun : LEMMA continuous_vr?(f1) AND continuous_vr?(f2)
IMPLIES continuous_vr?(f1 * f2)
const_cont_vr_fun: LEMMA continuous_vr?(const_fun(u))
scal_cont_vr_fun : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(u * f)
neg_cont_vr_fun : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(-f)
div_cont_vr_fun : LEMMA continuous_vr?(f) AND continuous_vr?(g)
IMPLIES continuous_vr?(f/g)
inv_cont_vr_fun : LEMMA continuous_vr?(g) IMPLIES continuous_vr?(1/g)
expt_cont_vr_fun : LEMMA continuous_vr?(f) IMPLIES continuous_vr?(f^n)
%--- Properties ---%
continuous_vr_fun: TYPE+ = { f | continuous_vr?(f) }
nz_continuous_vr_fun: TYPE = { g | continuous_vr?(g) }
h, h1, h2: VAR continuous_vr_fun
h3: VAR nz_continuous_vr_fun
sum_fun_continuous_vr : JUDGEMENT +(h1, h2) HAS_TYPE continuous_vr_fun
diff_fun_continuous_vr: JUDGEMENT -(h1, h2) HAS_TYPE continuous_vr_fun
prod_fun_continuous_vr: JUDGEMENT *(h1, h2) HAS_TYPE continuous_vr_fun
const_fun_continuous_vr: JUDGEMENT const_fun(u) HAS_TYPE continuous_vr_fun
scal_fun_continuous_vr: JUDGEMENT *(u, h) HAS_TYPE continuous_vr_fun
neg_fun_continuous_vr : JUDGEMENT -(h) HAS_TYPE continuous_vr_fun
div_fun_continuous_vr : JUDGEMENT /(h, h3) HAS_TYPE continuous_vr_fun
inv_fun_continuous_vr : LEMMA continuous_vr?(1/h3)
expt_fun_continuous_vr: LEMMA continuous_vr?(f) IMPLIES continuous_vr?(f^n)
END cont_vect3_real
¤ Dauer der Verarbeitung: 0.17 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.
|
