|
cont_vect2_vect2: THEORY
%------------------------------------------------------------------------------
% Continuous functions [ Vect2 -> real]
%
% Author: Rick Butler NASA Langley Research Center 2/1/2009
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING limit_vect2_vect2
f, f1, f2 : VAR [Vect2 -> Vect2]
g : VAR [Vect2 -> Nz_vect2]
u : VAR Vect2
x, x0 : VAR Vect2
epsilon, delta : VAR posreal
n : VAR nat
%--------------------
% Continuity at x0
%--------------------
continuous_vv?(f, x0) : bool =
FORALL epsilon : EXISTS delta :
FORALL x: norm(x-x0) < delta
IMPLIES norm(f(x) - f(x0)) < epsilon
continuity_def : LEMMA
continuous_vv?(f, x0) IFF convergence(f, x0, f(x0))
continuity_def2 : LEMMA
continuous_vv?(f, x0) IFF convergent?(f, x0)
%------------------------------------------
% Operations preserving continuity at x0
%------------------------------------------
sum_continuous_vv : LEMMA continuous_vv?(f1, x0) AND continuous_vv?(f2, x0)
IMPLIES continuous_vv?(f1 + f2, x0)
diff_continuous_vv : LEMMA continuous_vv?(f1, x0) AND continuous_vv?(f2, x0)
IMPLIES continuous_vv?(f1 - f2, x0)
const_continuous_vv: LEMMA continuous_vv?(const_fun(u), x0)
identity_continuous_vv: LEMMA continuous_vv?((LAMBDA(x):x),x0)
neg_continuous_vv : LEMMA continuous_vv?(f, x0) IMPLIES continuous_vv?(- f, x0)
%---------------------------------
% Continuity of f in its domain
%---------------------------------
continuous_vv?(f): bool = FORALL x0: continuous_vv?(f, x0)
sum_cont_vv_fun : LEMMA continuous_vv?(f1) AND continuous_vv?(f2)
IMPLIES continuous_vv?(f1 + f2)
diff_cont_vv_fun : LEMMA continuous_vv?(f1) AND continuous_vv?(f2)
IMPLIES continuous_vv?(f1 - f2)
const_cont_vv_fun: LEMMA continuous_vv?(const_fun(u))
neg_cont_vv_fun : LEMMA continuous_vv?(f) IMPLIES continuous_vv?(-f)
id_cont_vv_fun : LEMMA continuous_vv?((LAMBDA(x):x))
%--- Properties ---%
continuous_vv_fun: TYPE+ = { f | continuous_vv?(f) }
nz_continuous_vv_fun: TYPE = { g | continuous_vv?(g) }
h, h1, h2: VAR continuous_vv_fun
h3: VAR nz_continuous_vv_fun
sum_fun_continuous_vv : JUDGEMENT +(h1, h2) HAS_TYPE continuous_vv_fun
diff_fun_continuous_vv: JUDGEMENT -(h1, h2) HAS_TYPE continuous_vv_fun
const_fun_continuous_vv: JUDGEMENT const_fun(u) HAS_TYPE continuous_vv_fun
neg_fun_continuous_vv : JUDGEMENT -(h) HAS_TYPE continuous_vv_fun
END cont_vect2_vect2
¤ Dauer der Verarbeitung: 0.23 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.
|
