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

Functional Sequence from a Domain to a Domain

by
Beata Perkowska

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;