:: Property of Complex Functions
:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, PARTFUN1, NUMBERS, RELAT_1, ARYTM_3, CARD_1,
COMPLEX1, ORDINAL4, FUNCT_1, ARYTM_1, VALUED_1, TARSKI, XXREAL_2,
XXREAL_0, FUNCT_7, REAL_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, RFUNCT_1, COMPLEX1,
VALUED_1, COMSEQ_2, SEQ_2;
constructors PARTFUN1, XXREAL_0, REAL_1, COMPLEX1, PARTFUN2, VALUED_1,
RFUNCT_1, SEQ_2, NAT_1, RELSET_1, COMSEQ_2;
registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, RFUNCT_1,
XCMPLX_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve x,y,X,Y for set;
reserve C for non empty set;
reserve c for Element of C;
reserve f,f1,f2,f3,g,g1 for PartFunc of C,COMPLEX;
reserve r1,r2,p1 for Real;
reserve r,q,cr1,cr2 for Complex;
::
::DEFINITIONS OF COMPLEX FUNCTIONS
::
definition
let C,f1,f2;
func f1/f2 -> PartFunc of C,COMPLEX means
:: CFUNCT_1:def 1
dom it = dom f1 /\ (dom f2 \ f2"{0}) &
for c st c in dom it holds it/.c = f1/.c * (f2/.c)";
end;
definition
let C,f;
func f^ -> PartFunc of C,COMPLEX means
:: CFUNCT_1:def 2
dom it = dom f \ f"{0} & for c st c in dom it holds it/.c = (f/.c)";
end;
theorem :: CFUNCT_1:1
dom (f1+f2) = dom f1 /\ dom f2 & for c st c in dom(f1+f2) holds (
f1+f2)/.c = (f1/.c) + (f2/.c);
theorem :: CFUNCT_1:2
dom (f1-f2) = dom f1 /\ dom f2 & for c st c in dom(f1-f2) holds (
f1-f2)/.c = (f1/.c) - (f2/.c);
theorem :: CFUNCT_1:3
dom(f1(#)f2)=dom f1 /\ dom f2 & for c st c in dom(f1(#)f2) holds
(f1(#)f2)/.c =(f1/.c) * (f2/.c);
theorem :: CFUNCT_1:4
dom (r(#)f) = dom f &
for c st c in dom (r(#)f) holds (r(#)f)/.c = r * (f/.c);
theorem :: CFUNCT_1:5
dom (-f) = dom f & for c st c in dom (-f) holds (-f)/.c = -f/.c;
theorem :: CFUNCT_1:6
dom (g^) c= dom g & dom g /\ (dom g \ g"{0}) = dom g \ g"{0};
theorem :: CFUNCT_1:7
dom (f1(#)f2) \ (f1(#)f2)"{0} = (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0});
theorem :: CFUNCT_1:8
c in dom (f^) implies (f/.c) <> 0;
theorem :: CFUNCT_1:9
(f^)"{0} = {};
theorem :: CFUNCT_1:10
|.f.|"{0} = f"{0} & (-f)"{0} = f"{0};
theorem :: CFUNCT_1:11
dom (f^^) = dom (f|(dom (f^)));
theorem :: CFUNCT_1:12
r<>0 implies (r(#)f)"{0} = f"{0};
begin
::
:: BASIC PROPERTIES OF OPERATIONS
::
theorem :: CFUNCT_1:13
(f1 + f2) + f3 = f1 + (f2 + f3);
theorem :: CFUNCT_1:14
(f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3);
theorem :: CFUNCT_1:15
(f1 + f2) (#) f3=f1 (#) f3 + f2 (#) f3;
theorem :: CFUNCT_1:16
f3 (#) (f1 + f2)=f3(#)f1 + f3(#)f2;
theorem :: CFUNCT_1:17
r(#)(f1(#)f2)=r(#)f1(#)f2;
theorem :: CFUNCT_1:18
r(#)(f1(#)f2)=f1(#)(r(#)f2);
theorem :: CFUNCT_1:19
(f1 - f2)(#)f3=f1(#)f3 - f2(#)f3;
theorem :: CFUNCT_1:20
f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2);
theorem :: CFUNCT_1:21
r(#)(f1 + f2) = r(#)f1 + r(#)f2;
theorem :: CFUNCT_1:22
(r*q)(#)f = r(#)(q(#)f);
theorem :: CFUNCT_1:23
r(#)(f1 - f2) = r(#)f1 - r(#)f2;
theorem :: CFUNCT_1:24
f1-f2 = (-1r)(#)(f2-f1);
theorem :: CFUNCT_1:25
f1 - (f2 + f3) = f1 - f2 - f3;
theorem :: CFUNCT_1:26
1r(#)f = f;
theorem :: CFUNCT_1:27
f1 - (f2 - f3) = f1 - f2 + f3;
theorem :: CFUNCT_1:28
f1 + (f2 - f3) =f1 + f2 - f3;
theorem :: CFUNCT_1:29
|.f1(#)f2.| = |.f1.|(#)|.f2.|;
theorem :: CFUNCT_1:30
|.r(#)f.| = |.r.|(#)|.f.|;
theorem :: CFUNCT_1:31
-f = (-1r)(#)f;
::$CT
theorem :: CFUNCT_1:33
f1 - (-f2) = f1 + f2;
theorem :: CFUNCT_1:34
f^^ = f|(dom (f^));
theorem :: CFUNCT_1:35
(f1(#)f2)^ = (f1^)(#)(f2^);
theorem :: CFUNCT_1:36
r<>0 implies (r(#)f)^ = r" (#) (f^);
theorem :: CFUNCT_1:37
(-f)^ = (-1r)(#)(f^);
theorem :: CFUNCT_1:38
|.f.|^ = |. f^ .|;
theorem :: CFUNCT_1:39
f/g = f(#) (g^);
theorem :: CFUNCT_1:40
r(#)(g/f) = (r(#)g)/f;
theorem :: CFUNCT_1:41
(f/g)(#)g = (f|dom(g^));
theorem :: CFUNCT_1:42
(f/g)(#)(f1/g1) = (f(#)f1)/(g(#)g1);
theorem :: CFUNCT_1:43
(f1/f2)^ = (f2|dom(f2^))/f1;
theorem :: CFUNCT_1:44
g (#) (f1/f2) = (g (#) f1)/f2;
theorem :: CFUNCT_1:45
g/(f1/f2) = (g(#)(f2|dom(f2^)))/f1;
theorem :: CFUNCT_1:46
-f/g = (-f)/g & f/(-g) = -f/g;
theorem :: CFUNCT_1:47
f1/f + f2/f = (f1 + f2)/f & f1/f - f2/f = (f1 - f2)/f;
theorem :: CFUNCT_1:48
f1/f + g1/g = (f1(#)g + g1(#)f)/(f(#)g);
theorem :: CFUNCT_1:49
(f/g)/(f1/g1) = (f(#)(g1|dom(g1^)))/(g(#)f1);
theorem :: CFUNCT_1:50
f1/f - g1/g = (f1(#)g - g1(#)f)/(f(#)g);
theorem :: CFUNCT_1:51
|.f1/f2.| = |.f1.|/|.f2.|;
theorem :: CFUNCT_1:52
(f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X;
theorem :: CFUNCT_1:53
(f1(#)f2)|X = f1|X (#) f2|X & (f1(#)f2)|X = f1|X (#) f2 & (f1(#)
f2)|X = f1 (#) f2|X;
theorem :: CFUNCT_1:54
(-f)|X = -(f|X) & (f^)|X = (f|X)^ & (|.f.|)|X = |.(f|X).|;
theorem :: CFUNCT_1:55
(f1-f2)|X = f1|X - f2|X & (f1-f2)|X = f1|X - f2 &(f1-f2)|X = f1 - f2|X;
theorem :: CFUNCT_1:56
(f1/f2)|X = f1|X / f2|X & (f1/f2)|X = f1|X / f2 &(f1/f2)|X = f1 / f2|X;
theorem :: CFUNCT_1:57
(r(#)f)|X = r(#)(f|X);
begin
::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN, TO COMPLEX
::
theorem :: CFUNCT_1:58
(f1 is total & f2 is total iff f1+f2 is total) & (f1 is total &
f2 is total iff f1-f2 is total) & (f1 is total & f2 is total iff f1(#)f2 is
total);
theorem :: CFUNCT_1:59
f is total iff r(#)f is total;
theorem :: CFUNCT_1:60
f is total iff -f is total;
theorem :: CFUNCT_1:61
f is total iff |.f.| is total;
theorem :: CFUNCT_1:62
f^ is total iff f"{0} = {} & f is total;
theorem :: CFUNCT_1:63
f1 is total & f2"{0} = {} & f2 is total iff f1/f2 is total;
theorem :: CFUNCT_1:64
f1 is total & f2 is total implies (f1+f2)/.c = ((f1/.c)) + ((f2/.c)) &
(f1-f2)/.c = ((f1/.c)) - ((f2/.c)) & (f1(#) f2)/.c = ((f1/.c)) * ((f2/.c));
theorem :: CFUNCT_1:65
f is total implies (r(#)f)/.c = r * ((f/.c));
theorem :: CFUNCT_1:66
f is total implies (-f)/.c = - (f/.c) & (|.f.|).c = |. (f/.c) .|;
theorem :: CFUNCT_1:67
f^ is total implies (f^)/.c = ((f/.c))";
theorem :: CFUNCT_1:68
f1 is total & f2^ is total implies (f1/f2)/.c = ((f1/.c)) *(((f2/.c))) ";
begin
theorem :: CFUNCT_1:69
f|Y is bounded iff ex p be Real st for c st c in Y /\ dom
f holds |.(f/.c).|<= p;
theorem :: CFUNCT_1:70
Y c= X & f|X is bounded implies f|Y is bounded;
theorem :: CFUNCT_1:71
X misses dom f implies f|X is bounded;
theorem :: CFUNCT_1:72
f|Y is bounded implies (r(#)f)|Y is bounded;
theorem :: CFUNCT_1:73
|.f.||X is bounded_below;
theorem :: CFUNCT_1:74
f|Y is bounded implies |.f.||Y is bounded & (-f)|Y is bounded;
theorem :: CFUNCT_1:75
f1|X is bounded & f2|Y is bounded implies (f1+f2)|(X /\ Y) is bounded;
theorem :: CFUNCT_1:76
f1|X is bounded & f2|Y is bounded implies (f1(#)f2)|(X /\ Y) is
bounded & (f1-f2)|(X /\ Y) is bounded;
theorem :: CFUNCT_1:77
f|X is bounded & f|Y is bounded implies f|(X \/ Y) is bounded;
theorem :: CFUNCT_1:78
f1|X is constant & f2|Y is constant implies (f1+f2)|(X /\ Y) is
constant & (f1-f2)|(X /\ Y) is constant & (f1(#)f2)|(X /\ Y) is constant;
theorem :: CFUNCT_1:79
f|Y is constant implies (q(#)f)|Y is constant;
theorem :: CFUNCT_1:80
f|Y is constant implies |.f.||Y is constant & (-f)|Y is constant;
theorem :: CFUNCT_1:81
f|Y is constant implies f|Y is bounded;
theorem :: CFUNCT_1:82
f|Y is constant implies (for r holds (r(#)f)|Y is bounded) & (-f)|Y is
bounded & |.f.||Y is bounded;
theorem :: CFUNCT_1:83
f1|X is bounded & f2|Y is constant implies (f1+f2)|(X /\ Y) is bounded;
theorem :: CFUNCT_1:84
f1|X is bounded & f2|Y is constant implies (f1-f2)|(X /\ Y) is bounded
& (f2-f1)|(X /\ Y) is bounded & (f1(#)f2)|(X /\ Y) is bounded;
theorem :: CFUNCT_1:85
|.f.| is bounded iff f is bounded;
registration let D be non empty set; let f be Function of COMPLEX,D;
let c be Complex;
identify f/.c with f.c;
end;