The abstract of the Mizar article:

Algebra of Vector Functions

by

Hiroshi Yamazaki, and

Yasunari Shidama

Received October 27, 1992

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;