:: Algebra of Complex Vector Valued Functions
:: by Noboru Endou
::
:: Received August 20, 2004
:: Copyright (c) 2004 Association of Mizar Users
definition
let M be non
empty set ;
let V be
ComplexNormSpace;
let f1,
f2 be
PartFunc of
M,the
carrier of
V;
deffunc H1(
Element of
M)
-> Element of the
carrier of
V =
(f1 /. $1) + (f2 /. $1);
deffunc H2(
Element of
M)
-> Element of the
carrier of
V =
(f1 /. $1) - (f2 /. $1);
defpred S1[
set ]
means $1
in (dom f1) /\ (dom f2);
set X =
(dom f1) /\ (dom f2);
func f1 + f2 -> PartFunc of
M,the
carrier of
V means :
Def1:
:: VFUNCT_2:def 1
(
dom it = (dom f1) /\ (dom f2) & ( for
c being
Element of
M st
c in dom it holds
it /. c = (f1 /. c) + (f2 /. c) ) );
existence
ex b1 being PartFunc of M,the carrier of V st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b1 holds
b1 /. c = (f1 /. c) + (f2 /. c) ) )
uniqueness
for b1, b2 being PartFunc of M,the carrier of V st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b1 holds
b1 /. c = (f1 /. c) + (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b2 holds
b2 /. c = (f1 /. c) + (f2 /. c) ) holds
b1 = b2
func f1 - f2 -> PartFunc of
M,the
carrier of
V means :
Def2:
:: VFUNCT_2:def 2
(
dom it = (dom f1) /\ (dom f2) & ( for
c being
Element of
M st
c in dom it holds
it /. c = (f1 /. c) - (f2 /. c) ) );
existence
ex b1 being PartFunc of M,the carrier of V st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b1 holds
b1 /. c = (f1 /. c) - (f2 /. c) ) )
uniqueness
for b1, b2 being PartFunc of M,the carrier of V st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b1 holds
b1 /. c = (f1 /. c) - (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b2 holds
b2 /. c = (f1 /. c) - (f2 /. c) ) holds
b1 = b2
end;
:: deftheorem Def1 defines + VFUNCT_2:def 1 :
:: deftheorem Def2 defines - VFUNCT_2:def 2 :
:: deftheorem Def3 defines (#) VFUNCT_2:def 3 :
:: deftheorem Def4 defines (#) VFUNCT_2:def 4 :
:: deftheorem Def5 defines ||. VFUNCT_2:def 5 :
:: deftheorem Def6 defines - VFUNCT_2:def 6 :
theorem :: VFUNCT_2:1
theorem :: VFUNCT_2:2
theorem :: VFUNCT_2:3
theorem :: VFUNCT_2:4
theorem :: VFUNCT_2:5
theorem :: VFUNCT_2:6
theorem :: VFUNCT_2:7
theorem :: VFUNCT_2:8
theorem :: VFUNCT_2:9
theorem :: VFUNCT_2:10
theorem :: VFUNCT_2:11
theorem :: VFUNCT_2:12
theorem :: VFUNCT_2:13
theorem Th14: :: VFUNCT_2:14
theorem :: VFUNCT_2:15
theorem :: VFUNCT_2:16
theorem :: VFUNCT_2:17
theorem Th18: :: VFUNCT_2:18
theorem :: VFUNCT_2:19
theorem :: VFUNCT_2:20
theorem :: VFUNCT_2:21
theorem :: VFUNCT_2:22
theorem Th23: :: VFUNCT_2:23
theorem Th24: :: VFUNCT_2:24
theorem Th25: :: VFUNCT_2:25
theorem :: VFUNCT_2:26
theorem Th27: :: VFUNCT_2:27
theorem :: VFUNCT_2:28
theorem Th29: :: VFUNCT_2:29
theorem :: VFUNCT_2:30
theorem :: VFUNCT_2:31
theorem Th32: :: VFUNCT_2:32
theorem Th33: :: VFUNCT_2:33
theorem Th34: :: VFUNCT_2:34
theorem Th35: :: VFUNCT_2:35
theorem Th36: :: VFUNCT_2:36
theorem :: VFUNCT_2:37
theorem :: VFUNCT_2:38
theorem :: VFUNCT_2:39
theorem :: VFUNCT_2:40
:: deftheorem Def7 defines is_bounded_on VFUNCT_2:def 7 :
theorem :: VFUNCT_2:41
theorem :: VFUNCT_2:42
theorem :: VFUNCT_2:43
theorem Th44: :: VFUNCT_2:44
theorem Th45: :: VFUNCT_2:45
theorem Th46: :: VFUNCT_2:46
theorem :: VFUNCT_2:47
theorem :: VFUNCT_2:48
theorem :: VFUNCT_2:49
theorem :: VFUNCT_2:50
theorem :: VFUNCT_2:51
theorem Th52: :: VFUNCT_2:52
theorem Th53: :: VFUNCT_2:53
theorem Th54: :: VFUNCT_2:54
theorem :: VFUNCT_2:55
theorem :: VFUNCT_2:56
theorem :: VFUNCT_2:57