|
unique: THEORY
BEGIN
IMPORTING prelude_aux
IMPORTING cauchy
IMPORTING neg
IMPORTING add
p,s: VAR nat
x,y: VAR real
cx: VAR cauchy_real
nzcx: VAR cauchy_nzreal
nncx: VAR cauchy_nnreal
npcx: VAR cauchy_npreal
ncx: VAR cauchy_negreal
pcx: VAR cauchy_posreal
px: VAR posreal
nzx: VAR nzreal
f: VAR [nzreal->nzreal]
cf: VAR [cauchy_nzreal->cauchy_nzreal]
unique_cauchy: LEMMA cauchy_prop(x,cx) AND cauchy_prop(y,cx) => x = y
cauchy_dich1: LEMMA cauchy_posreal?(nzcx) IFF NOT cauchy_negreal?(nzcx)
cauchy_dich2: LEMMA cauchy_negreal?(nzcx) IFF NOT cauchy_posreal?(nzcx)
cauchy_dich3: LEMMA cauchy_nnreal?(nncx) IFF NOT cauchy_negreal?(nncx)
cauchy_dich4: LEMMA cauchy_npreal?(npcx) IFF NOT cauchy_posreal?(npcx)
cauchy_dich5: LEMMA cauchy_negreal?(nzcx) OR cauchy_posreal?(nzcx)
cauchy_trich: LEMMA cauchy_negreal?(cx) OR cx = cauchy_zero OR cauchy_posreal?(cx)
cauchy_pos_characteristic: LEMMA 0 <= pcx(p)
cauchy_neg_characteristic: LEMMA ncx(p) <= 0
cauchy_pos_monotonic: LEMMA 3 <= pcx(s) => 3 <= pcx(s+p)
cauchy_monotonic: LEMMA 3 <= abs(nzcx(s)) => 3 <= abs(nzcx(s+p))
odd_real_fn?(f:[nzreal->nzreal]):bool = FORALL (x:nzreal): (f(-x) = -f(x))
odd_cauchy_fn?(cf:[cauchy_nzreal->cauchy_nzreal]):bool
= FORALL (cx:cauchy_nzreal):(cf(cauchy_neg(cx)) = cauchy_neg(cf(cx)))
cauchy_odd_extend: LEMMA odd_real_fn?(f) AND odd_cauchy_fn?(cf) AND
(FORALL (px:posreal, pcx:cauchy_posreal):
cauchy_prop(px,pcx) => cauchy_prop(f(px),cf(pcx))) =>
(cauchy_prop(nzx,nzcx) => cauchy_prop(f(nzx),cf(nzcx)))
END unique
¤ Dauer der Verarbeitung: 0.14 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.
|
