:: Property of Complex Functions
:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999 Association of Mizar Users
:: deftheorem Def1 defines / CFUNCT_1:def 1 :
:: deftheorem Def2 defines ^ CFUNCT_1:def 2 :
theorem :: CFUNCT_1:1
canceled;
theorem :: CFUNCT_1:2
canceled;
theorem Th3: :: CFUNCT_1:3
theorem Th4: :: CFUNCT_1:4
theorem Th5: :: CFUNCT_1:5
theorem :: CFUNCT_1:6
canceled;
theorem Th7: :: CFUNCT_1:7
theorem :: CFUNCT_1:8
canceled;
theorem Th9: :: CFUNCT_1:9
Lm1:
for x, Y being set
for C being non empty set
for f being PartFunc of C, COMPLEX holds
( x in f " Y iff ( x in dom f & f /. x in Y ) )
by PARTFUN2:44;
theorem :: CFUNCT_1:10
canceled;
theorem :: CFUNCT_1:11
canceled;
theorem :: CFUNCT_1:12
canceled;
theorem :: CFUNCT_1:13
canceled;
theorem :: CFUNCT_1:14
canceled;
theorem Th15: :: CFUNCT_1:15
theorem Th16: :: CFUNCT_1:16
theorem Th17: :: CFUNCT_1:17
theorem Th18: :: CFUNCT_1:18
theorem Th19: :: CFUNCT_1:19
theorem Th20: :: CFUNCT_1:20
theorem Th21: :: CFUNCT_1:21
theorem :: CFUNCT_1:22
theorem Th23: :: CFUNCT_1:23
theorem Th24: :: CFUNCT_1:24
theorem :: CFUNCT_1:25
theorem Th26: :: CFUNCT_1:26
theorem Th27: :: CFUNCT_1:27
theorem Th28: :: CFUNCT_1:28
theorem :: CFUNCT_1:29
theorem :: CFUNCT_1:30
theorem :: CFUNCT_1:31
theorem :: CFUNCT_1:32
theorem :: CFUNCT_1:33
theorem :: CFUNCT_1:34
theorem :: CFUNCT_1:35
theorem :: CFUNCT_1:36
theorem :: CFUNCT_1:37
theorem Th38: :: CFUNCT_1:38
theorem Th39: :: CFUNCT_1:39
theorem :: CFUNCT_1:40
theorem :: CFUNCT_1:41
theorem :: CFUNCT_1:42
canceled;
theorem :: CFUNCT_1:43
theorem Th44: :: CFUNCT_1:44
theorem Th45: :: CFUNCT_1:45
theorem Th46: :: CFUNCT_1:46
Lm2:
(- 1r ) " = - 1r
by COMPLEX1:def 7;
theorem :: CFUNCT_1:47
canceled;
theorem :: CFUNCT_1:48
canceled;
theorem :: CFUNCT_1:49
theorem Th50: :: CFUNCT_1:50
theorem Th51: :: CFUNCT_1:51
theorem Th52: :: CFUNCT_1:52
theorem :: CFUNCT_1:53
theorem Th54: :: CFUNCT_1:54
theorem Th55: :: CFUNCT_1:55
theorem Th56: :: CFUNCT_1:56
theorem :: CFUNCT_1:57
theorem :: CFUNCT_1:58
theorem :: CFUNCT_1:59
theorem Th60: :: CFUNCT_1:60
theorem :: CFUNCT_1:61
theorem :: CFUNCT_1:62
theorem :: CFUNCT_1:63
theorem Th64: :: CFUNCT_1:64
theorem Th65: :: CFUNCT_1:65
theorem Th66: :: CFUNCT_1:66
theorem :: CFUNCT_1:67
theorem :: CFUNCT_1:68
theorem :: CFUNCT_1:69
theorem Th70: :: CFUNCT_1:70
theorem Th71: :: CFUNCT_1:71
theorem Th72: :: CFUNCT_1:72
theorem Th73: :: CFUNCT_1:73
theorem Th74: :: CFUNCT_1:74
theorem Th75: :: CFUNCT_1:75
theorem :: CFUNCT_1:76
theorem :: CFUNCT_1:77
theorem :: CFUNCT_1:78
theorem :: CFUNCT_1:79
theorem :: CFUNCT_1:80
Def3:
for C being non empty set
for f being PartFunc of C, COMPLEX holds
( |.f.| is bounded iff f is bounded )
theorem Th81: :: CFUNCT_1:81
theorem :: CFUNCT_1:82
theorem :: CFUNCT_1:83
theorem Th84: :: CFUNCT_1:84
theorem :: CFUNCT_1:85
theorem Th86: :: CFUNCT_1:86
theorem Th87: :: CFUNCT_1:87
theorem Th88: :: CFUNCT_1:88
theorem :: CFUNCT_1:89
theorem :: CFUNCT_1:90
theorem Th91: :: CFUNCT_1:91
theorem Th92: :: CFUNCT_1:92
theorem Th93: :: CFUNCT_1:93
theorem :: CFUNCT_1:94
theorem Th95: :: CFUNCT_1:95
theorem :: CFUNCT_1:96
theorem :: CFUNCT_1:97