|
four_vects_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,Vect2,Vect2,Vect2]->Vect2]
ffr,ggr,hhr : VAR [[Vect2,Vect2,Vect2,Vect2]->real]
so,vo,si,vi,
nso,nvo,nsi,nvi : VAR Vect2
nzv : VAR Nz_vect2
c : VAR real
continuous_vvv?(ffv): bool =
FORALL (epsil:posreal,so,vo,si,vi):
EXISTS (dso,dvo,dsi,dvi: posreal):
FORALL (nso,nvo,nsi,nvi):
norm(so - nso) < dso AND
norm(vo - nvo) < dvo AND
norm(si - nsi) < dsi AND
norm(vi - nvi) < dvi
IMPLIES
norm(ffv(so,vo,si,vi)-ffv(nso,nvo,nsi,nvi)) < epsil
sum_vvv(ggv,hhv)(so,vo,si,vi): Vect2 = ggv(so,vo,si,vi)+hhv(so,vo,si,vi)
diff_vvv(ggv,hhv)(so,vo,si,vi): Vect2 = ggv(so,vo,si,vi)-hhv(so,vo,si,vi)
scal_vvv(c,hhv)(so,vo,si,vi): Vect2 = c*hhv(so,vo,si,vi)
continuous_vvr?(ffr): bool =
FORALL (epsil:posreal,so,vo,si,vi):
EXISTS (dso,dvo,dsi,dvi: posreal):
FORALL (nso,nvo,nsi,nvi):
norm(so - nso) < dso AND
norm(vo - nvo) < dvo AND
norm(si - nsi) < dsi AND
norm(vi - nvi) < dvi
IMPLIES
abs(ffr(so,vo,si,vi)-ffr(nso,nvo,nsi,nvi)) < epsil
sum_vvr(ggr,hhr)(so,vo,si,vi): real = ggr(so,vo,si,vi)+hhr(so,vo,si,vi)
diff_vvr(ggr,hhr)(so,vo,si,vi): real = ggr(so,vo,si,vi)-hhr(so,vo,si,vi)
prod_vvr(ggr,hhr)(so,vo,si,vi): real = ggr(so,vo,si,vi)*hhr(so,vo,si,vi)
max_vvr(ggr,hhr)(so,vo,si,vi): real = max(ggr(so,vo,si,vi),hhr(so,vo,si,vi))
scal_vvr(c,hhr)(so,vo,si,vi): real = c*hhr(so,vo,si,vi)
const_vvr(c)(so,vo,si,vi): real = c
scal_vvr_vvv(ffr,ggv)(so,vo,si,vi): Vect2 = ffr(so,vo,si,vi)*ggv(so,vo,si,vi)
dot_vvv(ffv,ggv)(so,vo,si,vi): real = ffv(so,vo,si,vi)*ggv(so,vo,si,vi)
nzero_vvr?(ffr): bool = (FORALL (so,vo,si,vi): ffr(so,vo,si,vi)/=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)(so,vo,si,vi): real = ffr(so,vo,si,vi)/ggnz(so,vo,si,vi)
norm_vvv(ffv)(so,vo,si,vi): nnreal = norm(ffv(so,vo,si,vi))
%%%%%%% %%%%%%%
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))
input1_vvv_cont: LEMMA continuous_vvv?(LAMBDA (so,vo,si,vi): so)
input2_vvv_cont: LEMMA continuous_vvv?(LAMBDA (so,vo,si,vi): vo)
input3_vvv_cont: LEMMA continuous_vvv?(LAMBDA (so,vo,si,vi): si)
input4_vvv_cont: LEMMA continuous_vvv?(LAMBDA (so,vo,si,vi): vi)
max_vvr_cont: LEMMA continuous_vvr?(max_vvr(ffrc,ggrc))
norm_vvv_cont: LEMMA continuous_vvr?(norm_vvv(ffvc))
END four_vects_2D_continuity
¤ Dauer der Verarbeitung: 0.0 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.
|
