Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Algebra of Vector Functions

by
Hiroshi Yamazaki, and
Yasunari Shidama

MML identifier: VFUNCT_1
[ Mizar article, MML identifier index ]

```environ

vocabulary NORMSP_1, PARTFUN1, RELAT_1, BOOLE, ARYTM_1, SEQ_1, FUNCT_1,
RLVECT_1, ABSVALUE, RFUNCT_1, PARTFUN2, FINSEQ_4, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1,
STRUCT_0, ABSVALUE, FINSEQ_4, RELSET_1, PARTFUN1, PARTFUN2, RLVECT_1,
NORMSP_1, SEQ_1, RFUNCT_1;
constructors REAL_1, ABSVALUE, FINSEQ_4, PARTFUN1, PARTFUN2, NORMSP_1,
RFUNCT_1, SEQ_1, MEMBERED, XBOOLE_0;
clusters RELSET_1, STRUCT_0, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve x,X,Y for set;
reserve C for non empty set;
reserve c for Element of C;
reserve V for RealNormSpace;
reserve f,f1,f2,f3 for PartFunc of C,the carrier of V;
reserve r,r1,r2,p for Real;

::
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF REAL NUMBERS
::

definition let C;let V;let f1,f2;
func f1+f2 -> PartFunc of C,the carrier of V means
:: VFUNCT_1:def 1
dom it = dom f1 /\ dom f2 &
for c st c in dom it holds it/.c = (f1/.c) + (f2/.c);

func f1-f2 -> PartFunc of C,the carrier of V means
:: VFUNCT_1:def 2
dom it = dom f1 /\ dom f2 &
for c st c in dom it holds it/.c = (f1/.c) - (f2/.c);
end;

definition let C;let V;let f1 be PartFunc of C,REAL;let f2;
func f1(#)f2 -> PartFunc of C,the carrier of V means
:: VFUNCT_1:def 3
dom it = dom f1 /\ dom f2 & for c st c in dom it holds it/.c = f1.c * (f2/.c);
end;

definition let C;let V;let f,r;
func r(#)f -> PartFunc of C,the carrier of V means
:: VFUNCT_1:def 4
dom it = dom f & for c st c in dom it holds it/.c = r * (f/.c);
end;

definition let C;let V; let f;
func ||.f.|| -> PartFunc of C,REAL means
:: VFUNCT_1:def 5
dom it = dom f & for c st c in dom it holds it.c = ||. f/.c .||;

func -f ->PartFunc of C,the carrier of V means
:: VFUNCT_1:def 6
dom it = dom f & for c st c in dom it holds it/.c = -(f/.c);
end;

canceled 6;

theorem :: VFUNCT_1:7
for f1 be PartFunc of C,REAL holds
dom (f1(#)f2) \ (f1(#)f2)"{0.V} =
(dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V});

theorem :: VFUNCT_1:8
(||.f.||)"{0} = f"{0.V} & (-f)"{0.V} = f"{0.V};

theorem :: VFUNCT_1:9
r<>0 implies (r(#)f)"{0.V} = f"{0.V};

::
:: BASIC PROPERTIES OF OPERATIONS
::

theorem :: VFUNCT_1:10
f1 + f2 = f2 + f1;

theorem :: VFUNCT_1:11
(f1 + f2) + f3 = f1 + (f2 + f3);

theorem :: VFUNCT_1:12
for f1,f2 be PartFunc of C,REAL,f3 be PartFunc of C,the carrier of V
holds
(f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3);

theorem :: VFUNCT_1:13
for f1,f2 be PartFunc of C,REAL holds
(f1 + f2) (#) f3=f1 (#) f3 + f2 (#) f3;

theorem :: VFUNCT_1:14
for f3 be PartFunc of C,REAL holds
f3 (#) (f1 + f2)=f3(#)f1 + f3(#)f2;

theorem :: VFUNCT_1:15
for f1 be PartFunc of C,REAL holds
r(#)(f1(#)f2)=r(#)f1(#)f2;

theorem :: VFUNCT_1:16
for f1 be PartFunc of C,REAL holds
r(#)(f1(#)f2)=f1(#)(r(#)f2);

theorem :: VFUNCT_1:17
for f1,f2 be PartFunc of C,REAL holds
(f1 - f2)(#)f3=f1(#)f3 - f2(#)f3;

theorem :: VFUNCT_1:18
for f3 be PartFunc of C,REAL holds
f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2);

theorem :: VFUNCT_1:19
r(#)(f1 + f2) = r(#)f1 + r(#)f2;

theorem :: VFUNCT_1:20
(r*p)(#)f = r(#)(p(#)f);

theorem :: VFUNCT_1:21
r(#)(f1 - f2) = r(#)f1 - r(#)f2;

theorem :: VFUNCT_1:22
f1-f2 = (-1)(#)(f2-f1);

theorem :: VFUNCT_1:23
f1 - (f2 + f3) = f1 - f2 - f3;

theorem :: VFUNCT_1:24
1(#)f = f;

theorem :: VFUNCT_1:25
f1 - (f2 - f3) = f1 - f2 + f3;

theorem :: VFUNCT_1:26
f1 + (f2 - f3) = f1 + f2 - f3;

theorem :: VFUNCT_1:27
for f1 be PartFunc of C,REAL holds
||.f1(#)f2.|| = abs(f1)(#)||.f2.||;

theorem :: VFUNCT_1:28
||.r(#)f.|| = abs(r)(#)||.f.||;

theorem :: VFUNCT_1:29
-f = (-1)(#)f;

theorem :: VFUNCT_1:30
-(-f) = f;

theorem :: VFUNCT_1:31
f1 - f2 = f1 + -f2;

theorem :: VFUNCT_1:32
f1 - (-f2) = f1 + f2;

theorem :: VFUNCT_1:33
(f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X;

theorem :: VFUNCT_1:34
for f1 be PartFunc of C,REAL holds
(f1(#)f2)|X = f1|X (#) f2|X & (f1(#)f2)|X = f1|X (#) f2 &
(f1(#)f2)|X = f1 (#) f2|X;

theorem :: VFUNCT_1:35
(-f)|X = -(f|X) & (||.f.||)|X = ||.(f|X).||;

theorem :: VFUNCT_1:36
(f1-f2)|X = f1|X - f2|X & (f1-f2)|X = f1|X - f2 &(f1-f2)|X = f1 - f2|X;

theorem :: VFUNCT_1:37
(r(#)f)|X = r(#)(f|X);

::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO REAL
::

theorem :: VFUNCT_1:38
(f1 is total & f2 is total iff f1+f2 is total) &
(f1 is total & f2 is total iff f1-f2 is total);

theorem :: VFUNCT_1:39
for f1 be PartFunc of C,REAL holds
(f1 is total & f2 is total iff f1(#)f2 is total);

theorem :: VFUNCT_1:40
f is total iff r(#)f is total;

theorem :: VFUNCT_1:41
f is total iff -f is total;

theorem :: VFUNCT_1:42
f is total iff ||.f.|| is total;

theorem :: VFUNCT_1:43
f1 is total & f2 is total implies (f1+f2)/.c = (f1/.c) + (f2/.c) &
(f1-f2)/.c = (f1/.c) - (f2/.c);

theorem :: VFUNCT_1:44
for f1 be PartFunc of C,REAL holds
f1 is total & f2 is total implies (f1(#)f2)/.c = f1.c * (f2/.c);

theorem :: VFUNCT_1:45
f is total implies (r(#)f)/.c = r * (f/.c);

theorem :: VFUNCT_1:46
f is total implies (-f)/.c = - f/.c & (||.f.||).c = ||. f/.c .||;

::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN TO A NORMED REAL SPACE
::

definition let C; let V; let f,Y;
pred f is_bounded_on Y means
:: VFUNCT_1:def 7
ex r st for c st c in Y /\ dom f holds ||.f/.c.|| <= r;
end;

canceled;

theorem :: VFUNCT_1:48
Y c= X & f is_bounded_on X implies f is_bounded_on Y;

theorem :: VFUNCT_1:49
X misses dom f implies f is_bounded_on X;

theorem :: VFUNCT_1:50
0(#)f is_bounded_on Y;

theorem :: VFUNCT_1:51
f is_bounded_on Y implies r(#)f is_bounded_on Y;

theorem :: VFUNCT_1:52
f is_bounded_on Y implies ||.f.|| is_bounded_on Y & -f is_bounded_on Y;

theorem :: VFUNCT_1:53
f1 is_bounded_on X & f2 is_bounded_on Y implies
f1+f2 is_bounded_on (X /\ Y);

theorem :: VFUNCT_1:54
for f1 be PartFunc of C,REAL holds
f1 is_bounded_on X & f2 is_bounded_on Y implies
f1(#)f2 is_bounded_on (X /\ Y);

theorem :: VFUNCT_1:55
f1 is_bounded_on X & f2 is_bounded_on Y implies
f1-f2 is_bounded_on X /\ Y;

theorem :: VFUNCT_1:56
f is_bounded_on X & f is_bounded_on Y implies
f is_bounded_on X \/ Y;

theorem :: VFUNCT_1:57
f1 is_constant_on X & f2 is_constant_on Y implies
(f1 + f2) is_constant_on (X /\ Y) &
(f1 - f2) is_constant_on (X /\ Y);

theorem :: VFUNCT_1:58
for f1 be PartFunc of C,REAL holds
f1 is_constant_on X & f2 is_constant_on Y implies
(f1 (#) f2) is_constant_on (X /\ Y);

theorem :: VFUNCT_1:59
f is_constant_on Y implies p(#)f is_constant_on Y;

theorem :: VFUNCT_1:60
f is_constant_on Y implies ||.f.|| is_constant_on Y &
-f is_constant_on Y;

theorem :: VFUNCT_1:61
f is_constant_on Y implies f is_bounded_on Y;

theorem :: VFUNCT_1:62
f is_constant_on Y implies (for r holds r(#)f is_bounded_on Y) &
(-f is_bounded_on Y) &
||.f.|| is_bounded_on Y;

theorem :: VFUNCT_1:63
f1 is_bounded_on X & f2 is_constant_on Y implies
f1+f2 is_bounded_on (X /\ Y);

theorem :: VFUNCT_1:64
f1 is_bounded_on X & f2 is_constant_on Y implies
f1-f2 is_bounded_on X /\ Y &
f2-f1 is_bounded_on X /\ Y;
```