|
vect_vect_2D_continuity: THEORY
%%% A theory of continuity for functions from [Vect2,Nz_vect2] into
%%% both Vect2 and real
BEGIN
IMPORTING vectors@vectors_2D
ffv,ggv,hhv : VAR [[Vect2,Nz_vect2]->Vect2]
ffr,ggr,hhr : VAR [[Vect2,Nz_vect2]->real]
s : VAR Vect2
nzv : VAR Nz_vect2
c : VAR real
continuous_vvv?(ffv): bool =
FORALL (epsil:posreal,s:Vect2,nzv:Nz_vect2):
EXISTS (ds, dv: posreal):
FORALL (sp:Vect2,nzvp:Nz_vect2):
norm(s - sp) < ds AND
norm(nzv-nzvp) < dv
IMPLIES
norm(ffv(s, nzv) - ffv(sp,nzvp)) < epsil
sum_vvv(ggv,hhv)(s,nzv): Vect2 = ggv(s,nzv)+hhv(s,nzv)
diff_vvv(ggv,hhv)(s,nzv): Vect2 = ggv(s,nzv)-hhv(s,nzv)
scal_vvv(c,hhv)(s,nzv): Vect2 = c*hhv(s,nzv)
continuous_vvr?(ffr): bool =
FORALL (epsil:posreal,s:Vect2,nzv:Nz_vect2):
EXISTS (ds, dv: posreal):
FORALL (sp:Vect2,nzvp:Nz_vect2):
norm(s - sp) < ds AND
norm(nzv-nzvp) < dv
IMPLIES
abs(ffr(s, nzv) - ffr(sp,nzvp)) < epsil
sum_vvr(ggr,hhr)(s,nzv): real = ggr(s,nzv)+hhr(s,nzv)
diff_vvr(ggr,hhr)(s,nzv): real = ggr(s,nzv)-hhr(s,nzv)
prod_vvr(ggr,hhr)(s,nzv): real = ggr(s,nzv)*hhr(s,nzv)
max_vvr(ggr,hhr)(s,nzv): real = max(ggr(s,nzv),hhr(s,nzv))
scal_vvr(c,hhr)(s,nzv): real = c*hhr(s,nzv)
const_vvr(c)(s,nzv): real = c
scal_vvr_vvv(ffr,ggv)(s,nzv): Vect2 = ffr(s,nzv)*ggv(s,nzv)
dot_vvv(ffv,ggv)(s,nzv): real = ffv(s,nzv)*ggv(s,nzv)
nzero_vvr?(ffr): bool = (FORALL (s,nzv): ffr(s,nzv)/=0)
continuous_nz_vvr?(ffr): bool = continuous_vvr?(ffr) AND nzero_vvr?(ffr)
ffvc,ggvc,hhvc: VAR (continuous_vvv?)
ffrc,ggrc,hhrc: VAR (continuous_vvr?)
ggnz : VAR (nzero_vvr?)
ggnzc : VAR (continuous_nz_vvr?)
div_vvr(ffr,ggnz)(s,nzv): real = ffr(s,nzv)/ggnz(s,nzv)
norm_vvv(ffv)(s,nzv): nnreal = norm(ffv(s,nzv))
%%%%%%% %%%%%%%
sum_vvv_cont: LEMMA continuous_vvv?(sum_vvv(ffvc,ggvc))
sum_vvr_cont: LEMMA continuous_vvr?(sum_vvr(ffrc,ggrc))
diff_vvv_cont: LEMMA continuous_vvv?(diff_vvv(ffvc,ggvc))
scal_vvv_cont: LEMMA continuous_vvv?(scal_vvv(c,ffvc))
dot_vvv_cont: LEMMA continuous_vvr?(dot_vvv(ffvc,ggvc))
prod_vvr_cont: LEMMA continuous_vvr?(prod_vvr(ffrc,ggrc))
const_vvr_cont: LEMMA continuous_vvr?(const_vvr(c))
scal_vvr_vvv_cont: LEMMA continuous_vvv?(scal_vvr_vvv(ffrc,ggvc))
scal_vvr_cont: LEMMA continuous_vvr?(scal_vvr(c,ffrc))
div_vvr_cont: LEMMA continuous_vvr?(div_vvr(ffrc,ggnzc))
nzv_vvv_cont: LEMMA continuous_vvv?(LAMBDA (s,nzv): nzv)
s_vvv_cont: LEMMA continuous_vvv?(LAMBDA (s,nzv): s)
max_vvr_cont: LEMMA continuous_vvr?(max_vvr(ffrc,ggrc))
norm_vvv_cont: LEMMA continuous_vvr?(norm_vvv(ffvc))
END vect_vect_2D_continuity
¤ Dauer der Verarbeitung: 0.16 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.
|
