The abstract of the Mizar article:

Functional Sequence from a Domain to a Domain

by

Beata Perkowska

Received May 22, 1992

MML identifier: SEQFUNC

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, PARTFUN1, BOOLE, SEQ_1, FINSEQ_1, ARYTM_1,
      ABSVALUE, ARYTM_3, TDGROUP, SEQ_2, ORDINAL2, FCONT_1, SQUARE_1, SEQFUNC,
      ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      NAT_1, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, RFUNCT_1, ABSVALUE,
      SEQ_1, SEQ_2, FCONT_1, LIMFUNC1;
 constructors REAL_1, PARTFUN1, RFUNCT_1, ABSVALUE, SEQ_2, FCONT_1, LIMFUNC1,
      MEMBERED, XBOOLE_0;
 clusters RELSET_1, XREAL_0, SEQ_1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS,
      ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve D,D1,D2 for non empty set,
         x,y,z for set,
         n,k for Nat,
         p,x1,r for Real,
         f for Function;

definition let D1,D2;
mode Functional_Sequence of D1,D2 -> Function means
:: SEQFUNC:def 1
dom it = NAT & rng it c= PFuncs(D1,D2);
end;

reserve F,F1,F2 for Functional_Sequence of D1,D2;

definition let D1,D2,F,n;
 redefine func F.n -> PartFunc of D1,D2;
end;

reserve G,H,H1,H2,J for Functional_Sequence of D,REAL;

theorem :: SEQFUNC:1
  f is Functional_Sequence of D1,D2 iff
(dom f = NAT & for n holds f.n is PartFunc of D1,D2);

theorem :: SEQFUNC:2
for F1,F2 st (for n holds F1.n = F2.n) holds F1 = F2;

scheme ExFuncSeq{D1() -> non empty set, D2() -> non empty set,
                 F(Nat)->PartFunc of D1(),D2()}:
ex G being Functional_Sequence of D1(), D2() st for n holds G.n = F(n);

