|
%------------------------------------------------------------------------------
% Set-valued complex functions
%
% Author: David Lester, Manchester University & NIA
%
% Version 1.0 4/12/07 Initial version (DRL)
%------------------------------------------------------------------------------
complex_sets: THEORY
BEGIN
IMPORTING exp
z,z1,z2: VAR complex
n0x,n0y,n0z: VAR nzcomplex
nnx: VAR nnreal
nx: VAR negreal
r,x,y: VAR real
j: VAR int
theta: VAR argrng
% Considerable notational and practical convenience can be obtained by using
% instead "Arg" to represent the set of all possible argument values.
% To bring elegance into this theory we define addition and unary and
% binary minus.
;
-: MACRO [nonempty_set[real]->nonempty_set[real]]
= (LAMBDA (X:nonempty_set[real]): {x | X(-x)});
+: MACRO [nonempty_set[real],nonempty_set[real]->nonempty_set[real]]
= (LAMBDA (X,Y:nonempty_set[real]): {z:real | EXISTS (x:(X),y:(Y)): z = x+y});
-: MACRO [nonempty_set[real],nonempty_set[real]->nonempty_set[real]]
= (LAMBDA (X,Y:nonempty_set[real]): {z:real | EXISTS (x:(X),y:(Y)): z = x-y});
Arg(n0z): nonempty_set[real] = {x:real | EXISTS j: x = arg(n0z) + 2*j*pi}
Arg_def: LEMMA Arg(n0z) = {x:real | abs(n0z)*exp(x*i) = n0z}
Arg_mult: LEMMA Arg(n0x*n0y) = Arg(n0x) + Arg(n0y)
Arg_inv: LEMMA Arg(1/n0z) = -Arg(n0z)
Arg_div: LEMMA Arg(n0x/n0y) = Arg(n0x) - Arg(n0y)
END complex_sets
¤ 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.
|