definition
 let D,H,r;
 func r(#)H ->Functional_Sequence of D,REAL means
:: SEQFUNC:def 2
   for n holds it.n = r(#)(H.n);
end;

definition
 let D,H;
 func H" -> Functional_Sequence of D,REAL means
:: SEQFUNC:def 3
  for n holds it.n=(H.n)^;

func - H -> Functional_Sequence of D,REAL means
:: SEQFUNC:def 4
 for n holds it.n = -H.n;

func abs(H)->Functional_Sequence of D,REAL means
:: SEQFUNC:def 5
   for n holds it.n=abs(H.n);
end;

definition
 let D,G,H;
func G + H -> Functional_Sequence of D,REAL means
:: SEQFUNC:def 6
   for n holds it.n = G.n + H.n;
end;

definition
 let D,G,H;
func G - H -> Functional_Sequence of D,REAL equals
:: SEQFUNC:def 7
  G + -H;
end;

definition
 let D,G,H;
func G (#) H -> Functional_Sequence of D,REAL means
:: SEQFUNC:def 8
  for n holds it.n =G.n (#) H.n;
end;

definition
 let D,H,G;
func G / H ->Functional_Sequence of D,REAL equals
:: SEQFUNC:def 9
  G (#) (H");
end;

theorem :: SEQFUNC:3
  H1 = G/H iff for n holds H1.n = G.n / H.n;

theorem :: SEQFUNC:4
H1 = G - H iff for n holds H1.n = G.n - H.n;

theorem :: SEQFUNC:5
  G + H = H + G & (G + H) + J = G + (H + J);

theorem :: SEQFUNC:6
G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J);

theorem :: SEQFUNC:7
  (G + H) (#) J = G(#)J + H(#)J &
J (#) (G + H) = J(#)G + J(#)H;

theorem :: SEQFUNC:8
-H = (-1)(#)H;

theorem :: SEQFUNC:9
  (G - H) (#) J = G(#)J - H(#)J &
J(#)G - J(#)H = J (#) (G - H);

theorem :: SEQFUNC:10
  r(#)(G + H) = r(#)G + r(#)H & r(#)(G - H) = r(#)G - r(#)H;

theorem :: SEQFUNC:11
(r*p)(#)H = r(#)(p(#)H);

theorem :: SEQFUNC:12
1 (#) H = H;

theorem :: SEQFUNC:13
  -(-H) = H;

theorem :: SEQFUNC:14
  G" (#) H" = (G(#)H)";

theorem :: SEQFUNC:15
  r<>0 implies (r(#)H)" = r" (#) H";

theorem :: SEQFUNC:16
abs(H)"=abs(H");

theorem :: SEQFUNC:17
abs(G(#)H) = abs(G) (#) abs(H);

theorem :: SEQFUNC:18
  abs(G/H) = abs(G) / abs(H);

theorem :: SEQFUNC:19
  abs(r(#)H) = abs(r) (#) abs(H);

 reserve x for Element of D,
         X,Y for set,
         S1,S2 for Real_Sequence,
         f for PartFunc of D,REAL;

definition let D1,D2,F,X;
 pred X common_on_dom F means
:: SEQFUNC:def 10
  X <> {} & for n holds X c= dom (F.n);
 end;

definition let D,H,x;
 func H#x ->Real_Sequence means
:: SEQFUNC:def 11
 for n holds it.n = (H.n).x;
end;

definition let D,H,X;
 pred H is_point_conv_on X means
:: SEQFUNC:def 12
  X common_on_dom H & ex f st X = dom f &
  for x st x in X holds for p st p>0 ex k st
               for n st n>=k holds abs((H.n).x - f.x) < p;
 end;

theorem :: SEQFUNC:20
H is_point_conv_on X iff
X common_on_dom H &
 ex f st X = dom f &
         for x st x in X holds (H#x) is convergent & lim(H#x) = f.x;

theorem :: SEQFUNC:21
H is_point_conv_on X iff X common_on_dom H &
                             for x st x in X holds (H#x) is convergent;

definition let D,H,X;
 pred H is_unif_conv_on X means
:: SEQFUNC:def 13
  X common_on_dom H &
  ex f st X = dom f & for p st p>0 ex k st
     for n,x st n>=k & x in X holds abs((H.n).x - f.x) < p;
 end;

definition let D,H,X;
 assume  H is_point_conv_on X;
 func lim(H,X) -> PartFunc of D,REAL means
:: SEQFUNC:def 14
 dom it = X & for x st x in dom it holds it.x = lim(H#x);
end;

theorem :: SEQFUNC:22
H is_point_conv_on X implies
(f = lim(H,X) iff dom f = X &
for x st x in X holds
   for p st p>0 ex k st for n st n>=k holds abs((H.n).x - f.x) < p);

theorem :: SEQFUNC:23
H is_unif_conv_on X implies H is_point_conv_on X;

theorem :: SEQFUNC:24
Y c= X & Y<>{} & X common_on_dom H implies Y common_on_dom H;

theorem :: SEQFUNC:25
  Y c= X & Y<>{} & H is_point_conv_on X implies H is_point_conv_on Y &
lim(H,X)|Y = lim(H,Y);

theorem :: SEQFUNC:26
  Y c= X & Y<>{} & H is_unif_conv_on X implies H is_unif_conv_on Y;

theorem :: SEQFUNC:27
X common_on_dom H implies for x st x in X holds {x} common_on_dom H;

theorem :: SEQFUNC:28
  H is_point_conv_on X implies for x st x in X holds {x} common_on_dom H;

theorem :: SEQFUNC:29
{x} common_on_dom H1 & {x} common_on_dom H2 implies
H1#x + H2#x = (H1+H2)#x &
H1#x - H2#x = (H1-H2)#x &
(H1#x) (#) (H2#x) = (H1(#)H2)#x;

theorem :: SEQFUNC:30
{x} common_on_dom H implies (abs(H))#x = abs(H#x) & (-H)#x = -(H#x);

theorem :: SEQFUNC:31
{x} common_on_dom H implies (r(#)H)#x = r(#)(H#x);

theorem :: SEQFUNC:32
X common_on_dom H1 & X common_on_dom H2 implies
for x st x in X holds H1#x + H2#x = (H1+H2)#x &
                   H1#x - H2#x = (H1-H2)#x &
                   (H1#x) (#) (H2#x) = (H1(#)H2)#x;

theorem :: SEQFUNC:33
X common_on_dom H implies
for x st x in X holds abs(H)#x = abs(H#x) & (-H)#x = -(H#x);

theorem :: SEQFUNC:34
X common_on_dom H implies
for x st x in X holds (r(#)H)#x = r(#)(H#x);

theorem :: SEQFUNC:35
H1 is_point_conv_on X & H2 is_point_conv_on X implies
for x st x in X holds H1#x + H2#x = (H1+H2)#x &
                   H1#x - H2#x = (H1-H2)#x &
                   (H1#x) (#) (H2#x) = (H1(#)H2)#x;

theorem :: SEQFUNC:36
H is_point_conv_on X implies
for x st x in X holds abs(H)#x = abs(H#x) & (-H)#x = -(H#x);


theorem :: SEQFUNC:37
  H is_point_conv_on X implies
for x st x in X holds (r(#)H)#x = r(#)(H#x);

theorem :: SEQFUNC:38
X common_on_dom H1 & X common_on_dom H2 implies
X common_on_dom H1+H2 & X common_on_dom H1-H2 & X common_on_dom H1(#)H2;

theorem :: SEQFUNC:39
X common_on_dom H implies X common_on_dom abs(H) & X common_on_dom (-H);

theorem :: SEQFUNC:40
X common_on_dom H implies X common_on_dom r(#)H;

theorem :: SEQFUNC:41
  H1 is_point_conv_on X & H2 is_point_conv_on X implies
H1+H2 is_point_conv_on X & lim(H1+H2,X) = lim(H1,X) + lim(H2,X) &
H1-H2 is_point_conv_on X & lim(H1-H2,X) = lim(H1,X) - lim(H2,X) &
H1(#)H2 is_point_conv_on X & lim(H1(#)H2,X) = lim(H1,X) (#) lim(H2,X);

theorem :: SEQFUNC:42
  H is_point_conv_on X implies
abs(H) is_point_conv_on X & lim (abs(H),X) = abs( lim (H,X) ) &
-H is_point_conv_on X & lim (-H,X) = - lim(H,X);

theorem :: SEQFUNC:43
  H is_point_conv_on X implies
r(#)H is_point_conv_on X & lim (r(#)H,X) = r(#)(lim(H,X));

theorem :: SEQFUNC:44
H is_unif_conv_on X iff X common_on_dom H & H is_point_conv_on X &
for r st 0<r ex k st for n,x st n>=k & x in X holds abs((H.n).x-(lim(H,X)).x)<r
;

 reserve H for Functional_Sequence of REAL,REAL;

theorem :: SEQFUNC:45
  H is_unif_conv_on X & (for n holds H.n is_continuous_on X) implies
lim(H,X) is_continuous_on X;