:: Continuous Functions on Real and Complex Normed Linear Spaces
:: by Noboru Endou
::
:: Received August 20, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, XCMPLX_0, CLVECT_1, NORMSP_1, NAT_1,
ARYTM_1, ARYTM_3, COMPLEX1, RELAT_1, FUNCT_1, PARTFUN1, STRUCT_0,
PRE_TOPC, RCOMP_1, CARD_1, TARSKI, XXREAL_0, SUPINF_2, VALUED_0, SEQ_2,
ORDINAL2, FCONT_1, FUNCT_2, XBOOLE_0, VALUED_1, CFCONT_1, COMSEQ_1,
SEQ_1, SEQ_4, NFCONT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
PARTFUN2, FUNCT_2, PRE_TOPC, XREAL_0, ORDINAL1, NUMBERS, XCMPLX_0,
COMPLEX1, REAL_1, NAT_1, RLVECT_1, SEQ_1, SEQ_2, VALUED_0, SEQ_4,
VFUNCT_1, COMSEQ_1, CFCONT_1, RCOMP_1, COMSEQ_2, STRUCT_0, VFUNCT_2,
CLVECT_1, NFCONT_1, XXREAL_0, NORMSP_0, NORMSP_1;
constructors REAL_1, SEQ_4, RCOMP_1, PARTFUN2, COMSEQ_2, COMSEQ_3, CFCONT_1,
NFCONT_1, VFUNCT_2, SEQ_2, RELSET_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, NAT_1, STRUCT_0,
VALUED_0, XREAL_0, VFUNCT_1, FUNCT_2, XCMPLX_0;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, NFCONT_1;
equalities RELAT_1;
expansions TARSKI, NFCONT_1;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1,
ZFMISC_1, RCOMP_1, SEQ_2, RELAT_1, FUNCT_1, VFUNCT_1, LOPBAN_1, FUNCT_2,
SEQ_4, NORMSP_1, PARTFUN1, PARTFUN2, CLVECT_1, COMSEQ_2, VFUNCT_2,
NFCONT_1, CLOPBAN1, CFCONT_1, COMPLEX1, XREAL_1, XXREAL_0, BHSP_1,
VALUED_0, NORMSP_0, ORDINAL1;
schemes FUNCT_2;
begin :: Continuous Function on Normed Complex Linear Spaces
reserve n,m for Element of NAT;
reserve r,s for Real;
reserve z for Complex;
reserve CNS,CNS1,CNS2 for ComplexNormSpace;
reserve RNS for RealNormSpace;
theorem Th1:
for seq be sequence of CNS holds -seq=(-1r)*seq
proof
let seq be sequence of CNS;
now
let n;
thus ((-1r)*seq).n =(-1r)*seq.n by CLVECT_1:def 14
.=-seq.n by CLVECT_1:3
.=(-seq).n by BHSP_1:44;
end;
hence thesis by FUNCT_2:63;
end;
definition
let CNS;
let x0 be Point of CNS;
mode Neighbourhood of x0 -> Subset of CNS means
:Def1:
ex g be Real st 0<g &
{y where y is Point of CNS: ||.y-x0 .|| < g} c= it;
existence
proof
set N= {y where y is Point of CNS : ||.y-x0 .|| < 1};
take N;
N c= the carrier of CNS
proof
let x be object;
assume x in {y where y is Point of CNS : ||.y-x0 .|| < 1};
then ex y be Point of CNS st x=y & ||.y-x0 .|| < 1;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th2:
for x0 be Point of CNS for g be Real st 0 < g holds {y where y is
Point of CNS: ||.y-x0 .|| < g} is Neighbourhood of x0
proof
let x0 be Point of CNS;
let g be Real such that
A1: g >0;
set N= {y where y is Point of CNS : ||.y-x0 .|| < g};
N c= the carrier of CNS
proof
let x be object;
assume x in {y where y is Point of CNS : ||.y-x0 .|| < g};
then ex y be Point of CNS st x=y & ||.y-x0 .|| < g;
hence thesis;
end;
hence thesis by A1,Def1;
end;
theorem Th3:
for x0 be Point of CNS for N being Neighbourhood of x0 holds x0 in N
proof
let x0 be Point of CNS;
let N be Neighbourhood of x0;
consider g be Real such that
A1: 0<g and
A2: {z where z is Point of CNS : ||.z-x0 .|| < g} c= N by Def1;
||.x0-x0 .|| = ||.0.CNS.|| by RLVECT_1:15
.=0 by CLVECT_1:102;
then x0 in {z where z is Point of CNS : ||.z-x0 .|| < g} by A1;
hence thesis by A2;
end;
definition
let CNS;
let X be Subset of CNS;
attr X is compact means
for s1 be sequence of CNS st rng s1 c= X ex
s2 be sequence of CNS st s2 is subsequence of s1 & s2 is convergent & lim s2 in
X;
end;
definition
let CNS;
let X be Subset of CNS;
attr X is closed means
for s1 be sequence of CNS st rng s1 c= X & s1 is
convergent holds lim s1 in X;
end;
definition
let CNS;
let X be Subset of CNS;
attr X is open means
X` is closed;
end;
definition
let CNS1,CNS2;
let f be PartFunc of CNS1,CNS2;
let x0 be Point of CNS1;
pred f is_continuous_in x0 means
x0 in dom f & for seq be sequence
of CNS1 st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
convergent & f/.x0 = lim (f/*seq);
end;
definition
let CNS,RNS;
let f be PartFunc of CNS,RNS;
let x0 be Point of CNS;
pred f is_continuous_in x0 means
x0 in dom f & for seq be sequence
of CNS st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
convergent & f/.x0 = lim (f/*seq);
end;
definition
let RNS;
let CNS;
let f be PartFunc of RNS,CNS;
let x0 be Point of RNS;
pred f is_continuous_in x0 means
x0 in dom f & for seq be sequence
of RNS st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
convergent & f/.x0 = lim (f/*seq);
end;
definition
let CNS;
let f be PartFunc of the carrier of CNS,COMPLEX;
let x0 be Point of CNS;
pred f is_continuous_in x0 means
x0 in dom f & for seq be sequence
of CNS st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
convergent & f/.x0 = lim (f/*seq);
end;
definition
let CNS;
let f be PartFunc of the carrier of CNS,REAL;
let x0 be Point of CNS;
pred f is_continuous_in x0 means
x0 in dom f & for seq be sequence
of CNS st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
convergent & f/.x0 = lim (f/*seq);
end;
definition
let RNS;
let f be PartFunc of the carrier of RNS,COMPLEX;
let x0 be Point of RNS;
pred f is_continuous_in x0 means
x0 in dom f & for seq be sequence
of RNS st rng seq c= dom f & seq is convergent & lim seq = x0 holds f/*seq is
convergent & f/.x0 = lim (f/*seq);
end;
theorem Th4:
for n being Nat
for seq be sequence of CNS1, h be PartFunc of CNS1,CNS2 st rng
seq c= dom h
holds seq.n in dom h
proof
let n be Nat;
let seq be sequence of CNS1;
let h be PartFunc of CNS1,CNS2;
n in NAT by ORDINAL1:def 12;
then
A1: n in dom seq by FUNCT_2:def 1;
assume rng seq c= dom h;
then n in dom ((h qua Function)*seq) by A1,RELAT_1:27;
hence thesis by FUNCT_1:11;
end;
theorem Th5:
for n being Nat
for seq be sequence of CNS, h be PartFunc of CNS,RNS st rng seq
c= dom h holds seq.n in dom h
proof let n be Nat;
let seq be sequence of CNS;
let h be PartFunc of CNS,RNS;
n in NAT by ORDINAL1:def 12;
then
A1: n in dom seq by FUNCT_2:def 1;
assume rng seq c= dom h;
then n in dom ((h qua Function)*seq) by A1,RELAT_1:27;
hence thesis by FUNCT_1:11;
end;
theorem Th6:
for n being Nat
for seq be sequence of RNS, h be PartFunc of RNS,CNS st rng seq
c= dom h holds seq.n in dom h
proof let n be Nat;
let seq be sequence of RNS;
let h be PartFunc of RNS,CNS;
n in NAT by ORDINAL1:def 12;
then
A1: n in dom seq by FUNCT_2:def 1;
assume rng seq c= dom h;
then n in dom ((h qua Function)*seq) by A1,RELAT_1:27;
hence thesis by FUNCT_1:11;
end;
theorem Th7:
for seq be sequence of CNS, x be set holds x in rng seq
iff ex n being Nat st x = seq.n
proof
let seq be sequence of CNS;
let x be set;
thus x in rng seq implies ex n being Nat st x = seq.n
proof
assume x in rng seq;
then consider y be object such that
A1: y in dom seq and
A2: x = seq.y by FUNCT_1:def 3;
reconsider m=y as Element of NAT by A1;
take m;
thus thesis by A2;
end;
given n being Nat such that
A3: x = seq.n;
n in NAT by ORDINAL1:def 12;
then n in dom seq by FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:def 3;
end;
theorem Th8:
for f be PartFunc of CNS1,CNS2, x0 be Point of CNS1 holds f
is_continuous_in x0 iff x0 in dom f & for r st 0<r ex s st 0<s & for x1 be
Point of CNS1 st x1 in dom f & ||. x1- x0 .|| <s holds ||. f/.x1-f/.x0 .||<r
proof
let f be PartFunc of CNS1,CNS2;
let x0 be Point of CNS1;
thus f is_continuous_in x0 implies x0 in dom f & for r st 0<r ex s st 0<s &
for x1 be Point of CNS1 st x1 in dom f & ||. x1- x0 .|| <s holds ||. f/.x1- f/.
x0 .|| <r
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
given r such that
A2: 0<r and
A3: for s holds not 0<s or ex x1 be Point of CNS1 st x1 in dom f & ||.
x1- x0 .|| <s & not ||. f/.x1- f/.x0 .|| <r;
defpred P[Element of NAT ,Point of CNS1] means $2 in dom f & ||. $2-x0 .||
< 1/($1+1) & not ||.f/.$2-f/.x0 .||<r;
A4: for n ex p be Point of CNS1 st P[n,p]
proof
let n;
0<1/(n+1);
then consider p be Point of CNS1 such that
A5: p in dom f & ||.p-x0 .|| < 1/(n+1) & not ||.f/.p-f/.x0 .|| <r by A3;
take p;
thus thesis by A5;
end;
consider s1 being sequence of the carrier of CNS1 such that
A6: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A4);
reconsider s1 as sequence of CNS1;
A7: rng s1 c= dom f
proof
A8: dom s1= NAT by FUNCT_2:def 1;
let v be object;
assume v in rng s1;
then ex n be object st n in NAT & v=s1.n by A8,FUNCT_1:def 3;
hence thesis by A6;
end;
A9: now
let n;
not ||.f/.(s1.n)-f/.x0 .||<r by A6;
hence not ||.(f/*s1).n-f/.x0 .||<r by A7,FUNCT_2:109;
end;
A10: now
let s be Real;
consider n being Nat such that
A11: s"<n by SEQ_4:3;
assume 0<s;
then
A12: 0<s";
s"+0 <n+1 by A11,XREAL_1:8;
then 1/(n+1)<1/s" by A12,XREAL_1:76;
then
A13: 1/(n+1)<s by XCMPLX_1:216;
take k=n;
let m be Nat;
A14: m in NAT by ORDINAL1:def 12;
assume k<=m;
then k+1<=m+1 by XREAL_1:6;
then 1/(m+1)<=1/(k+1) by XREAL_1:118;
then 1/(m+1)<s by A13,XXREAL_0:2;
hence ||. s1.m-x0 .|| <s by A6,XXREAL_0:2,A14;
end;
then
A15: s1 is convergent by CLVECT_1:def 15;
then lim s1=x0 by A10,CLVECT_1:def 16;
then f/*s1 is convergent & f/.x0=lim(f/*s1) by A1,A7,A15;
then consider n being Nat such that
A16: for m being Nat st n<=m
holds ||.(f/*s1).m-f/.x0.||<r by A2,CLVECT_1:def 16;
A17: n in NAT by ORDINAL1:def 12;
||.(f/*s1).n-f/.x0.||<r by A16;
hence contradiction by A9,A17;
end;
assume that
A18: x0 in dom f and
A19: for r st 0<r ex s st 0<s & for x1 be Point of CNS1 st x1 in dom f &
||. x1- x0 .|| <s holds ||. f/.x1- f/.x0 .|| <r;
now
let s1 be sequence of CNS1 such that
A20: rng s1 c= dom f and
A21: s1 is convergent & lim s1 = x0;
A22: now
let p be Real;
assume 0<p;
then consider s such that
A23: 0<s and
A24: for x1 be Point of CNS1 st x1 in dom f & ||. x1- x0 .|| <s
holds ||. f/.x1- f/.x0 .|| <p by A19;
consider n being Nat such that
A25: for m being Nat st n<=m holds ||. s1.m-x0 .|| <s
by A21,A23,CLVECT_1:def 16;
take k=n;
let m be Nat;
A26: m in NAT by ORDINAL1:def 12;
assume k<=m;
then
A27: ||. s1.m-x0 .|| <s by A25;
dom s1 = NAT by FUNCT_2:def 1;
then s1.m in rng s1 by FUNCT_1:3,A26;
then ||.f/.(s1.m)-f/.x0.||<p by A20,A24,A27;
hence ||.(f/*s1).m - f/.x0.||<p by A20,FUNCT_2:109,A26;
end;
then f/*s1 is convergent by CLVECT_1:def 15;
hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by A22,CLVECT_1:def 16;
end;
hence thesis by A18;
end;
theorem Th9:
for f be PartFunc of CNS,RNS, x0 be Point of CNS holds f
is_continuous_in x0 iff x0 in dom f & for r st 0<r ex s st 0<s & for x1 be
Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds ||. f/.x1-f/.x0 .||<r
proof
let f be PartFunc of CNS,RNS;
let x0 be Point of CNS;
thus f is_continuous_in x0 implies x0 in dom f & for r st 0<r ex s st 0<s &
for x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds ||. f/.x1- f/.
x0 .|| <r
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
given r such that
A2: 0<r and
A3: for s holds not 0<s or ex x1 be Point of CNS st x1 in dom f & ||.
x1 - x0 .|| <s & not ||. f/.x1- f/.x0 .|| <r;
defpred P[Element of NAT ,Point of CNS] means $2 in dom f & ||. $2-x0 .||
< 1/($1+1) & not ||.f/.$2-f/.x0 .||<r;
A4: for n ex p be Point of CNS st P[n,p]
proof
let n;
0<1/(n+1);
then consider p be Point of CNS such that
A5: p in dom f & ||.p-x0 .|| < 1/(n+1) & not ||.f/.p-f/.x0 .|| <r by A3;
take p;
thus thesis by A5;
end;
consider s1 being sequence of the carrier of CNS such that
A6: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A4);
reconsider s1 as sequence of CNS;
A7: rng s1 c= dom f
proof
A8: dom s1= NAT by FUNCT_2:def 1;
let v be object;
assume v in rng s1;
then ex n be object st n in NAT & v=s1.n by A8,FUNCT_1:def 3;
hence thesis by A6;
end;
A9: now
let n;
not ||.f/.(s1.n)-f/.x0 .||<r by A6;
hence not ||.(f/*s1).n-f/.x0 .||<r by A7,FUNCT_2:109;
end;
A10: now
let s be Real;
consider n being Nat such that
A11: s"<n by SEQ_4:3;
assume 0<s;
then
A12: 0<s";
s"+0 <n+1 by A11,XREAL_1:8;
then 1/(n+1)<1/s" by A12,XREAL_1:76;
then
A13: 1/(n+1)<s by XCMPLX_1:216;
take k=n;
let m be Nat;
A14: m in NAT by ORDINAL1:def 12;
assume k<=m;
then k+1<=m+1 by XREAL_1:6;
then 1/(m+1)<=1/(k+1) by XREAL_1:118;
then 1/(m+1)<s by A13,XXREAL_0:2;
hence ||. s1.m-x0 .|| <s by A6,XXREAL_0:2,A14;
end;
then
A15: s1 is convergent by CLVECT_1:def 15;
then lim s1=x0 by A10,CLVECT_1:def 16;
then f/*s1 is convergent & f/.x0=lim(f/*s1) by A1,A7,A15;
then consider n being Nat such that
A16: for m being Nat st n<=m holds ||.(f/*s1).m-f/.x0.||<r
by A2,NORMSP_1:def 7;
A17: n in NAT by ORDINAL1:def 12;
||.(f/*s1).n-f/.x0.||<r by A16;
hence contradiction by A9,A17;
end;
assume that
A18: x0 in dom f and
A19: for r st 0<r ex s st 0<s & for x1 be Point of CNS st x1 in dom f &
||. x1- x0 .|| <s holds ||. f/.x1- f/.x0 .|| <r;
now
let s1 be sequence of CNS such that
A20: rng s1 c= dom f and
A21: s1 is convergent & lim s1 = x0;
A22: now
let p be Real;
assume 0<p;
then consider s such that
A23: 0<s and
A24: for x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds
||. f/.x1- f/.x0 .|| <p by A19;
consider n being Nat such that
A25: for m being Nat st n<=m holds ||. s1.m-x0 .|| <s
by A21,A23,CLVECT_1:def 16;
take k=n;
let m be Nat;
A26: m in NAT by ORDINAL1:def 12;
assume k<=m;
then
A27: ||. s1.m-x0 .|| <s by A25;
dom s1 = NAT by FUNCT_2:def 1;
then s1.m in rng s1 by FUNCT_1:3,A26;
then ||.f/.(s1.m)-f/.x0.||<p by A20,A24,A27;
hence ||.(f/*s1).m - f/.x0.||<p by A20,FUNCT_2:109,A26;
end;
then f/*s1 is convergent by NORMSP_1:def 6;
hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by A22,NORMSP_1:def 7;
end;
hence thesis by A18;
end;
theorem Th10:
for f be PartFunc of RNS,CNS, x0 be Point of RNS holds f
is_continuous_in x0 iff x0 in dom f & for r st 0<r ex s st 0<s & for x1 be
Point of RNS st x1 in dom f & ||. x1- x0 .|| < s holds ||. f/.x1-f/.x0 .||<r
proof
let f be PartFunc of RNS,CNS;
let x0 be Point of RNS;
thus f is_continuous_in x0 implies x0 in dom f & for r st 0<r ex s st 0<s &
for x1 be Point of RNS st x1 in dom f & ||. x1- x0 .|| <s holds ||. f/.x1- f/.
x0 .|| <r
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
given r such that
A2: 0<r and
A3: for s holds not 0<s or ex x1 be Point of RNS st x1 in dom f & ||.
x1 - x0 .|| <s & not ||. f/.x1- f/.x0 .|| <r;
defpred P[Element of NAT ,Point of RNS] means $2 in dom f & ||. $2-x0 .||
< 1/($1+1) & not ||.f/.$2-f/.x0 .||<r;
A4: for n ex p be Point of RNS st P[n,p]
proof
let n;
0<1/(n+1);
then consider p be Point of RNS such that
A5: p in dom f & ||.p-x0 .|| < 1/(n+1) & not ||.f/.p-f/.x0 .|| <r by A3;
take p;
thus thesis by A5;
end;
consider s1 being sequence of the carrier of RNS such that
A6: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A4);
reconsider s1 as sequence of RNS;
A7: rng s1 c= dom f
proof
A8: dom s1= NAT by FUNCT_2:def 1;
let v be object;
assume v in rng s1;
then ex n be object st n in NAT & v=s1.n by A8,FUNCT_1:def 3;
hence thesis by A6;
end;
A9: now
let n;
not ||.f/.(s1.n)-f/.x0 .||<r by A6;
hence not ||.(f/*s1).n-f/.x0 .||<r by A7,FUNCT_2:109;
end;
A10: now
let s be Real;
consider n being Nat such that
A11: s"<n by SEQ_4:3;
assume 0<s;
then
A12: 0<s";
s"+0 <n+1 by A11,XREAL_1:8;
then 1/(n+1)<1/s" by A12,XREAL_1:76;
then
A13: 1/(n+1)<s by XCMPLX_1:216;
take k=n;
let m be Nat;
A14: m in NAT by ORDINAL1:def 12;
assume k<=m;
then k+1<=m+1 by XREAL_1:6;
then 1/(m+1)<=1/(k+1) by XREAL_1:118;
then 1/(m+1)<s by A13,XXREAL_0:2;
hence ||. s1.m-x0 .|| <s by A6,XXREAL_0:2,A14;
end;
then
A15: s1 is convergent by NORMSP_1:def 6;
then lim s1=x0 by A10,NORMSP_1:def 7;
then f/*s1 is convergent & f/.x0=lim(f/*s1) by A1,A7,A15;
then consider n being Nat such that
A16: for m being Nat st n<=m holds ||.(f/*s1).m-f/.x0.||<r
by A2,CLVECT_1:def 16;
A17: n in NAT by ORDINAL1:def 12;
||.(f/*s1).n-f/.x0.||<r by A16;
hence contradiction by A9,A17;
end;
assume that
A18: x0 in dom f and
A19: for r st 0<r ex s st 0<s & for x1 be Point of RNS st x1 in dom f &
||. x1- x0 .|| <s holds ||. f/.x1- f/.x0 .|| <r;
now
let s1 be sequence of RNS such that
A20: rng s1 c= dom f and
A21: s1 is convergent & lim s1 = x0;
A22: now
let p be Real;
assume 0<p;
then consider s such that
A23: 0<s and
A24: for x1 be Point of RNS st x1 in dom f & ||. x1- x0 .|| <s holds
||. f/.x1- f/.x0 .|| <p by A19;
consider n being Nat such that
A25: for m being Nat st n<=m holds ||. s1.m-x0 .|| <s
by A21,A23,NORMSP_1:def 7;
take k=n;
let m be Nat;
A26: m in NAT by ORDINAL1:def 12;
assume k<=m;
then
A27: ||. s1.m-x0 .|| <s by A25;
dom s1 = NAT by FUNCT_2:def 1;
then s1.m in rng s1 by FUNCT_1:3,A26;
then ||.f/.(s1.m)-f/.x0.||<p by A20,A24,A27;
hence ||.(f/*s1).m - f/.x0.||<p by A20,FUNCT_2:109,A26;
end;
then f/*s1 is convergent by CLVECT_1:def 15;
hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by A22,CLVECT_1:def 16;
end;
hence thesis by A18;
end;
theorem Th11:
for f be PartFunc of the carrier of CNS,REAL, x0 be Point of CNS
holds (f is_continuous_in x0 iff x0 in dom f & for r st 0<r ex s st 0<s & for
x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds |. f/.x1-f/.x0 .|<
r )
proof
let f be PartFunc of the carrier of CNS,REAL;
let x0 be Point of CNS;
thus f is_continuous_in x0 implies x0 in dom f & for r st 0<r ex s st 0<s &
for x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds |. f/.x1- f/.
x0 .| <r
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
given r such that
A2: 0<r and
A3: for s holds not 0<s or ex x1 be Point of CNS st x1 in dom f & ||.
x1 - x0 .|| <s & not |. f/.x1- f/.x0 .| <r;
defpred P[Element of NAT ,Point of CNS] means $2 in dom f & ||. $2-x0 .||
< 1/($1+1) & not |.f/.$2-f/.x0 .|<r;
A4: for n ex p be Point of CNS st P[n,p]
proof
let n;
0<1/(n+1);
then consider p be Point of CNS such that
A5: p in dom f & ||.p-x0 .|| < 1/(n+1) & not |.f/.p-f/.x0 .| <r by A3;
take p;
thus thesis by A5;
end;
consider s1 being sequence of the carrier of CNS such that
A6: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A4);
reconsider s1 as sequence of CNS;
A7: rng s1 c= dom f
proof
A8: dom s1= NAT by FUNCT_2:def 1;
let v be object;
assume v in rng s1;
then ex n be object st n in NAT & v=s1.n by A8,FUNCT_1:def 3;
hence thesis by A6;
end;
A9: now
let n;
not |.f/.(s1.n)-f/.x0 .|<r by A6;
hence not |. (f/*s1).n-f/.x0 .|<r by A7,FUNCT_2:109;
end;
A10: now
let s be Real;
consider n being Nat such that
A11: s"<n by SEQ_4:3;
assume 0<s;
then
A12: 0<s";
s"+0 <n+1 by A11,XREAL_1:8;
then 1/(n+1)<1/s" by A12,XREAL_1:76;
then
A13: 1/(n+1)<s by XCMPLX_1:216;
take k=n;
let m be Nat;
A14: m in NAT by ORDINAL1:def 12;
assume k<=m;
then k+1<=m+1 by XREAL_1:6;
then 1/(m+1)<=1/(k+1) by XREAL_1:118;
then 1/(m+1)<s by A13,XXREAL_0:2;
hence ||. s1.m-x0 .|| <s by A6,XXREAL_0:2,A14;
end;
then
A15: s1 is convergent by CLVECT_1:def 15;
then lim s1=x0 by A10,CLVECT_1:def 16;
then f/*s1 is convergent & f/.x0=lim(f/*s1) by A1,A7,A15;
then consider n being Nat such that
A16: for m being Nat st n<=m holds |. (f/*s1).m-f/.x0.|<r
by A2,SEQ_2:def 7;
A17: n in NAT by ORDINAL1:def 12;
|.(f/*s1).n-f/.x0.| <r by A16;
hence contradiction by A9,A17;
end;
assume that
A18: x0 in dom f and
A19: for r st 0<r ex s st 0<s & for x1 be Point of CNS st x1 in dom f &
||. x1- x0 .|| <s holds |. f/.x1- f/.x0 .| <r;
now
let s1 be sequence of CNS such that
A20: rng s1 c= dom f and
A21: s1 is convergent & lim s1 = x0;
A22: now
let p be Real;
reconsider pp=p as Real;
assume 0<p;
then consider s such that
A23: 0<s and
A24: for x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds
|.f/.x1- f/.x0 .| <pp by A19;
consider n being Nat such that
A25: for m being Nat st n<=m holds ||. s1.m-x0 .|| <s
by A21,A23,CLVECT_1:def 16;
take k=n;
let m be Nat;
A26: m in NAT by ORDINAL1:def 12;
assume k<=m;
then
A27: ||. s1.m-x0 .|| <s by A25;
dom s1 = NAT by FUNCT_2:def 1;
then s1.m in rng s1 by FUNCT_1:3,A26;
then |.f/.(s1.m)-f/.x0.| <p by A20,A24,A27;
hence |. (f/*s1).m - f/.x0.| <p by A20,FUNCT_2:109,A26;
end;
then f/*s1 is convergent by SEQ_2:def 6;
hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by A22,SEQ_2:def 7;
end;
hence thesis by A18;
end;
theorem Th12:
for f be PartFunc of the carrier of CNS,COMPLEX, x0 be Point of
CNS holds (f is_continuous_in x0 iff x0 in dom f & for r st 0 < r ex s st 0 < s
& for x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds |. f/.x1-f/.
x0 .|<r )
proof
let f be PartFunc of the carrier of CNS,COMPLEX;
let x0 be Point of CNS;
thus f is_continuous_in x0 implies x0 in dom f & for r st 0<r ex s st 0<s &
for x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds |. f/.x1- f/.x0
.| <r
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
given r such that
A2: 0<r and
A3: for s holds not 0<s or ex x1 be Point of CNS st x1 in dom f & ||.
x1 - x0 .|| <s & not |. f/.x1- f/.x0 .| <r;
defpred P[Element of NAT ,Point of CNS] means $2 in dom f & ||. $2-x0 .||
< 1/($1+1) & not |.(f/.$2-f/.x0 ).|<r;
A4: for n ex p be Point of CNS st P[n,p]
proof
let n;
0<1/(n+1);
then consider p be Point of CNS such that
A5: p in dom f & ||.p-x0 .|| < 1/(n+1) & not |. f/.p-f/.x0 .| <r by A3;
take p;
thus thesis by A5;
end;
consider s1 being sequence of the carrier of CNS such that
A6: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A4);
reconsider s1 as sequence of CNS;
A7: rng s1 c= dom f
proof
A8: dom s1= NAT by FUNCT_2:def 1;
let v be object;
assume v in rng s1;
then ex n be object st n in NAT & v=s1.n by A8,FUNCT_1:def 3;
hence thesis by A6;
end;
A9: now
let n;
not |. f/.(s1.n)-f/.x0 .|<r by A6;
hence not |. (f/*s1).n-f/.x0 .|<r by A7,FUNCT_2:109;
end;
A10: now
let s be Real;
consider n being Nat such that
A11: s"<n by SEQ_4:3;
assume 0<s;
then
A12: 0<s";
s"+0 <n+1 by A11,XREAL_1:8;
then 1/(n+1)<1/s" by A12,XREAL_1:76;
then
A13: 1/(n+1)<s by XCMPLX_1:216;
take k=n;
let m be Nat;
A14: m in NAT by ORDINAL1:def 12;
assume k<=m;
then k+1<=m+1 by XREAL_1:6;
then 1/(m+1)<=1/(k+1) by XREAL_1:118;
then 1/(m+1)<s by A13,XXREAL_0:2;
hence ||. s1.m-x0 .|| <s by A6,XXREAL_0:2,A14;
end;
then
A15: s1 is convergent by CLVECT_1:def 15;
then lim s1=x0 by A10,CLVECT_1:def 16;
then f/*s1 is convergent & f/.x0=lim(f/*s1) by A1,A7,A15;
then consider n being Nat such that
A16: for m being Nat st n<=m
holds |. (f/*s1).m-f/.x0 .|<r by A2,COMSEQ_2:def 6;
A17: n in NAT by ORDINAL1:def 12;
|. (f/*s1).n-f/.x0 .| <r by A16;
hence contradiction by A9,A17;
end;
assume that
A18: x0 in dom f and
A19: for r st 0<r ex s st 0<s & for x1 be Point of CNS st x1 in dom f &
||. x1- x0 .|| <s holds |. f/.x1- f/.x0 .| <r;
now
let s1 be sequence of CNS such that
A20: rng s1 c= dom f and
A21: s1 is convergent & lim s1 = x0;
A22: now
let p be Real;
assume 0<p;
then consider s such that
A23: 0<s and
A24: for x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds
|. f/.x1- f/.x0 .| <p by A19;
consider n being Nat such that
A25: for m being Nat st n<=m holds ||. s1.m-x0 .|| <s
by A21,A23,CLVECT_1:def 16;
take k=n;
let m be Nat;
A26: m in NAT by ORDINAL1:def 12;
assume k<=m;
then
A27: ||. s1.m-x0 .|| <s by A25;
dom s1 = NAT by FUNCT_2:def 1;
then s1.m in rng s1 by FUNCT_1:3,A26;
then |. f/.(s1.m)-f/.x0 .| <p by A20,A24,A27;
hence |. (f/*s1).m - f/.x0 .| <p by A20,FUNCT_2:109,A26;
end;
then f/*s1 is convergent by COMSEQ_2:def 5;
hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by A22,COMSEQ_2:def 6;
end;
hence thesis by A18;
end;
theorem Th13:
for f be PartFunc of the carrier of RNS,COMPLEX, x0 be Point of
RNS holds (f is_continuous_in x0 iff x0 in dom f & for r st 0<r ex s st 0<s &
for x1 be Point of RNS st x1 in dom f & ||. x1- x0 .|| <s holds |. f/.x1-f/.x0
.|<r )
proof
let f be PartFunc of the carrier of RNS,COMPLEX;
let x0 be Point of RNS;
thus f is_continuous_in x0 implies x0 in dom f & for r st 0<r ex s st 0<s &
for x1 be Point of RNS st x1 in dom f & ||. x1- x0 .|| <s holds |. f/.x1- f/.x0
.| <r
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
given r such that
A2: 0<r and
A3: for s holds not 0<s or ex x1 be Point of RNS st x1 in dom f & ||.
x1 - x0 .|| <s & not |. f/.x1- f/.x0 .| <r;
defpred P[Element of NAT ,Point of RNS] means $2 in dom f & ||. $2-x0 .||
< 1/($1+1) & not |.(f/.$2-f/.x0 ).|<r;
A4: for n ex p be Point of RNS st P[n,p]
proof
let n;
0<1/(n+1);
then consider p be Point of RNS such that
A5: p in dom f & ||.p-x0 .|| < 1/(n+1) & not |. f/.p-f/.x0 .| <r by A3;
take p;
thus thesis by A5;
end;
consider s1 being sequence of the carrier of RNS such that
A6: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A4);
reconsider s1 as sequence of RNS;
A7: rng s1 c= dom f
proof
A8: dom s1= NAT by FUNCT_2:def 1;
let v be object;
assume v in rng s1;
then ex n be object st n in NAT & v=s1.n by A8,FUNCT_1:def 3;
hence thesis by A6;
end;
A9: now
let n;
not |. f/.(s1.n)-f/.x0 .|<r by A6;
hence not |. (f/*s1).n-f/.x0 .|<r by A7,FUNCT_2:109;
end;
A10: now
let s be Real;
consider n being Nat such that
A11: s"<n by SEQ_4:3;
assume 0<s;
then
A12: 0<s";
s"+0 <n+1 by A11,XREAL_1:8;
then 1/(n+1)<1/s" by A12,XREAL_1:76;
then
A13: 1/(n+1)<s by XCMPLX_1:216;
take k=n;
let m be Nat;
A14: m in NAT by ORDINAL1:def 12;
assume k<=m;
then k+1<=m+1 by XREAL_1:6;
then 1/(m+1)<=1/(k+1) by XREAL_1:118;
then 1/(m+1)<s by A13,XXREAL_0:2;
hence ||. s1.m-x0 .|| <s by A6,XXREAL_0:2,A14;
end;
then
A15: s1 is convergent by NORMSP_1:def 6;
then lim s1=x0 by A10,NORMSP_1:def 7;
then f/*s1 is convergent & f/.x0=lim(f/*s1) by A1,A7,A15;
then consider n being Nat such that
A16: for m being Nat st n<=m holds |. (f/*s1).m-f/.x0 .|<r
by A2,COMSEQ_2:def 6;
A17: n in NAT by ORDINAL1:def 12;
|. (f/*s1).n-f/.x0 .| <r by A16;
hence contradiction by A9,A17;
end;
assume that
A18: x0 in dom f and
A19: for r st 0<r ex s st 0<s & for x1 be Point of RNS st x1 in dom f &
||. x1- x0 .|| <s holds |. f/.x1- f/.x0 .| <r;
now
let s1 be sequence of RNS such that
A20: rng s1 c= dom f and
A21: s1 is convergent & lim s1 = x0;
A22: now
let p be Real;
assume 0<p;
then consider s such that
A23: 0<s and
A24: for x1 be Point of RNS st x1 in dom f & ||. x1- x0 .|| <s holds
|. f/.x1- f/.x0 .| <p by A19;
consider n being Nat such that
A25: for m being Nat st n<=m
holds ||. s1.m-x0 .|| <s by A21,A23,NORMSP_1:def 7;
take k=n;
let m be Nat;
A26: m in NAT by ORDINAL1:def 12;
assume k<=m;
then
A27: ||. s1.m-x0 .|| <s by A25;
dom s1 = NAT by FUNCT_2:def 1;
then s1.m in rng s1 by FUNCT_1:3,A26;
then |. f/.(s1.m)-f/.x0 .| <p by A20,A24,A27;
hence |. (f/*s1).m - f/.x0 .| <p by A20,FUNCT_2:109,A26;
end;
then f/*s1 is convergent by COMSEQ_2:def 5;
hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by A22,COMSEQ_2:def 6;
end;
hence thesis by A18;
end;
theorem Th14:
for f be PartFunc of CNS1,CNS2,x0 be Point of CNS1 holds f
is_continuous_in x0 iff x0 in dom f & for N1 being Neighbourhood of f/.x0 ex N
being Neighbourhood of x0 st for x1 be Point of CNS1 st x1 in dom f & x1 in N
holds f/.x1 in N1
proof
let f be PartFunc of CNS1,CNS2;
let x0 be Point of CNS1;
thus f is_continuous_in x0 implies x0 in dom f & for N1 being Neighbourhood
of f/.x0 ex N being Neighbourhood of x0 st for x1 be Point of CNS1 st x1 in dom
f & x1 in N holds f/.x1 in N1
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
let N1 be Neighbourhood of f/.x0;
consider r such that
A2: 0<r and
A3: {y where y is Point of CNS2 : ||.y-f/.x0 .|| < r} c= N1 by Def1;
consider s such that
A4: 0<s and
A5: for x1 be Point of CNS1 st x1 in dom f & ||. x1- x0 .|| <s holds
||. f/.x1- f/.x0 .|| <r by A1,A2,Th8;
reconsider N={z where z is Point of CNS1 : ||.z-x0 .|| < s} as
Neighbourhood of x0 by A4,Th2;
take N;
let x1 be Point of CNS1;
assume that
A6: x1 in dom f and
A7: x1 in N;
ex z be Point of CNS1 st x1=z & ||.z-x0 .|| < s by A7;
then ||. f/.x1- f/.x0 .|| <r by A5,A6;
then f/.x1 in {y where y is Point of CNS2 : ||.y-f/.x0 .|| < r};
hence thesis by A3;
end;
assume that
A8: x0 in dom f and
A9: for N1 being Neighbourhood of f/.x0 ex N being Neighbourhood of x0
st for x1 be Point of CNS1 st x1 in dom f & x1 in N holds f/.x1 in N1;
now
let r;
assume 0<r;
then reconsider N1 = {y where y is Point of CNS2 : ||.y-f/.x0 .|| < r} as
Neighbourhood of f/.x0 by Th2;
consider N2 being Neighbourhood of x0 such that
A10: for x1 be Point of CNS1 st x1 in dom f & x1 in N2 holds f/.x1 in N1 by A9;
consider s such that
A11: 0<s and
A12: {z where z is Point of CNS1 : ||.z-x0 .|| < s} c= N2 by Def1;
take s;
for x1 be Point of CNS1 st x1 in dom f & ||. x1- x0 .|| <s holds ||.
f/.x1- f/.x0 .|| <r
proof
let x1 be Point of CNS1;
assume that
A13: x1 in dom f and
A14: ||. x1- x0 .|| <s;
x1 in {z where z is Point of CNS1 : ||.z-x0 .|| < s} by A14;
then f/.x1 in N1 by A10,A12,A13;
then ex y be Point of CNS2 st f/.x1=y & ||.y-f/.x0 .|| < r;
hence thesis;
end;
hence 0<s & for x1 be Point of CNS1 st x1 in dom f & ||. x1- x0 .|| < s
holds ||. f/.x1- f/.x0 .|| <r by A11;
end;
hence thesis by A8,Th8;
end;
theorem Th15:
for f be PartFunc of CNS,RNS,x0 be Point of CNS holds f
is_continuous_in x0 iff x0 in dom f & for N1 being Neighbourhood of f/.x0 ex N
being Neighbourhood of x0 st for x1 be Point of CNS st x1 in dom f & x1 in N
holds f/.x1 in N1
proof
let f be PartFunc of CNS,RNS;
let x0 be Point of CNS;
thus f is_continuous_in x0 implies x0 in dom f & for N1 being Neighbourhood
of f/.x0 ex N being Neighbourhood of x0 st for x1 be Point of CNS st x1 in dom
f & x1 in N holds f/.x1 in N1
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
let N1 be Neighbourhood of f/.x0;
consider r such that
A2: 0<r and
A3: {y where y is Point of RNS : ||.y-f/.x0 .|| < r} c= N1 by NFCONT_1:def 1;
consider s such that
A4: 0<s and
A5: for x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds
||. f/.x1- f/.x0 .|| <r by A1,A2,Th9;
reconsider N={z where z is Point of CNS : ||.z-x0 .|| < s} as
Neighbourhood of x0 by A4,Th2;
take N;
let x1 be Point of CNS;
assume that
A6: x1 in dom f and
A7: x1 in N;
ex z be Point of CNS st x1=z & ||.z-x0 .|| < s by A7;
then ||. f/.x1- f/.x0 .|| <r by A5,A6;
then f/.x1 in {y where y is Point of RNS : ||.y-f/.x0 .|| < r};
hence thesis by A3;
end;
assume that
A8: x0 in dom f and
A9: for N1 being Neighbourhood of f/.x0 ex N being Neighbourhood of x0
st for x1 be Point of CNS st x1 in dom f & x1 in N holds f/.x1 in N1;
now
let r;
assume 0<r;
then reconsider N1 = {y where y is Point of RNS : ||.y-f/.x0 .|| < r} as
Neighbourhood of f/.x0 by NFCONT_1:3;
consider N2 being Neighbourhood of x0 such that
A10: for x1 be Point of CNS st x1 in dom f & x1 in N2 holds f/.x1 in N1 by A9;
consider s such that
A11: 0<s and
A12: {z where z is Point of CNS : ||.z-x0 .|| < s} c= N2 by Def1;
take s;
for x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds ||. f
/.x1- f/.x0 .|| <r
proof
let x1 be Point of CNS;
assume that
A13: x1 in dom f and
A14: ||. x1- x0 .|| <s;
x1 in {z where z is Point of CNS : ||.z-x0 .|| < s} by A14;
then f/.x1 in N1 by A10,A12,A13;
then ex y be Point of RNS st f/.x1=y & ||.y-f/.x0 .|| < r;
hence thesis;
end;
hence 0<s & for x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| < s
holds ||. f/.x1- f/.x0 .|| <r by A11;
end;
hence thesis by A8,Th9;
end;
theorem Th16:
for f be PartFunc of RNS,CNS, x0 be Point of RNS holds f
is_continuous_in x0 iff x0 in dom f & for N1 being Neighbourhood of f/.x0 ex N
being Neighbourhood of x0 st for x1 be Point of RNS st x1 in dom f & x1 in N
holds f/.x1 in N1
proof
let f be PartFunc of RNS,CNS;
let x0 be Point of RNS;
thus f is_continuous_in x0 implies x0 in dom f & for N1 being Neighbourhood
of f/.x0 ex N being Neighbourhood of x0 st for x1 be Point of RNS st x1 in dom
f & x1 in N holds f/.x1 in N1
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
let N1 be Neighbourhood of f/.x0;
consider r such that
A2: 0<r and
A3: {y where y is Point of CNS : ||.y-f/.x0 .|| < r} c= N1 by Def1;
consider s such that
A4: 0<s and
A5: for x1 be Point of RNS st x1 in dom f & ||. x1- x0 .|| <s holds
||. f/.x1- f/.x0 .|| <r by A1,A2,Th10;
reconsider N={z where z is Point of RNS : ||.z-x0 .|| < s} as
Neighbourhood of x0 by A4,NFCONT_1:3;
take N;
let x1 be Point of RNS;
assume that
A6: x1 in dom f and
A7: x1 in N;
ex z be Point of RNS st x1=z & ||.z-x0 .|| < s by A7;
then ||. f/.x1- f/.x0 .|| <r by A5,A6;
then f/.x1 in {y where y is Point of CNS : ||.y-f/.x0 .|| < r};
hence thesis by A3;
end;
assume that
A8: x0 in dom f and
A9: for N1 being Neighbourhood of f/.x0 ex N being Neighbourhood of x0
st for x1 be Point of RNS st x1 in dom f & x1 in N holds f/.x1 in N1;
now
let r;
assume 0<r;
then reconsider N1 = {y where y is Point of CNS : ||.y-f/.x0 .|| < r} as
Neighbourhood of f/.x0 by Th2;
consider N2 being Neighbourhood of x0 such that
A10: for x1 be Point of RNS st x1 in dom f & x1 in N2 holds f/.x1 in N1 by A9;
consider s such that
A11: 0<s and
A12: {z where z is Point of RNS : ||.z-x0 .|| < s} c= N2 by NFCONT_1:def 1;
take s;
for x1 be Point of RNS st x1 in dom f & ||. x1- x0 .|| <s holds ||. f
/.x1- f/.x0 .|| <r
proof
let x1 be Point of RNS;
assume that
A13: x1 in dom f and
A14: ||. x1- x0 .|| <s;
x1 in {z where z is Point of RNS : ||.z-x0 .|| < s} by A14;
then f/.x1 in N1 by A10,A12,A13;
then ex y be Point of CNS st f/.x1=y & ||.y-f/.x0 .|| < r;
hence thesis;
end;
hence 0<s & for x1 be Point of RNS st x1 in dom f & ||. x1 - x0 .|| < s
holds ||. f/.x1- f/.x0 .|| <r by A11;
end;
hence thesis by A8,Th10;
end;
theorem Th17:
for f be PartFunc of CNS1,CNS2, x0 be Point of CNS1 holds f
is_continuous_in x0 iff x0 in dom f & for N1 being Neighbourhood of f/.x0 ex N
being Neighbourhood of x0 st f.:N c= N1
proof
let f be PartFunc of CNS1,CNS2;
let x0 be Point of CNS1;
thus f is_continuous_in x0 implies x0 in dom f & for N1 being Neighbourhood
of f/.x0 ex N being Neighbourhood of x0 st f.:N c= N1
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
let N1 be Neighbourhood of f/.x0;
consider N being Neighbourhood of x0 such that
A2: for x1 be Point of CNS1 st x1 in dom f & x1 in N holds f/.x1 in N1
by A1,Th14;
take N;
now
let r be object;
assume r in f.:N;
then consider x be Point of CNS1 such that
A3: x in dom f and
A4: x in N and
A5: r=f.x by PARTFUN2:59;
r=f/.x by A3,A5,PARTFUN1:def 6;
hence r in N1 by A2,A3,A4;
end;
hence thesis;
end;
assume that
A6: x0 in dom f and
A7: for N1 being Neighbourhood of f/.x0 ex N being Neighbourhood of x0
st f.:N c= N1;
now
let N1 be Neighbourhood of f/.x0;
consider N being Neighbourhood of x0 such that
A8: f.:N c= N1 by A7;
take N;
let x1 be Point of CNS1;
assume that
A9: x1 in dom f and
A10: x1 in N;
f.x1 in f.:N by A9,A10,FUNCT_1:def 6;
then f.x1 in N1 by A8;
hence f/.x1 in N1 by A9,PARTFUN1:def 6;
end;
hence thesis by A6,Th14;
end;
theorem Th18:
for f be PartFunc of CNS,RNS, x0 be Point of CNS holds f
is_continuous_in x0 iff x0 in dom f & for N1 being Neighbourhood of f/.x0 ex N
being Neighbourhood of x0 st f.:N c= N1
proof
let f be PartFunc of CNS,RNS;
let x0 be Point of CNS;
thus f is_continuous_in x0 implies x0 in dom f & for N1 being Neighbourhood
of f/.x0 ex N being Neighbourhood of x0 st f.:N c= N1
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
let N1 be Neighbourhood of f/.x0;
consider N being Neighbourhood of x0 such that
A2: for x1 be Point of CNS st x1 in dom f & x1 in N holds f/.x1 in N1
by A1,Th15;
take N;
now
let r be object;
assume r in f.:N;
then consider x be Point of CNS such that
A3: x in dom f and
A4: x in N and
A5: r=f.x by PARTFUN2:59;
r=f/.x by A3,A5,PARTFUN1:def 6;
hence r in N1 by A2,A3,A4;
end;
hence thesis;
end;
assume that
A6: x0 in dom f and
A7: for N1 being Neighbourhood of f/.x0 ex N being Neighbourhood of x0
st f.:N c= N1;
now
let N1 be Neighbourhood of f/.x0;
consider N being Neighbourhood of x0 such that
A8: f.:N c= N1 by A7;
take N;
let x1 be Point of CNS;
assume that
A9: x1 in dom f and
A10: x1 in N;
f.x1 in f.:N by A9,A10,FUNCT_1:def 6;
then f.x1 in N1 by A8;
hence f/.x1 in N1 by A9,PARTFUN1:def 6;
end;
hence thesis by A6,Th15;
end;
theorem Th19:
for f be PartFunc of RNS,CNS, x0 be Point of RNS holds f
is_continuous_in x0 iff x0 in dom f & for N1 being Neighbourhood of f/.x0 ex N
being Neighbourhood of x0 st f.:N c= N1
proof
let f be PartFunc of RNS,CNS;
let x0 be Point of RNS;
thus f is_continuous_in x0 implies x0 in dom f & for N1 being Neighbourhood
of f/.x0 ex N being Neighbourhood of x0 st f.:N c= N1
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
let N1 be Neighbourhood of f/.x0;
consider N being Neighbourhood of x0 such that
A2: for x1 be Point of RNS st x1 in dom f & x1 in N holds f/.x1 in N1
by A1,Th16;
take N;
now
let r be object;
assume r in f.:N;
then consider x be Point of RNS such that
A3: x in dom f and
A4: x in N and
A5: r=f.x by PARTFUN2:59;
r=f/.x by A3,A5,PARTFUN1:def 6;
hence r in N1 by A2,A3,A4;
end;
hence thesis;
end;
assume that
A6: x0 in dom f and
A7: for N1 being Neighbourhood of f/.x0 ex N being Neighbourhood of x0
st f.:N c= N1;
now
let N1 be Neighbourhood of f/.x0;
consider N being Neighbourhood of x0 such that
A8: f.:N c= N1 by A7;
take N;
let x1 be Point of RNS;
assume that
A9: x1 in dom f and
A10: x1 in N;
f.x1 in f.:N by A9,A10,FUNCT_1:def 6;
then f.x1 in N1 by A8;
hence f/.x1 in N1 by A9,PARTFUN1:def 6;
end;
hence thesis by A6,Th16;
end;
theorem
for f be PartFunc of CNS1,CNS2, x0 be Point of CNS1 st x0 in dom f & (
ex N be Neighbourhood of x0 st dom f /\ N = {x0}) holds f is_continuous_in x0
proof
let f be PartFunc of CNS1,CNS2;
let x0 be Point of CNS1;
assume
A1: x0 in dom f;
given N be Neighbourhood of x0 such that
A2: dom f /\ N = {x0};
now
let N1 be Neighbourhood of f/.x0;
take N;
A3: f/.x0 in N1 by Th3;
f.:N = Im(f,x0) by A2,RELAT_1:112
.= {f.x0} by A1,FUNCT_1:59
.= {f/.x0} by A1,PARTFUN1:def 6;
hence f.:N c= N1 by A3,ZFMISC_1:31;
end;
hence thesis by A1,Th17;
end;
theorem
for f be PartFunc of CNS,RNS, x0 be Point of CNS st x0 in dom f & (ex
N be Neighbourhood of x0 st dom f /\ N = {x0}) holds f is_continuous_in x0
proof
let f be PartFunc of CNS,RNS;
let x0 be Point of CNS;
assume
A1: x0 in dom f;
given N be Neighbourhood of x0 such that
A2: dom f /\ N = {x0};
now
let N1 be Neighbourhood of f/.x0;
take N;
A3: f/.x0 in N1 by NFCONT_1:4;
f.:N = Im(f,x0) by A2,RELAT_1:112
.= {f.x0} by A1,FUNCT_1:59
.= {f/.x0} by A1,PARTFUN1:def 6;
hence f.:N c= N1 by A3,ZFMISC_1:31;
end;
hence thesis by A1,Th18;
end;
theorem
for f be PartFunc of RNS,CNS, x0 be Point of RNS st x0 in dom f & (ex
N be Neighbourhood of x0 st dom f /\ N = {x0}) holds f is_continuous_in x0
proof
let f be PartFunc of RNS,CNS;
let x0 be Point of RNS;
assume
A1: x0 in dom f;
given N be Neighbourhood of x0 such that
A2: dom f /\ N = {x0};
now
let N1 be Neighbourhood of f/.x0;
take N;
A3: f/.x0 in N1 by Th3;
f.:N = Im(f,x0) by A2,RELAT_1:112
.= {f.x0} by A1,FUNCT_1:59
.= {f/.x0} by A1,PARTFUN1:def 6;
hence f.:N c= N1 by A3,ZFMISC_1:31;
end;
hence thesis by A1,Th19;
end;
theorem Th23:
for h1,h2 be PartFunc of CNS1,CNS2, seq be sequence of CNS1 st
rng seq c= dom h1 /\ dom h2 holds (h1+h2)/*seq=h1/*seq+h2/*seq & (h1-h2)/*seq=
h1/*seq-h2/*seq
proof
let h1,h2 be PartFunc of CNS1,CNS2;
let seq be sequence of CNS1;
A1: dom h1 /\ dom h2 c= dom h1 by XBOOLE_1:17;
A2: dom h1 /\ dom h2 c= dom h2 by XBOOLE_1:17;
assume
A3: rng seq c= dom h1 /\ dom h2;
then
A4: rng seq c= dom (h1 + h2) by VFUNCT_1:def 1;
now
let n be Nat;
A5: n in NAT by ORDINAL1:def 12;
A6: seq.n in dom (h1 + h2) by A4,Th4;
thus ((h1+h2)/*seq).n = (h1+h2)/.(seq.n) by A4,FUNCT_2:109,A5
.= h1/.(seq.n) + h2/.(seq.n) by A6,VFUNCT_1:def 1
.= (h1/*seq).n + h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A5
.= (h1/*seq).n + (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A5;
end;
hence (h1+h2)/*seq=h1/*seq+h2/*seq by NORMSP_1:def 2;
A7: rng seq c= dom (h1 - h2) by A3,VFUNCT_1:def 2;
now
let n be Nat;
A8: n in NAT by ORDINAL1:def 12;
A9: seq.n in dom (h1 - h2) by A7,Th4;
thus ((h1-h2)/*seq).n = (h1-h2)/.(seq.n) by A7,FUNCT_2:109,A8
.= h1/.(seq.n) - h2/.(seq.n) by A9,VFUNCT_1:def 2
.= (h1/*seq).n - h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A8
.= (h1/*seq).n - (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A8;
end;
hence thesis by NORMSP_1:def 3;
end;
theorem Th24:
for h1,h2 be PartFunc of CNS,RNS, seq be sequence of CNS st rng
seq c= dom h1 /\ dom h2 holds (h1+h2)/*seq=h1/*seq+h2/*seq & (h1-h2)/*seq=h1/*
seq-h2/*seq
proof
let h1,h2 be PartFunc of CNS,RNS;
let seq be sequence of CNS;
A1: dom h1 /\ dom h2 c= dom h1 by XBOOLE_1:17;
A2: dom h1 /\ dom h2 c= dom h2 by XBOOLE_1:17;
assume
A3: rng seq c= dom h1 /\ dom h2;
then
A4: rng seq c= dom (h1 + h2) by VFUNCT_1:def 1;
now
let n be Nat;
A5: n in NAT by ORDINAL1:def 12;
A6: seq.n in dom (h1 + h2) by A4,Th5;
thus ((h1+h2)/*seq).n = (h1+h2)/.(seq.n) by A4,FUNCT_2:109,A5
.= h1/.(seq.n) + h2/.(seq.n) by A6,VFUNCT_1:def 1
.= (h1/*seq).n + h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A5
.= (h1/*seq).n + (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A5;
end;
hence (h1+h2)/*seq=h1/*seq+h2/*seq by NORMSP_1:def 2;
A7: rng seq c= dom (h1 - h2) by A3,VFUNCT_1:def 2;
now
let n be Nat;
A8: n in NAT by ORDINAL1:def 12;
A9: seq.n in dom (h1 - h2) by A7,Th5;
thus ((h1-h2)/*seq).n = (h1-h2)/.(seq.n) by A7,FUNCT_2:109,A8
.= h1/.(seq.n) - h2/.(seq.n) by A9,VFUNCT_1:def 2
.= (h1/*seq).n - h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A8
.= (h1/*seq).n - (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A8;
end;
hence thesis by NORMSP_1:def 3;
end;
theorem Th25:
for h1,h2 be PartFunc of RNS,CNS, seq be sequence of RNS st rng
seq c= dom h1 /\ dom h2 holds (h1+h2)/*seq=h1/*seq+h2/*seq & (h1-h2)/*seq=h1/*
seq-h2/*seq
proof
let h1,h2 be PartFunc of RNS,CNS;
let seq be sequence of RNS;
A1: dom h1 /\ dom h2 c= dom h1 by XBOOLE_1:17;
A2: dom h1 /\ dom h2 c= dom h2 by XBOOLE_1:17;
assume
A3: rng seq c= dom h1 /\ dom h2;
then
A4: rng seq c= dom (h1 + h2) by VFUNCT_1:def 1;
now
let n be Nat;
A5: n in NAT by ORDINAL1:def 12;
A6: seq.n in dom (h1 + h2) by A4,Th6;
thus ((h1+h2)/*seq).n = (h1+h2)/.(seq.n) by A4,FUNCT_2:109,A5
.= h1/.(seq.n) + h2/.(seq.n) by A6,VFUNCT_1:def 1
.= (h1/*seq).n + h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A5
.= (h1/*seq).n + (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A5;
end;
hence (h1+h2)/*seq=h1/*seq+h2/*seq by NORMSP_1:def 2;
A7: rng seq c= dom (h1 - h2) by A3,VFUNCT_1:def 2;
now
let n be Nat;
A8: n in NAT by ORDINAL1:def 12;
A9: seq.n in dom (h1 - h2) by A7,Th6;
thus ((h1-h2)/*seq).n = (h1-h2)/.(seq.n) by A7,FUNCT_2:109,A8
.= h1/.(seq.n) - h2/.(seq.n) by A9,VFUNCT_1:def 2
.= (h1/*seq).n - h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A8
.= (h1/*seq).n - (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A8;
end;
hence thesis by NORMSP_1:def 3;
end;
theorem Th26:
for h be PartFunc of CNS1,CNS2, seq be sequence of CNS1, z be
Complex st rng seq c= dom h holds (z(#)h)/*seq = z*(h/*seq)
proof
let h be PartFunc of CNS1,CNS2;
let seq be sequence of CNS1;
let z be Complex;
assume
A1: rng seq c= dom h;
then
A2: rng seq c= dom (z(#)h) by VFUNCT_2:def 2;
now
let n be Nat;
A3: n in NAT by ORDINAL1:def 12;
A4: seq.n in dom (z(#)h) by A2,Th4;
thus ((z(#)h)/*seq).n = (z(#)h)/.(seq.n) by A2,FUNCT_2:109,A3
.= z * (h/.(seq.n)) by A4,VFUNCT_2:def 2
.= z * (h/*seq).n by A1,FUNCT_2:109,A3;
end;
hence thesis by CLVECT_1:def 14;
end;
theorem Th27:
for h be PartFunc of CNS,RNS, seq be sequence of CNS, r be Real
st rng seq c= dom h holds (r(#)h)/*seq = r*(h/*seq)
proof
let h be PartFunc of CNS,RNS;
let seq be sequence of CNS;
let r be Real;
assume
A1: rng seq c= dom h;
then
A2: rng seq c= dom (r(#)h) by VFUNCT_1:def 4;
now
let n be Nat;
A3: n in NAT by ORDINAL1:def 12;
A4: seq.n in dom (r(#)h) by A2,Th5;
thus ((r(#)h)/*seq).n = (r(#)h)/.(seq.n) by A2,FUNCT_2:109,A3
.= r * (h/.(seq.n)) by A4,VFUNCT_1:def 4
.= r * (h/*seq).n by A1,FUNCT_2:109,A3;
end;
hence thesis by NORMSP_1:def 5;
end;
theorem Th28:
for h be PartFunc of RNS,CNS, seq be sequence of RNS, z be
Complex st rng seq c= dom h holds (z(#)h)/*seq = z*(h/*seq)
proof
let h be PartFunc of RNS,CNS;
let seq be sequence of RNS;
let z be Complex;
assume
A1: rng seq c= dom h;
then
A2: rng seq c= dom (z(#)h) by VFUNCT_2:def 2;
now
let n be Nat;
A3: n in NAT by ORDINAL1:def 12;
A4: seq.n in dom (z(#)h) by A2,Th6;
thus ((z(#)h)/*seq).n = (z(#)h)/.(seq.n) by A2,FUNCT_2:109,A3
.= z * (h/.(seq.n)) by A4,VFUNCT_2:def 2
.= z * (h/*seq).n by A1,FUNCT_2:109,A3;
end;
hence thesis by CLVECT_1:def 14;
end;
theorem Th29:
for h be PartFunc of CNS1,CNS2, seq be sequence of CNS1 st rng
seq c= dom h holds ||. h/*seq .|| = ||.h.||/*seq & -(h/*seq) = (-h)/*seq
proof
let h be PartFunc of CNS1,CNS2;
let seq be sequence of CNS1;
assume
A1: rng seq c= dom h;
then
A2: rng seq c= dom ||.h.|| by NORMSP_0:def 3;
now
let n;
seq.n in rng seq by Th7;
then seq.n in dom h by A1;
then
A3: seq.n in dom ||.h.|| by NORMSP_0:def 3;
thus ||.h/*seq.||.n = ||.(h/*seq).n.|| by NORMSP_0:def 4
.= ||.h/.(seq.n).|| by A1,FUNCT_2:109
.= ||.h.||.(seq.n) by A3,NORMSP_0:def 3
.= ||.h.||/.(seq.n) by A3,PARTFUN1:def 6
.= (||.h.||/*seq).n by A2,FUNCT_2:109;
end;
hence ||.h/*seq.|| = ||.h.||/*seq by FUNCT_2:63;
thus -(h/*seq) =(-1r)*(h/*seq) by Th1
.= ((-1r)(#)h)/*seq by A1,Th26
.= (-h)/*seq by VFUNCT_2:23;
end;
theorem Th30:
for h be PartFunc of CNS,RNS, seq be sequence of CNS st rng seq
c= dom h holds ||. h/*seq .|| = ||.h.||/*seq & -(h/*seq) = (-h)/*seq
proof
let h be PartFunc of CNS,RNS;
let seq be sequence of CNS;
assume
A1: rng seq c= dom h;
then
A2: rng seq c= dom ||.h.|| by NORMSP_0:def 3;
now
let n;
seq.n in rng seq by Th7;
then seq.n in dom h by A1;
then
A3: seq.n in dom ||.h.|| by NORMSP_0:def 3;
thus ||.h/*seq.||.n = ||.(h/*seq).n.|| by NORMSP_0:def 4
.= ||.h/.(seq.n).|| by A1,FUNCT_2:109
.= ||.h.||.(seq.n) by A3,NORMSP_0:def 3
.= ||.h.||/.(seq.n) by A3,PARTFUN1:def 6
.= (||.h.||/*seq).n by A2,FUNCT_2:109;
end;
hence ||.h/*seq.|| = ||.h.||/*seq by FUNCT_2:63;
thus -(h/*seq) =(-1)*(h/*seq) by NFCONT_1:2
.= ((-1)(#)h)/*seq by A1,Th27
.= (-h)/*seq by VFUNCT_1:23;
end;
theorem Th31:
for h be PartFunc of RNS,CNS, seq be sequence of RNS st rng seq
c= dom h holds ||. h/*seq .|| = ||.h.||/*seq & -(h/*seq) = (-h)/*seq
proof
let h be PartFunc of RNS,CNS;
let seq be sequence of RNS;
assume
A1: rng seq c= dom h;
then
A2: rng seq c= dom ||.h.|| by NORMSP_0:def 3;
now
let n;
seq.n in rng seq by NFCONT_1:6;
then seq.n in dom h by A1;
then
A3: seq.n in dom ||.h.|| by NORMSP_0:def 3;
thus ||.h/*seq.||.n = ||.(h/*seq).n.|| by NORMSP_0:def 4
.= ||.h/.(seq.n).|| by A1,FUNCT_2:109
.= ||.h.||.(seq.n) by A3,NORMSP_0:def 3
.= ||.h.||/.(seq.n) by A3,PARTFUN1:def 6
.= (||.h.||/*seq).n by A2,FUNCT_2:109;
end;
hence ||.h/*seq.|| = ||.h.||/*seq by FUNCT_2:63;
thus -(h/*seq) =(-1r)*(h/*seq) by Th1
.= ((-1r)(#)h)/*seq by A1,Th28
.= (-h)/*seq by VFUNCT_2:23;
end;
theorem
for f1,f2 be PartFunc of CNS1,CNS2, x0 be Point of CNS1 st f1
is_continuous_in x0 & f2 is_continuous_in x0 holds f1+f2 is_continuous_in x0 &
f1-f2 is_continuous_in x0
proof
let f1,f2 be PartFunc of CNS1,CNS2;
let x0 be Point of CNS1;
assume that
A1: f1 is_continuous_in x0 and
A2: f2 is_continuous_in x0;
A3: x0 in dom f1 & x0 in dom f2 by A1,A2;
now
x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
hence
A4: x0 in dom (f1+f2) by VFUNCT_1:def 1;
let s1 be sequence of CNS1;
assume that
A5: rng s1 c= dom(f1+f2) and
A6: s1 is convergent & lim s1=x0;
A7: rng s1 c= dom f1 /\ dom f2 by A5,VFUNCT_1:def 1;
dom (f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
then dom (f1+f2) c= dom f2 by XBOOLE_1:17;
then
A8: rng s1 c= dom f2 by A5;
then
A9: f2/*s1 is convergent by A2,A6;
dom (f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
then dom (f1+f2) c= dom f1 by XBOOLE_1:17;
then
A10: rng s1 c= dom f1 by A5;
then
A11: f1/*s1 is convergent by A1,A6;
then (f1/*s1)+(f2/*s1) is convergent by A9,CLVECT_1:113;
hence (f1+f2)/*s1 is convergent by A7,Th23;
A12: f1/.x0 = lim (f1/*s1) by A1,A6,A10;
A13: f2/.x0 = lim (f2/*s1) by A2,A6,A8;
thus (f1+f2)/.x0 = f1/.x0 + f2/.x0 by A4,VFUNCT_1:def 1
.= lim (f1/*s1 + f2/*s1) by A11,A12,A9,A13,CLVECT_1:119
.= lim ((f1+f2)/*s1) by A7,Th23;
end;
hence f1+f2 is_continuous_in x0;
now
x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
hence
A14: x0 in dom (f1-f2) by VFUNCT_1:def 2;
let s1 be sequence of CNS1;
assume that
A15: rng s1 c= dom(f1-f2) and
A16: s1 is convergent & lim s1=x0;
A17: rng s1 c= dom f1 /\ dom f2 by A15,VFUNCT_1:def 2;
dom (f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
then dom (f1-f2) c= dom f2 by XBOOLE_1:17;
then
A18: rng s1 c= dom f2 by A15;
then
A19: f2/*s1 is convergent by A2,A16;
dom (f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
then dom (f1-f2) c= dom f1 by XBOOLE_1:17;
then
A20: rng s1 c= dom f1 by A15;
then
A21: f1/*s1 is convergent by A1,A16;
then f1/*s1-f2/*s1 is convergent by A19,CLVECT_1:114;
hence (f1-f2)/*s1 is convergent by A17,Th23;
A22: f1/.x0 = lim (f1/*s1) by A1,A16,A20;
A23: f2/.x0 = lim (f2/*s1) by A2,A16,A18;
thus (f1-f2)/.x0 = f1/.x0 - f2/.x0 by A14,VFUNCT_1:def 2
.= lim (f1/*s1 - f2/*s1) by A21,A22,A19,A23,CLVECT_1:120
.= lim ((f1-f2)/*s1) by A17,Th23;
end;
hence thesis;
end;
theorem
for f1,f2 be PartFunc of CNS,RNS, x0 be Point of CNS st f1
is_continuous_in x0 & f2 is_continuous_in x0 holds f1+f2 is_continuous_in x0 &
f1-f2 is_continuous_in x0
proof
let f1,f2 be PartFunc of CNS,RNS;
let x0 be Point of CNS;
assume that
A1: f1 is_continuous_in x0 and
A2: f2 is_continuous_in x0;
A3: x0 in dom f1 & x0 in dom f2 by A1,A2;
now
x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
hence
A4: x0 in dom (f1+f2) by VFUNCT_1:def 1;
let s1 be sequence of CNS;
assume that
A5: rng s1 c= dom(f1+f2) and
A6: s1 is convergent & lim s1=x0;
A7: rng s1 c= dom f1 /\ dom f2 by A5,VFUNCT_1:def 1;
dom (f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
then dom (f1+f2) c= dom f2 by XBOOLE_1:17;
then
A8: rng s1 c= dom f2 by A5;
then
A9: f2/*s1 is convergent by A2,A6;
dom (f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
then dom (f1+f2) c= dom f1 by XBOOLE_1:17;
then
A10: rng s1 c= dom f1 by A5;
then
A11: f1/*s1 is convergent by A1,A6;
then (f1/*s1)+(f2/*s1) is convergent by A9,NORMSP_1:19;
hence (f1+f2)/*s1 is convergent by A7,Th24;
A12: f1/.x0 = lim (f1/*s1) by A1,A6,A10;
A13: f2/.x0 = lim (f2/*s1) by A2,A6,A8;
thus (f1+f2)/.x0 = f1/.x0 + f2/.x0 by A4,VFUNCT_1:def 1
.= lim (f1/*s1 + f2/*s1) by A11,A12,A9,A13,NORMSP_1:25
.= lim ((f1+f2)/*s1) by A7,Th24;
end;
hence f1+f2 is_continuous_in x0;
now
x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
hence
A14: x0 in dom (f1-f2) by VFUNCT_1:def 2;
let s1 be sequence of CNS;
assume that
A15: rng s1 c= dom(f1-f2) and
A16: s1 is convergent & lim s1=x0;
A17: rng s1 c= dom f1 /\ dom f2 by A15,VFUNCT_1:def 2;
dom (f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
then dom (f1-f2) c= dom f2 by XBOOLE_1:17;
then
A18: rng s1 c= dom f2 by A15;
then
A19: f2/*s1 is convergent by A2,A16;
dom (f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
then dom (f1-f2) c= dom f1 by XBOOLE_1:17;
then
A20: rng s1 c= dom f1 by A15;
then
A21: f1/*s1 is convergent by A1,A16;
then f1/*s1-f2/*s1 is convergent by A19,NORMSP_1:20;
hence (f1-f2)/*s1 is convergent by A17,Th24;
A22: f1/.x0 = lim (f1/*s1) by A1,A16,A20;
A23: f2/.x0 = lim (f2/*s1) by A2,A16,A18;
thus (f1-f2)/.x0 = f1/.x0 - f2/.x0 by A14,VFUNCT_1:def 2
.= lim (f1/*s1 - f2/*s1) by A21,A22,A19,A23,NORMSP_1:26
.= lim ((f1-f2)/*s1) by A17,Th24;
end;
hence thesis;
end;
theorem
for f1,f2 be PartFunc of RNS,CNS, x0 be Point of RNS st f1
is_continuous_in x0 & f2 is_continuous_in x0 holds f1+f2 is_continuous_in x0 &
f1-f2 is_continuous_in x0
proof
let f1,f2 be PartFunc of RNS,CNS;
let x0 be Point of RNS;
assume that
A1: f1 is_continuous_in x0 and
A2: f2 is_continuous_in x0;
A3: x0 in dom f1 & x0 in dom f2 by A1,A2;
now
x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
hence
A4: x0 in dom (f1+f2) by VFUNCT_1:def 1;
let s1 be sequence of RNS;
assume that
A5: rng s1 c= dom(f1+f2) and
A6: s1 is convergent & lim s1=x0;
A7: rng s1 c= dom f1 /\ dom f2 by A5,VFUNCT_1:def 1;
dom (f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
then dom (f1+f2) c= dom f2 by XBOOLE_1:17;
then
A8: rng s1 c= dom f2 by A5;
then
A9: f2/*s1 is convergent by A2,A6;
dom (f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
then dom (f1+f2) c= dom f1 by XBOOLE_1:17;
then
A10: rng s1 c= dom f1 by A5;
then
A11: f1/*s1 is convergent by A1,A6;
then (f1/*s1)+(f2/*s1) is convergent by A9,CLVECT_1:113;
hence (f1+f2)/*s1 is convergent by A7,Th25;
A12: f1/.x0 = lim (f1/*s1) by A1,A6,A10;
A13: f2/.x0 = lim (f2/*s1) by A2,A6,A8;
thus (f1+f2)/.x0 = f1/.x0 + f2/.x0 by A4,VFUNCT_1:def 1
.= lim (f1/*s1 + f2/*s1) by A11,A12,A9,A13,CLVECT_1:119
.= lim ((f1+f2)/*s1) by A7,Th25;
end;
hence f1+f2 is_continuous_in x0;
now
x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
hence
A14: x0 in dom (f1-f2) by VFUNCT_1:def 2;
let s1 be sequence of RNS;
assume that
A15: rng s1 c= dom(f1-f2) and
A16: s1 is convergent & lim s1=x0;
A17: rng s1 c= dom f1 /\ dom f2 by A15,VFUNCT_1:def 2;
dom (f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
then dom (f1-f2) c= dom f2 by XBOOLE_1:17;
then
A18: rng s1 c= dom f2 by A15;
then
A19: f2/*s1 is convergent by A2,A16;
dom (f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
then dom (f1-f2) c= dom f1 by XBOOLE_1:17;
then
A20: rng s1 c= dom f1 by A15;
then
A21: f1/*s1 is convergent by A1,A16;
then f1/*s1-f2/*s1 is convergent by A19,CLVECT_1:114;
hence (f1-f2)/*s1 is convergent by A17,Th25;
A22: f1/.x0 = lim (f1/*s1) by A1,A16,A20;
A23: f2/.x0 = lim (f2/*s1) by A2,A16,A18;
thus (f1-f2)/.x0 = f1/.x0 - f2/.x0 by A14,VFUNCT_1:def 2
.= lim (f1/*s1 - f2/*s1) by A21,A22,A19,A23,CLVECT_1:120
.= lim ((f1-f2)/*s1) by A17,Th25;
end;
hence thesis;
end;
theorem Th35:
for f be PartFunc of CNS1,CNS2, x0 be Point of CNS1, z be
Complex st f is_continuous_in x0 holds z(#)f is_continuous_in x0
proof
let f be PartFunc of CNS1,CNS2;
let x0 be Point of CNS1;
let z be Complex;
assume
A1: f is_continuous_in x0;
then x0 in dom f;
hence
A2: x0 in dom (z(#)f) by VFUNCT_2:def 2;
let s1 be sequence of CNS1;
assume that
A3: rng s1 c= dom(z(#)f) and
A4: s1 is convergent & lim s1=x0;
A5: rng s1 c= dom f by A3,VFUNCT_2:def 2;
then
A6: f/.x0 = lim (f/*s1) by A1,A4;
A7: f/*s1 is convergent by A1,A4,A5;
then z*(f/*s1) is convergent by CLVECT_1:116;
hence (z(#)f)/*s1 is convergent by A5,Th26;
thus (z(#)f)/.x0 = z*f/.x0 by A2,VFUNCT_2:def 2
.= lim (z*(f/*s1)) by A7,A6,CLVECT_1:122
.= lim ((z(#)f)/*s1) by A5,Th26;
end;
theorem Th36:
for f be PartFunc of CNS,RNS, x0 be Point of CNS, r be Real st f
is_continuous_in x0 holds r(#)f is_continuous_in x0
proof
let f be PartFunc of CNS,RNS;
let x0 be Point of CNS;
let r be Real;
assume
A1: f is_continuous_in x0;
then x0 in dom f;
hence
A2: x0 in dom (r(#)f) by VFUNCT_1:def 4;
let s1 be sequence of CNS;
assume that
A3: rng s1 c= dom(r(#)f) and
A4: s1 is convergent & lim s1=x0;
A5: rng s1 c= dom f by A3,VFUNCT_1:def 4;
then
A6: f/.x0 = lim (f/*s1) by A1,A4;
A7: f/*s1 is convergent by A1,A4,A5;
then r*(f/*s1) is convergent by NORMSP_1:22;
hence (r(#)f)/*s1 is convergent by A5,Th27;
thus (r(#)f)/.x0 = r*f/.x0 by A2,VFUNCT_1:def 4
.= lim (r*(f/*s1)) by A7,A6,NORMSP_1:28
.= lim ((r(#)f)/*s1) by A5,Th27;
end;
theorem Th37:
for f be PartFunc of RNS,CNS, x0 be Point of RNS, z be Complex
st f is_continuous_in x0 holds z(#)f is_continuous_in x0
proof
let f be PartFunc of RNS,CNS;
let x0 be Point of RNS;
let z be Complex;
assume
A1: f is_continuous_in x0;
then x0 in dom f;
hence
A2: x0 in dom (z(#)f) by VFUNCT_2:def 2;
let s1 be sequence of RNS;
assume that
A3: rng s1 c= dom(z(#)f) and
A4: s1 is convergent & lim s1=x0;
A5: rng s1 c= dom f by A3,VFUNCT_2:def 2;
then
A6: f/.x0 = lim (f/*s1) by A1,A4;
A7: f/*s1 is convergent by A1,A4,A5;
then z*(f/*s1) is convergent by CLVECT_1:116;
hence (z(#)f)/*s1 is convergent by A5,Th28;
thus (z(#)f)/.x0 = z*f/.x0 by A2,VFUNCT_2:def 2
.= lim (z*(f/*s1)) by A7,A6,CLVECT_1:122
.= lim ((z(#)f)/*s1) by A5,Th28;
end;
theorem
for f be PartFunc of CNS1,CNS2, x0 be Point of CNS1 st f
is_continuous_in x0 holds ||. f .|| is_continuous_in x0 & -f is_continuous_in
x0
proof
let f be PartFunc of CNS1,CNS2;
let x0 be Point of CNS1;
assume
A1: f is_continuous_in x0;
then
A2: x0 in dom f;
now
thus
A3: x0 in dom (||.f .||) by A2,NORMSP_0:def 3;
let s1 be sequence of CNS1;
assume that
A4: rng s1 c= dom(||.f .||) and
A5: s1 is convergent & lim s1=x0;
A6: rng s1 c= dom f by A4,NORMSP_0:def 3;
then
A7: f/.x0 = lim (f/*s1) by A1,A5;
A8: f/*s1 is convergent by A1,A5,A6;
then ||.f/*s1.|| is convergent by CLVECT_1:117;
hence ||.f.||/*s1 is convergent by A6,Th29;
thus ||.f.||/.x0 =||.f.||.x0 by A3,PARTFUN1:def 6
.= ||.f/.x0 .|| by A3,NORMSP_0:def 3
.= lim ||.f/*s1 .|| by A8,A7,CLOPBAN1:40
.= lim (||.f.||/*s1) by A6,Th29;
end;
hence ||.f .|| is_continuous_in x0;
-f=(-1r)(#)f by VFUNCT_2:23;
hence thesis by A1,Th35;
end;
theorem
for f be PartFunc of CNS,RNS, x0 be Point of CNS st f is_continuous_in
x0 holds ||. f .|| is_continuous_in x0 & -f is_continuous_in x0
proof
let f be PartFunc of CNS,RNS;
let x0 be Point of CNS;
assume
A1: f is_continuous_in x0;
then
A2: x0 in dom f;
now
thus
A3: x0 in dom (||.f .||) by A2,NORMSP_0:def 3;
let s1 be sequence of CNS;
assume that
A4: rng s1 c= dom(||.f .||) and
A5: s1 is convergent & lim s1=x0;
A6: rng s1 c= dom f by A4,NORMSP_0:def 3;
then
A7: f/.x0 = lim (f/*s1) by A1,A5;
A8: f/*s1 is convergent by A1,A5,A6;
then ||.f/*s1.|| is convergent by NORMSP_1:23;
hence ||.f.||/*s1 is convergent by A6,Th30;
thus ||.f.||/.x0 =||.f.||.x0 by A3,PARTFUN1:def 6
.= ||.f/.x0 .|| by A3,NORMSP_0:def 3
.= lim ||.f/*s1 .|| by A8,A7,LOPBAN_1:41
.= lim (||.f.||/*s1) by A6,Th30;
end;
hence ||.f .|| is_continuous_in x0;
-f=(-1)(#)f by VFUNCT_1:23;
hence thesis by A1,Th36;
end;
theorem
for f be PartFunc of RNS,CNS, x0 be Point of RNS st f is_continuous_in
x0 holds ||. f .|| is_continuous_in x0 & -f is_continuous_in x0
proof
let f be PartFunc of RNS,CNS;
let x0 be Point of RNS;
assume
A1: f is_continuous_in x0;
then
A2: x0 in dom f;
now
thus
A3: x0 in dom (||.f .||) by A2,NORMSP_0:def 3;
let s1 be sequence of RNS;
assume that
A4: rng s1 c= dom(||.f .||) and
A5: s1 is convergent & lim s1=x0;
A6: rng s1 c= dom f by A4,NORMSP_0:def 3;
then
A7: f/.x0 = lim (f/*s1) by A1,A5;
A8: f/*s1 is convergent by A1,A5,A6;
then ||.f/*s1.|| is convergent by CLVECT_1:117;
hence ||.f.||/*s1 is convergent by A6,Th31;
thus ||.f.||/.x0 =||.f.||.x0 by A3,PARTFUN1:def 6
.= ||.f/.x0 .|| by A3,NORMSP_0:def 3
.= lim ||.f/*s1 .|| by A8,A7,CLOPBAN1:40
.= lim (||.f.||/*s1) by A6,Th31;
end;
hence ||.f .|| is_continuous_in x0;
-f=(-1r)(#)f by VFUNCT_2:23;
hence thesis by A1,Th37;
end;
definition
let CNS1,CNS2 be ComplexNormSpace;
let f be PartFunc of CNS1,CNS2;
let X be set;
pred f is_continuous_on X means
X c= dom f & for x0 be Point of CNS1
st x0 in X holds f|X is_continuous_in x0;
end;
definition
let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let f be PartFunc of CNS,RNS;
let X be set;
pred f is_continuous_on X means
X c= dom f & for x0 be Point of CNS st x0 in X holds f|X is_continuous_in x0;
end;
definition
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let g be PartFunc of RNS,CNS;
let X be set;
pred g is_continuous_on X means
X c= dom g & for x0 be Point of RNS st x0 in X holds g|X is_continuous_in x0;
end;
definition
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS, COMPLEX;
let X be set;
pred f is_continuous_on X means
X c= dom f & for x0 be Point of CNS st x0 in X holds f|X is_continuous_in x0;
end;
definition
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS, REAL;
let X be set;
pred f is_continuous_on X means
X c= dom f & for x0 be Point of CNS st x0 in X holds f|X is_continuous_in x0;
end;
definition
let RNS be RealNormSpace;
let f be PartFunc of the carrier of RNS, COMPLEX;
let X be set;
pred f is_continuous_on X means
X c= dom f & for x0 be Point of RNS st x0 in X holds f|X is_continuous_in x0;
end;
reserve X,X1 for set;
theorem Th41:
for f be PartFunc of CNS1,CNS2 holds f is_continuous_on X iff X
c= dom f & for s1 be sequence of CNS1 st rng s1 c= X & s1 is convergent & lim
s1 in X holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1)
proof
let f be PartFunc of CNS1,CNS2;
thus f is_continuous_on X implies X c= dom f & for s1 be sequence of CNS1 st
rng s1 c= X & s1 is convergent & lim s1 in X holds f/*s1 is convergent & f/.(
lim s1) = lim (f/*s1)
proof
assume
A1: f is_continuous_on X;
then
A2: X c= dom f;
now
let s1 be sequence of CNS1 such that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X;
A6: f|X is_continuous_in (lim s1) by A1,A5;
A7: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A8: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A3,A7,FUNCT_2:109
.= f/.(s1.n) by A3,A7,A8,PARTFUN2:15
.= (f/*s1).n by A2,A3,FUNCT_2:109,XBOOLE_1:1;
end;
then
A9: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
f/.(lim s1) = (f|X)/.(lim s1) by A5,A7,PARTFUN2:15
.= lim (f/*s1) by A3,A4,A7,A6,A9;
hence
f/*s1 is convergent & f/.(lim s1) = lim (f/*s1) by A3,A4,A7,A6,A9;
end;
hence thesis by A1;
end;
assume that
A10: X c= dom f and
A11: for s1 be sequence of CNS1 st rng s1 c= X & s1 is convergent & lim
s1 in X holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1);
now
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
let x1 be Point of CNS1 such that
A13: x1 in X;
now
let s1 be sequence of CNS1 such that
A14: rng s1 c= dom (f|X) and
A15: s1 is convergent and
A16: lim s1=x1;
now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A17: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A14,FUNCT_2:109
.= f/.(s1.n) by A14,A17,PARTFUN2:15
.= (f/*s1).n by A10,A12,A14,FUNCT_2:109,XBOOLE_1:1;
end;
then
A18: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
(f|X)/.(lim s1) = f/.(lim s1) by A13,A12,A16,PARTFUN2:15
.= lim ((f|X)/*s1) by A11,A13,A12,A14,A15,A16,A18;
hence (f|X)/*s1 is convergent & (f|X)/.x1 = lim ((f|X)/*s1) by A11,A13
,A12,A14,A15,A16,A18;
end;
hence f|X is_continuous_in x1 by A13,A12;
end;
hence thesis by A10;
end;
theorem Th42:
for f be PartFunc of CNS,RNS holds f is_continuous_on X iff X c=
dom f & for s1 be sequence of CNS st rng s1 c= X & s1 is convergent & lim s1 in
X holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1)
proof
let f be PartFunc of CNS,RNS;
thus f is_continuous_on X implies X c= dom f & for s1 be sequence of CNS st
rng s1 c= X & s1 is convergent & lim s1 in X holds f/*s1 is convergent & f/.(
lim s1) = lim (f/*s1)
proof
assume
A1: f is_continuous_on X;
then
A2: X c= dom f;
now
let s1 be sequence of CNS such that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X;
A6: f|X is_continuous_in (lim s1) by A1,A5;
A7: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A8: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A3,A7,FUNCT_2:109
.= f/.(s1.n) by A3,A7,A8,PARTFUN2:15
.= (f/*s1).n by A2,A3,FUNCT_2:109,XBOOLE_1:1;
end;
then
A9: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
f/.(lim s1) = (f|X)/.(lim s1) by A5,A7,PARTFUN2:15
.= lim (f/*s1) by A3,A4,A7,A6,A9;
hence
f/*s1 is convergent & f/.(lim s1) = lim (f/*s1) by A3,A4,A7,A6,A9;
end;
hence thesis by A1;
end;
assume that
A10: X c= dom f and
A11: for s1 be sequence of CNS st rng s1 c= X & s1 is convergent & lim
s1 in X holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1);
now
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
let x1 be Point of CNS such that
A13: x1 in X;
now
let s1 be sequence of CNS such that
A14: rng s1 c= dom (f|X) and
A15: s1 is convergent and
A16: lim s1=x1;
now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A17: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A14,FUNCT_2:109
.= f/.(s1.n) by A14,A17,PARTFUN2:15
.= (f/*s1).n by A10,A12,A14,FUNCT_2:109,XBOOLE_1:1;
end;
then
A18: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
(f|X)/.(lim s1) = f/.(lim s1) by A13,A12,A16,PARTFUN2:15
.= lim ((f|X)/*s1) by A11,A13,A12,A14,A15,A16,A18;
hence (f|X)/*s1 is convergent & (f|X)/.x1 = lim ((f|X)/*s1) by A11,A13
,A12,A14,A15,A16,A18;
end;
hence f|X is_continuous_in x1 by A13,A12;
end;
hence thesis by A10;
end;
theorem Th43:
for f be PartFunc of RNS,CNS holds f is_continuous_on X iff X c=
dom f & for s1 be sequence of RNS st rng s1 c= X & s1 is convergent & lim s1 in
X holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1)
proof
let f be PartFunc of RNS,CNS;
thus f is_continuous_on X implies X c= dom f & for s1 be sequence of RNS st
rng s1 c= X & s1 is convergent & lim s1 in X holds f/*s1 is convergent & f/.(
lim s1) = lim (f/*s1)
proof
assume
A1: f is_continuous_on X;
then
A2: X c= dom f;
now
let s1 be sequence of RNS such that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X;
A6: f|X is_continuous_in (lim s1) by A1,A5;
A7: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A8: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A3,A7,FUNCT_2:109
.= f/.(s1.n) by A3,A7,A8,PARTFUN2:15
.= (f/*s1).n by A2,A3,FUNCT_2:109,XBOOLE_1:1;
end;
then
A9: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
f/.(lim s1) = (f|X)/.(lim s1) by A5,A7,PARTFUN2:15
.= lim (f/*s1) by A3,A4,A7,A6,A9;
hence
f/*s1 is convergent & f/.(lim s1) = lim (f/*s1) by A3,A4,A7,A6,A9;
end;
hence thesis by A1;
end;
assume that
A10: X c= dom f and
A11: for s1 be sequence of RNS st rng s1 c= X & s1 is convergent & lim
s1 in X holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1);
now
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
let x1 be Point of RNS such that
A13: x1 in X;
now
let s1 be sequence of RNS such that
A14: rng s1 c= dom (f|X) and
A15: s1 is convergent and
A16: lim s1=x1;
now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A17: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A14,FUNCT_2:109
.= f/.(s1.n) by A14,A17,PARTFUN2:15
.= (f/*s1).n by A10,A12,A14,FUNCT_2:109,XBOOLE_1:1;
end;
then
A18: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
(f|X)/.(lim s1) = f/.(lim s1) by A13,A12,A16,PARTFUN2:15
.= lim ((f|X)/*s1) by A11,A13,A12,A14,A15,A16,A18;
hence (f|X)/*s1 is convergent & (f|X)/.x1 = lim ((f|X)/*s1) by A11,A13
,A12,A14,A15,A16,A18;
end;
hence f|X is_continuous_in x1 by A13,A12;
end;
hence thesis by A10;
end;
theorem Th44:
for f be PartFunc of CNS1,CNS2 holds f is_continuous_on X iff X
c= dom f & for x0 be Point of CNS1, r st x0 in X & 0<r ex s st 0<s & for x1 be
Point of CNS1 st x1 in X & ||. x1- x0 .|| < s holds ||. f/.x1 - f/.x0 .|| < r
proof
let f be PartFunc of CNS1,CNS2;
thus f is_continuous_on X implies X c= dom f & for x0 be Point of CNS1, r st
x0 in X & 0<r ex s st 0<s & for x1 be Point of CNS1 st x1 in X & ||. x1- x0 .||
< s holds ||. f/.x1 - f/.x0 .|| < r
proof
assume
A1: f is_continuous_on X;
hence X c= dom f;
A2: X c= dom f by A1;
let x0 be Point of CNS1,r;
assume that
A3: x0 in X and
A4: 0<r;
f|X is_continuous_in x0 by A1,A3;
then consider s such that
A5: 0<s and
A6: for x1 be Point of CNS1 st x1 in dom(f|X) & ||. x1- x0 .|| <s
holds ||. (f|X)/.x1-(f|X)/.x0 .||<r by A4,Th8;
take s;
thus 0<s by A5;
let x1 be Point of CNS1;
assume that
A7: x1 in X and
A8: ||. x1- x0 .|| <s;
A9: dom(f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
then ||. f/.x1 - f/.x0 .|| = ||. (f|X)/.x1 - f/.x0 .|| by A7,PARTFUN2:15
.= ||. (f|X)/.x1 - (f|X)/.x0 .|| by A3,A9,PARTFUN2:15;
hence thesis by A6,A9,A7,A8;
end;
assume that
A10: X c= dom f and
A11: for x0 be Point of CNS1, r st x0 in X & 0<r ex s st 0<s & for x1 be
Point of CNS1 st x1 in X & ||. x1- x0 .|| < s holds ||. f/.x1 - f/.x0 .|| < r;
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
now
let x0 be Point of CNS1 such that
A13: x0 in X;
for r st 0<r ex s st 0<s & for x1 be Point of CNS1 st x1 in dom(f|X)
& ||. x1- x0 .|| <s holds ||. (f|X)/.x1-(f|X)/.x0 .||<r
proof
let r;
assume 0<r;
then consider s such that
A14: 0<s and
A15: for x1 be Point of CNS1 st x1 in X & ||. x1- x0 .|| < s holds
||. f /.x1 - f/.x0 .|| < r by A11,A13;
take s;
thus 0<s by A14;
let x1 be Point of CNS1 such that
A16: x1 in dom(f|X) and
A17: ||. x1- x0 .|| <s;
||. (f|X)/.x1-(f|X)/.x0.|| = ||. (f|X)/.x1 - f/.x0.|| by A12,A13,
PARTFUN2:15
.= ||. f/.x1 - f/.x0 .|| by A16,PARTFUN2:15;
hence thesis by A12,A15,A16,A17;
end;
hence f|X is_continuous_in x0 by A12,A13,Th8;
end;
hence thesis by A10;
end;
theorem Th45:
for f be PartFunc of CNS,RNS holds f is_continuous_on X iff X c=
dom f & for x0 be Point of CNS, r st x0 in X & 0<r ex s st 0<s & for x1 be
Point of CNS st x1 in X & ||. x1- x0 .|| < s holds ||. f/.x1 - f/.x0 .|| < r
proof
let f be PartFunc of CNS,RNS;
thus f is_continuous_on X implies X c= dom f & for x0 be Point of CNS, r st
x0 in X & 0<r ex s st 0<s & for x1 be Point of CNS st x1 in X & ||. x1- x0 .||
< s holds ||. f/.x1 - f/.x0 .|| < r
proof
assume
A1: f is_continuous_on X;
hence X c= dom f;
A2: X c= dom f by A1;
let x0 be Point of CNS, r;
assume that
A3: x0 in X and
A4: 0<r;
f|X is_continuous_in x0 by A1,A3;
then consider s such that
A5: 0<s and
A6: for x1 be Point of CNS st x1 in dom(f|X) & ||. x1- x0 .|| <s holds
||. (f|X)/.x1-(f|X)/.x0 .||<r by A4,Th9;
take s;
thus 0<s by A5;
let x1 be Point of CNS;
assume that
A7: x1 in X and
A8: ||. x1- x0 .|| <s;
A9: dom(f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
then ||. f/.x1 - f/.x0 .|| = ||. (f|X)/.x1 - f/.x0 .|| by A7,PARTFUN2:15
.= ||. (f|X)/.x1 - (f|X)/.x0 .|| by A3,A9,PARTFUN2:15;
hence thesis by A6,A9,A7,A8;
end;
assume that
A10: X c= dom f and
A11: for x0 be Point of CNS, r st x0 in X & 0<r ex s st 0<s & for x1 be
Point of CNS st x1 in X & ||. x1- x0 .|| < s holds ||. f/.x1 - f/.x0 .|| < r;
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
now
let x0 be Point of CNS such that
A13: x0 in X;
for r st 0<r ex s st 0<s & for x1 be Point of CNS st x1 in dom(f|X) &
||. x1- x0 .|| <s holds ||. (f|X)/.x1-(f|X)/.x0 .||<r
proof
let r;
assume 0<r;
then consider s such that
A14: 0<s and
A15: for x1 be Point of CNS st x1 in X & ||. x1- x0 .|| < s holds
||. f /.x1 - f/.x0 .|| < r by A11,A13;
take s;
thus 0<s by A14;
let x1 be Point of CNS such that
A16: x1 in dom(f|X) and
A17: ||. x1- x0 .|| <s;
||. (f|X)/.x1-(f|X)/.x0.|| = ||. (f|X)/.x1 - f/.x0.|| by A12,A13,
PARTFUN2:15
.= ||. f/.x1 - f/.x0 .|| by A16,PARTFUN2:15;
hence thesis by A12,A15,A16,A17;
end;
hence f|X is_continuous_in x0 by A12,A13,Th9;
end;
hence thesis by A10;
end;
theorem Th46:
for f be PartFunc of RNS,CNS holds f is_continuous_on X iff X c=
dom f & for x0 be Point of RNS, r st x0 in X & 0<r ex s st 0<s & for x1 be
Point of RNS st x1 in X & ||. x1- x0 .|| < s holds ||. f/.x1 - f/.x0 .|| < r
proof
let f be PartFunc of RNS,CNS;
thus f is_continuous_on X implies X c= dom f & for x0 be Point of RNS, r st
x0 in X & 0<r ex s st 0<s & for x1 be Point of RNS st x1 in X & ||. x1- x0 .||
< s holds ||. f/.x1 - f/.x0 .|| < r
proof
assume
A1: f is_continuous_on X;
hence X c= dom f;
A2: X c= dom f by A1;
let x0 be Point of RNS, r;
assume that
A3: x0 in X and
A4: 0<r;
f|X is_continuous_in x0 by A1,A3;
then consider s such that
A5: 0<s and
A6: for x1 be Point of RNS st x1 in dom(f|X) & ||. x1- x0 .|| <s holds
||. (f|X)/.x1-(f|X)/.x0 .||<r by A4,Th10;
take s;
thus 0<s by A5;
let x1 be Point of RNS;
assume that
A7: x1 in X and
A8: ||. x1- x0 .|| <s;
A9: dom(f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
then ||. f/.x1 - f/.x0 .|| = ||. (f|X)/.x1 - f/.x0 .|| by A7,PARTFUN2:15
.= ||. (f|X)/.x1 - (f|X)/.x0 .|| by A3,A9,PARTFUN2:15;
hence thesis by A6,A9,A7,A8;
end;
assume that
A10: X c= dom f and
A11: for x0 be Point of RNS, r st x0 in X & 0<r ex s st 0<s & for x1 be
Point of RNS st x1 in X & ||. x1- x0 .|| < s holds ||. f/.x1 - f/.x0 .|| < r;
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
now
let x0 be Point of RNS such that
A13: x0 in X;
for r st 0<r ex s st 0<s & for x1 be Point of RNS st x1 in dom(f|X) &
||. x1- x0 .|| <s holds ||. (f|X)/.x1-(f|X)/.x0 .||<r
proof
let r;
assume 0<r;
then consider s such that
A14: 0<s and
A15: for x1 be Point of RNS st x1 in X & ||. x1- x0 .|| < s holds
||. f /.x1 - f/.x0 .|| < r by A11,A13;
take s;
thus 0<s by A14;
let x1 be Point of RNS such that
A16: x1 in dom(f|X) and
A17: ||. x1- x0 .|| <s;
||. (f|X)/.x1-(f|X)/.x0.|| = ||. (f|X)/.x1 - f/.x0.|| by A12,A13,
PARTFUN2:15
.= ||. f/.x1 - f/.x0 .|| by A16,PARTFUN2:15;
hence thesis by A12,A15,A16,A17;
end;
hence f|X is_continuous_in x0 by A12,A13,Th10;
end;
hence thesis by A10;
end;
theorem
for f be PartFunc of the carrier of CNS, COMPLEX holds ( f
is_continuous_on X iff X c= dom f & for x0 be Point of CNS, r st x0 in X & 0 <
r ex s st 0 < s & for x1 be Point of CNS st x1 in X & ||. x1- x0 .|| < s holds
|. f/.x1 - f/.x0 .| < r )
proof
let f be PartFunc of the carrier of CNS, COMPLEX;
thus f is_continuous_on X implies X c= dom f & for x0 be Point of CNS, r st
x0 in X & 0 < r ex s st 0 < s & for x1 be Point of CNS st x1 in X & ||. x1- x0
.|| < s holds |. f/.x1 - f/.x0 .| < r
proof
assume
A1: f is_continuous_on X;
hence X c= dom f;
A2: X c= dom f by A1;
let x0 be Point of CNS, r;
assume that
A3: x0 in X and
A4: 0<r;
f|X is_continuous_in x0 by A1,A3;
then consider s such that
A5: 0<s and
A6: for x1 be Point of CNS st x1 in dom(f|X) & ||. x1- x0 .|| <s holds
|. (f|X)/.x1-(f|X)/.x0 .|<r by A4,Th12;
take s;
thus 0<s by A5;
let x1 be Point of CNS;
assume that
A7: x1 in X and
A8: ||. x1- x0 .|| <s;
A9: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
then |. f/.x1 - f/.x0 .| = |. (f|X)/.x1 - f/.x0 .| by A7,PARTFUN2:15
.= |. (f|X)/.x1 - (f|X)/.x0 .| by A3,A9,PARTFUN2:15;
hence thesis by A6,A9,A7,A8;
end;
assume that
A10: X c= dom f and
A11: for x0 be Point of CNS, r st x0 in X & 0<r ex s st 0<s & for x1 be
Point of CNS st x1 in X & ||. x1- x0 .|| < s holds |. f/.x1 - f/.x0 .| < r;
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
now
let x0 be Point of CNS such that
A13: x0 in X;
for r st 0<r ex s st 0<s & for x1 be Point of CNS st x1 in dom(f|X) &
||. x1- x0 .|| <s holds |. (f|X)/.x1-(f|X)/.x0 .|<r
proof
let r;
assume 0<r;
then consider s such that
A14: 0<s and
A15: for x1 be Point of CNS st x1 in X & ||. x1- x0 .|| < s holds |.
f/. x1 - f/.x0 .| < r by A11,A13;
take s;
thus 0<s by A14;
let x1 be Point of CNS such that
A16: x1 in dom(f|X) and
A17: ||. x1- x0 .|| <s;
|. (f|X)/.x1-(f|X)/.x0 .| = |. (f|X)/.x1 - f/.x0 .| by A12,A13,
PARTFUN2:15
.= |. f/.x1 - f/.x0 .| by A16,PARTFUN2:15;
hence thesis by A12,A15,A16,A17;
end;
hence f|X is_continuous_in x0 by A12,A13,Th12;
end;
hence thesis by A10;
end;
theorem
for f be PartFunc of the carrier of CNS, REAL holds ( f
is_continuous_on X iff X c= dom f & for x0 be Point of CNS, r st x0 in X & 0 <
r ex s st 0 < s & for x1 be Point of CNS st x1 in X & ||. x1- x0 .|| < s holds
|. f/.x1 - f/.x0 .| < r )
proof
let f be PartFunc of the carrier of CNS, REAL;
thus f is_continuous_on X implies X c= dom f & for x0 be Point of CNS, r st
x0 in X & 0 < r ex s st 0 < s & for x1 be Point of CNS st x1 in X & ||. x1- x0
.|| < s holds |. f/.x1 - f/.x0 .| < r
proof
assume
A1: f is_continuous_on X;
hence X c= dom f;
A2: X c= dom f by A1;
let x0 be Point of CNS, r;
assume that
A3: x0 in X and
A4: 0<r;
f|X is_continuous_in x0 by A1,A3;
then consider s such that
A5: 0<s and
A6: for x1 be Point of CNS st x1 in dom(f|X) & ||. x1- x0 .|| <s holds
|. (f|X)/.x1-(f|X)/.x0 .|<r by A4,Th11;
take s;
thus 0<s by A5;
let x1 be Point of CNS;
assume that
A7: x1 in X and
A8: ||. x1- x0 .|| <s;
A9: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
then |. f/.x1 - f/.x0 .| = |. (f|X)/.x1 - f/.x0 .| by A7,PARTFUN2:15
.= |. (f|X)/.x1 - (f|X)/.x0 .| by A3,A9,PARTFUN2:15;
hence thesis by A6,A9,A7,A8;
end;
assume that
A10: X c= dom f and
A11: for x0 be Point of CNS,r st x0 in X & 0<r ex s st 0<s & for x1 be
Point of CNS st x1 in X & ||. x1- x0 .|| < s holds |. f/.x1 - f/.x0 .| < r;
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
now
let x0 be Point of CNS such that
A13: x0 in X;
for r st 0<r ex s st 0<s & for x1 be Point of CNS st x1 in dom(f|X) &
||. x1- x0 .|| <s holds |. (f|X)/.x1-(f|X)/.x0 .|<r
proof
let r;
assume 0<r;
then consider s such that
A14: 0<s and
A15: for x1 be Point of CNS st x1 in X & ||. x1- x0 .|| < s holds
|. f /.x1 - f/.x0 .| < r by A11,A13;
take s;
thus 0<s by A14;
let x1 be Point of CNS such that
A16: x1 in dom(f|X) and
A17: ||. x1- x0 .|| <s;
|. (f|X)/.x1-(f|X)/.x0 .| = |. (f|X)/.x1 - f/.x0 .| by A12,A13,
PARTFUN2:15
.= |. f/.x1 - f/.x0 .| by A16,PARTFUN2:15;
hence thesis by A12,A15,A16,A17;
end;
hence f|X is_continuous_in x0 by A12,A13,Th11;
end;
hence thesis by A10;
end;
theorem
for f be PartFunc of the carrier of RNS, COMPLEX holds ( f
is_continuous_on X iff X c= dom f & for x0 be Point of RNS, r st x0 in X & 0 <
r ex s st 0 < s & for x1 be Point of RNS st x1 in X & ||. x1- x0 .|| < s holds
|. f/.x1 - f/.x0 .| < r )
proof
let f be PartFunc of the carrier of RNS, COMPLEX;
thus f is_continuous_on X implies X c= dom f & for x0 be Point of RNS,r st
x0 in X & 0 < r ex s st 0 < s & for x1 be Point of RNS st x1 in X & ||. x1- x0
.|| < s holds |. f/.x1 - f/.x0 .| < r
proof
assume
A1: f is_continuous_on X;
hence X c= dom f;
A2: X c= dom f by A1;
let x0 be Point of RNS,r;
assume that
A3: x0 in X and
A4: 0<r;
f|X is_continuous_in x0 by A1,A3;
then consider s such that
A5: 0<s and
A6: for x1 be Point of RNS st x1 in dom(f|X) & ||. x1- x0 .|| <s holds
|. (f|X)/.x1-(f|X)/.x0 .|<r by A4,Th13;
take s;
thus 0<s by A5;
let x1 be Point of RNS;
assume that
A7: x1 in X and
A8: ||. x1- x0 .|| <s;
A9: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
then |. f/.x1 - f/.x0 .| = |. (f|X)/.x1 - f/.x0 .| by A7,PARTFUN2:15
.= |. (f|X)/.x1 - (f|X)/.x0 .| by A3,A9,PARTFUN2:15;
hence thesis by A6,A9,A7,A8;
end;
assume that
A10: X c= dom f and
A11: for x0 be Point of RNS, r st x0 in X & 0<r ex s st 0<s & for x1 be
Point of RNS st x1 in X & ||. x1- x0 .|| < s holds |. f/.x1 - f/.x0 .| < r;
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
now
let x0 be Point of RNS such that
A13: x0 in X;
for r st 0<r ex s st 0<s & for x1 be Point of RNS st x1 in dom(f|X) &
||. x1- x0 .|| <s holds |. (f|X)/.x1-(f|X)/.x0 .|<r
proof
let r;
assume 0<r;
then consider s such that
A14: 0<s and
A15: for x1 be Point of RNS st x1 in X & ||. x1- x0 .|| < s holds |.
f/. x1 - f/.x0 .| < r by A11,A13;
take s;
thus 0<s by A14;
let x1 be Point of RNS such that
A16: x1 in dom(f|X) and
A17: ||. x1- x0 .|| <s;
|. (f|X)/.x1-(f|X)/.x0 .| = |. (f|X)/.x1 - f/.x0 .| by A12,A13,
PARTFUN2:15
.= |. f/.x1 - f/.x0 .| by A16,PARTFUN2:15;
hence thesis by A12,A15,A16,A17;
end;
hence f|X is_continuous_in x0 by A12,A13,Th13;
end;
hence thesis by A10;
end;
theorem
for f be PartFunc of CNS1,CNS2 holds f is_continuous_on X iff f|X
is_continuous_on X
proof
let f be PartFunc of CNS1,CNS2;
thus f is_continuous_on X implies f|X is_continuous_on X
proof
assume
A1: f is_continuous_on X;
then X c= dom f;
then X c= dom f /\ X by XBOOLE_1:28;
hence X c= dom (f|X) by RELAT_1:61;
let r be Point of CNS1;
assume r in X;
then f|X is_continuous_in r by A1;
hence thesis by RELAT_1:72;
end;
assume
A2: f|X is_continuous_on X;
then X c= dom(f|X);
then dom f /\ X c= dom f & X c= dom f /\ X by RELAT_1:61,XBOOLE_1:17;
hence X c= dom f;
let r be Point of CNS1;
assume r in X;
then (f|X)|X is_continuous_in r by A2;
hence thesis by RELAT_1:72;
end;
theorem
for f be PartFunc of CNS,RNS holds f is_continuous_on X iff f|X
is_continuous_on X
proof
let f be PartFunc of CNS,RNS;
thus f is_continuous_on X implies f|X is_continuous_on X
proof
assume
A1: f is_continuous_on X;
then X c= dom f;
then X c= dom f /\ X by XBOOLE_1:28;
hence X c= dom (f|X) by RELAT_1:61;
let r be Point of CNS;
assume r in X;
then f|X is_continuous_in r by A1;
hence thesis by RELAT_1:72;
end;
assume
A2: f|X is_continuous_on X;
then X c= dom(f|X);
then dom f /\ X c= dom f & X c= dom f /\ X by RELAT_1:61,XBOOLE_1:17;
hence X c= dom f;
let r be Point of CNS;
assume r in X;
then (f|X)|X is_continuous_in r by A2;
hence thesis by RELAT_1:72;
end;
theorem
for f be PartFunc of RNS,CNS holds f is_continuous_on X iff f|X
is_continuous_on X
proof
let f be PartFunc of RNS,CNS;
thus f is_continuous_on X implies f|X is_continuous_on X
proof
assume
A1: f is_continuous_on X;
then X c= dom f;
then X c= dom f /\ X by XBOOLE_1:28;
hence X c= dom (f|X) by RELAT_1:61;
let r be Point of RNS;
assume r in X;
then f|X is_continuous_in r by A1;
hence thesis by RELAT_1:72;
end;
assume
A2: f|X is_continuous_on X;
then X c= dom(f|X);
then dom f /\ X c= dom f & X c= dom f /\ X by RELAT_1:61,XBOOLE_1:17;
hence X c= dom f;
let r be Point of RNS;
assume r in X;
then (f|X)|X is_continuous_in r by A2;
hence thesis by RELAT_1:72;
end;
theorem
for f be PartFunc of the carrier of CNS,COMPLEX holds (f
is_continuous_on X iff f|X is_continuous_on X)
proof
let f be PartFunc of the carrier of CNS,COMPLEX;
thus f is_continuous_on X implies f|X is_continuous_on X
proof
assume
A1: f is_continuous_on X;
then X c= dom f;
then X c= dom f /\ X by XBOOLE_1:28;
hence X c= dom (f|X) by RELAT_1:61;
let r be Point of CNS;
assume r in X;
then f|X is_continuous_in r by A1;
hence thesis by RELAT_1:72;
end;
assume
A2: f|X is_continuous_on X;
then X c= dom(f|X);
then dom f /\ X c= dom f & X c= dom f /\ X by RELAT_1:61,XBOOLE_1:17;
hence X c= dom f;
let r be Point of CNS;
assume r in X;
then (f|X)|X is_continuous_in r by A2;
hence thesis by RELAT_1:72;
end;
theorem Th54:
for f be PartFunc of the carrier of CNS,REAL holds (f
is_continuous_on X iff f|X is_continuous_on X)
proof
let f be PartFunc of the carrier of CNS,REAL;
thus f is_continuous_on X implies f|X is_continuous_on X
proof
assume
A1: f is_continuous_on X;
then X c= dom f;
then X c= dom f /\ X by XBOOLE_1:28;
hence X c= dom (f|X) by RELAT_1:61;
let r be Point of CNS;
assume r in X;
then f|X is_continuous_in r by A1;
hence thesis by RELAT_1:72;
end;
assume
A2: f|X is_continuous_on X;
then X c= dom(f|X);
then dom f /\ X c= dom f & X c= dom f /\ X by RELAT_1:61,XBOOLE_1:17;
hence X c= dom f;
let r be Point of CNS;
assume r in X;
then (f|X)|X is_continuous_in r by A2;
hence thesis by RELAT_1:72;
end;
theorem
for f be PartFunc of the carrier of RNS,COMPLEX holds (f
is_continuous_on X iff f|X is_continuous_on X)
proof
let f be PartFunc of the carrier of RNS,COMPLEX;
thus f is_continuous_on X implies f|X is_continuous_on X
proof
assume
A1: f is_continuous_on X;
then X c= dom f;
then X c= dom f /\ X by XBOOLE_1:28;
hence X c= dom (f|X) by RELAT_1:61;
let r be Point of RNS;
assume r in X;
then f|X is_continuous_in r by A1;
hence thesis by RELAT_1:72;
end;
assume
A2: f|X is_continuous_on X;
then X c= dom(f|X);
then dom f /\ X c= dom f & X c= dom f /\ X by RELAT_1:61,XBOOLE_1:17;
hence X c= dom f;
let r be Point of RNS;
assume r in X;
then (f|X)|X is_continuous_in r by A2;
hence thesis by RELAT_1:72;
end;
theorem Th56:
for f be PartFunc of CNS1,CNS2 st f is_continuous_on X & X1 c= X
holds f is_continuous_on X1
proof
let f be PartFunc of CNS1,CNS2;
assume that
A1: f is_continuous_on X and
A2: X1 c= X;
X c= dom f by A1;
hence
A3: X1 c= dom f by A2;
let r be Point of CNS1;
assume
A4: r in X1;
then
A5: f|X is_continuous_in r by A1,A2;
thus f|X1 is_continuous_in r
proof
dom f /\ X1 c= dom f /\ X by A2,XBOOLE_1:26;
then dom (f|X1) c= dom f /\ X by RELAT_1:61;
then
A6: dom (f|X1) c= dom (f|X) by RELAT_1:61;
r in dom f /\ X1 by A3,A4,XBOOLE_0:def 4;
hence
A7: r in dom (f|X1) by RELAT_1:61;
then
A8: (f|X)/.r = f/.r by A6,PARTFUN2:15
.= (f|X1)/.r by A7,PARTFUN2:15;
let s1 be sequence of CNS1 such that
A9: rng s1 c= dom (f|X1) and
A10: s1 is convergent & lim s1 = r;
A11: rng s1 c= dom (f|X) by A9,A6;
A12: now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A13: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A9,A6,FUNCT_2:109,XBOOLE_1:1
.= f/.(s1.n) by A11,A13,PARTFUN2:15
.= (f|X1)/.(s1.n) by A9,A13,PARTFUN2:15
.= ((f|X1)/*s1).n by A9,FUNCT_2:109;
end;
(f|X)/*s1 is convergent & (f|X)/.r = lim ((f|X)/*s1) by A5,A10,A11;
hence thesis by A8,A12,FUNCT_2:63;
end;
end;
theorem Th57:
for f be PartFunc of CNS,RNS st f is_continuous_on X & X1 c= X
holds f is_continuous_on X1
proof
let f be PartFunc of CNS,RNS;
assume that
A1: f is_continuous_on X and
A2: X1 c= X;
X c= dom f by A1;
hence
A3: X1 c= dom f by A2;
let r be Point of CNS;
assume
A4: r in X1;
then
A5: f|X is_continuous_in r by A1,A2;
thus f|X1 is_continuous_in r
proof
dom f /\ X1 c= dom f /\ X by A2,XBOOLE_1:26;
then dom (f|X1) c= dom f /\ X by RELAT_1:61;
then
A6: dom (f|X1) c= dom (f|X) by RELAT_1:61;
r in dom f /\ X1 by A3,A4,XBOOLE_0:def 4;
hence
A7: r in dom (f|X1) by RELAT_1:61;
then
A8: (f|X)/.r = f/.r by A6,PARTFUN2:15
.= (f|X1)/.r by A7,PARTFUN2:15;
let s1 be sequence of CNS such that
A9: rng s1 c= dom (f|X1) and
A10: s1 is convergent & lim s1 = r;
A11: rng s1 c= dom (f|X) by A9,A6;
A12: now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A13: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A9,A6,FUNCT_2:109,XBOOLE_1:1
.= f/.(s1.n) by A11,A13,PARTFUN2:15
.= (f|X1)/.(s1.n) by A9,A13,PARTFUN2:15
.= ((f|X1)/*s1).n by A9,FUNCT_2:109;
end;
(f|X)/*s1 is convergent & (f|X)/.r = lim ((f|X)/*s1) by A5,A10,A11;
hence thesis by A8,A12,FUNCT_2:63;
end;
end;
theorem Th58:
for f be PartFunc of RNS,CNS st f is_continuous_on X & X1 c= X
holds f is_continuous_on X1
proof
let f be PartFunc of RNS,CNS;
assume that
A1: f is_continuous_on X and
A2: X1 c= X;
X c= dom f by A1;
hence
A3: X1 c= dom f by A2;
let r be Point of RNS;
assume
A4: r in X1;
then
A5: f|X is_continuous_in r by A1,A2;
thus f|X1 is_continuous_in r
proof
dom f /\ X1 c= dom f /\ X by A2,XBOOLE_1:26;
then dom (f|X1) c= dom f /\ X by RELAT_1:61;
then
A6: dom (f|X1) c= dom (f|X) by RELAT_1:61;
r in dom f /\ X1 by A3,A4,XBOOLE_0:def 4;
hence
A7: r in dom (f|X1) by RELAT_1:61;
then
A8: (f|X)/.r = f/.r by A6,PARTFUN2:15
.= (f|X1)/.r by A7,PARTFUN2:15;
let s1 be sequence of RNS such that
A9: rng s1 c= dom (f|X1) and
A10: s1 is convergent & lim s1 = r;
A11: rng s1 c= dom (f|X) by A9,A6;
A12: now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A13: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A9,A6,FUNCT_2:109,XBOOLE_1:1
.= f/.(s1.n) by A11,A13,PARTFUN2:15
.= (f|X1)/.(s1.n) by A9,A13,PARTFUN2:15
.= ((f|X1)/*s1).n by A9,FUNCT_2:109;
end;
(f|X)/*s1 is convergent & (f|X)/.r = lim ((f|X)/*s1) by A5,A10,A11;
hence thesis by A8,A12,FUNCT_2:63;
end;
end;
theorem
for f be PartFunc of CNS1,CNS2, x0 be Point of CNS1 st x0 in dom f
holds f is_continuous_on {x0}
proof
let f be PartFunc of CNS1,CNS2;
let x0 be Point of CNS1;
assume
A1: x0 in dom f;
thus {x0} c= dom f
by A1,TARSKI:def 1;
let p be Point of CNS1 such that
A2: p in {x0};
thus f|{x0} is_continuous_in p
proof
p in dom f by A1,A2,TARSKI:def 1;
then p in dom f /\ {x0} by A2,XBOOLE_0:def 4;
hence p in dom (f|{x0}) by RELAT_1:61;
let s1 be sequence of CNS1;
assume that
A3: rng s1 c= dom(f|{x0}) and
s1 is convergent and
lim s1=p;
A4: dom f /\ {x0} c= {x0} by XBOOLE_1:17;
rng s1 c= dom f /\ {x0} by A3,RELAT_1:61;
then
A5: rng s1 c= {x0} by A4;
A6: now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:3;
hence s1.n = x0 by A5,TARSKI:def 1;
end;
A7: p=x0 by A2,TARSKI:def 1;
A8: now
let g be Real such that
A9: 0<g;
reconsider n=0 as Nat;
take n;
let m be Nat such that
n<=m;
A10: m in NAT by ORDINAL1:def 12;
||. ((f|{x0})/*s1).m - (f|{x0})/.p.|| = ||. (f|{x0})/.(s1.m) - (f|{
x0})/.x0 .|| by A7,A3,FUNCT_2:109,A10
.= ||. (f|{x0})/.x0 - (f|{x0})/.x0.|| by A6,A10
.= ||. 0.CNS2 .|| by RLVECT_1:15
.= 0 by CLVECT_1:102;
hence ||. ((f|{x0})/*s1).m - (f|{x0})/.p .|| < g by A9;
end;
hence (f|{x0})/*s1 is convergent by CLVECT_1:def 15;
hence thesis by A8,CLVECT_1:def 16;
end;
end;
theorem
for f be PartFunc of CNS,RNS, x0 be Point of CNS st x0 in dom f holds
f is_continuous_on {x0}
proof
let f be PartFunc of CNS,RNS;
let x0 be Point of CNS;
assume
A1: x0 in dom f;
thus {x0} c= dom f
by A1,TARSKI:def 1;
let p be Point of CNS such that
A2: p in {x0};
thus f|{x0} is_continuous_in p
proof
p in dom f by A1,A2,TARSKI:def 1;
then p in dom f /\ {x0} by A2,XBOOLE_0:def 4;
hence p in dom (f|{x0}) by RELAT_1:61;
let s1 be sequence of CNS;
assume that
A3: rng s1 c= dom(f|{x0}) and
s1 is convergent and
lim s1=p;
A4: dom f /\ {x0} c= {x0} by XBOOLE_1:17;
rng s1 c= dom f /\ {x0} by A3,RELAT_1:61;
then
A5: rng s1 c= {x0} by A4;
A6: now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:3;
hence s1.n = x0 by A5,TARSKI:def 1;
end;
A7: p=x0 by A2,TARSKI:def 1;
A8: now
let g be Real such that
A9: 0<g;
reconsider n=0 as Nat;
take n;
let m be Nat such that
n<=m;
A10: m in NAT by ORDINAL1:def 12;
||. ((f|{x0})/*s1).m - (f|{x0})/.p.|| = ||. (f|{x0})/.(s1.m) - (f|{
x0})/.x0 .|| by A7,A3,FUNCT_2:109,A10
.= ||. (f|{x0})/.x0 - (f|{x0})/.x0.|| by A6,A10
.= ||. 0.RNS .|| by RLVECT_1:15
.= 0 by NORMSP_1:1;
hence ||. ((f|{x0})/*s1).m - (f|{x0})/.p .|| < g by A9;
end;
hence (f|{x0})/*s1 is convergent by NORMSP_1:def 6;
hence thesis by A8,NORMSP_1:def 7;
end;
end;
theorem
for f be PartFunc of RNS,CNS, x0 be Point of RNS st x0 in dom f holds
f is_continuous_on {x0}
proof
let f be PartFunc of RNS,CNS;
let x0 be Point of RNS;
assume
A1: x0 in dom f;
thus {x0} c= dom f
by A1,TARSKI:def 1;
let p be Point of RNS such that
A2: p in {x0};
thus f|{x0} is_continuous_in p
proof
p in dom f by A1,A2,TARSKI:def 1;
then p in dom f /\ {x0} by A2,XBOOLE_0:def 4;
hence p in dom (f|{x0}) by RELAT_1:61;
let s1 be sequence of RNS;
assume that
A3: rng s1 c= dom(f|{x0}) and
s1 is convergent and
lim s1=p;
A4: dom f /\ {x0} c= {x0} by XBOOLE_1:17;
rng s1 c= dom f /\ {x0} by A3,RELAT_1:61;
then
A5: rng s1 c= {x0} by A4;
A6: now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:3;
hence s1.n = x0 by A5,TARSKI:def 1;
end;
A7: p=x0 by A2,TARSKI:def 1;
A8: now
let g be Real such that
A9: 0<g;
reconsider n=0 as Nat;
take n;
let m be Nat such that
n<=m;
A10: m in NAT by ORDINAL1:def 12;
||. ((f|{x0})/*s1).m - (f|{x0})/.p.|| = ||. (f|{x0})/.(s1.m) - (f|{
x0})/.x0 .|| by A7,A3,FUNCT_2:109,A10
.= ||. (f|{x0})/.x0 - (f|{x0})/.x0.|| by A6,A10
.= ||. 0.CNS .|| by RLVECT_1:15
.= 0 by CLVECT_1:102;
hence ||. ((f|{x0})/*s1).m - (f|{x0})/.p .|| < g by A9;
end;
hence (f|{x0})/*s1 is convergent by CLVECT_1:def 15;
hence thesis by A8,CLVECT_1:def 16;
end;
end;
theorem Th62:
for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_continuous_on X & f2
is_continuous_on X holds f1+f2 is_continuous_on X & f1-f2 is_continuous_on X
proof
let f1,f2 be PartFunc of CNS1,CNS2;
assume
A1: f1 is_continuous_on X & f2 is_continuous_on X;
then X c= dom f1 & X c= dom f2;
then
A2: X c= dom f1 /\ dom f2 by XBOOLE_1:19;
then
A3: X c= dom (f1+f2) by VFUNCT_1:def 1;
now
let s1 be sequence of CNS1;
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f1/*s1 is convergent & f2/*s1 is convergent by A1,A4,A5,A6,Th41;
then
A8: (f1/*s1)+(f2/*s1) is convergent by CLVECT_1:113;
A9: rng s1 c= dom f1 /\ dom f2 by A2,A4;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A4,A5,A6
,Th41;
then (f1+f2)/.(lim s1) = lim (f1/*s1) + lim (f2/*s1) by A3,A6,
VFUNCT_1:def 1
.= lim (f1/*s1 + f2/*s1) by A7,CLVECT_1:119
.= lim ((f1+f2)/*s1) by A9,Th23;
hence
(f1+f2)/*s1 is convergent & (f1+f2)/.(lim s1)=lim((f1+f2)/*s1) by A9,A8
,Th23;
end;
hence f1+f2 is_continuous_on X by A3,Th41;
A10: X c= dom (f1-f2) by A2,VFUNCT_1:def 2;
now
let s1 be sequence of CNS1;
assume that
A11: rng s1 c= X and
A12: s1 is convergent and
A13: lim s1 in X;
A14: f1/*s1 is convergent & f2/*s1 is convergent by A1,A11,A12,A13,Th41;
then
A15: (f1/*s1)-(f2/*s1) is convergent by CLVECT_1:114;
A16: rng s1 c= dom f1 /\ dom f2 by A2,A11;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A11,A12,A13
,Th41;
then (f1-f2)/.(lim s1) = lim (f1/*s1) - lim (f2/*s1) by A10,A13,
VFUNCT_1:def 2
.= lim (f1/*s1 - f2/*s1) by A14,CLVECT_1:120
.= lim ((f1-f2)/*s1) by A16,Th23;
hence
(f1-f2)/*s1 is convergent & (f1-f2)/.(lim s1)=lim((f1-f2)/*s1) by A16,A15
,Th23;
end;
hence thesis by A10,Th41;
end;
theorem Th63:
for f1,f2 be PartFunc of CNS,RNS st f1 is_continuous_on X & f2
is_continuous_on X holds f1+f2 is_continuous_on X & f1-f2 is_continuous_on X
proof
let f1,f2 be PartFunc of CNS,RNS;
assume
A1: f1 is_continuous_on X & f2 is_continuous_on X;
then X c= dom f1 & X c= dom f2;
then
A2: X c= dom f1 /\ dom f2 by XBOOLE_1:19;
then
A3: X c= dom (f1+f2) by VFUNCT_1:def 1;
now
let s1 be sequence of CNS;
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f1/*s1 is convergent & f2/*s1 is convergent by A1,A4,A5,A6,Th42;
then
A8: (f1/*s1)+(f2/*s1) is convergent by NORMSP_1:19;
A9: rng s1 c= dom f1 /\ dom f2 by A2,A4;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A4,A5,A6
,Th42;
then (f1+f2)/.(lim s1) = lim (f1/*s1) + lim (f2/*s1) by A3,A6,
VFUNCT_1:def 1
.= lim (f1/*s1 + f2/*s1) by A7,NORMSP_1:25
.= lim ((f1+f2)/*s1) by A9,Th24;
hence
(f1+f2)/*s1 is convergent & (f1+f2)/.(lim s1)=lim((f1+f2)/*s1) by A9,A8
,Th24;
end;
hence f1+f2 is_continuous_on X by A3,Th42;
A10: X c= dom (f1-f2) by A2,VFUNCT_1:def 2;
now
let s1 be sequence of CNS;
assume that
A11: rng s1 c= X and
A12: s1 is convergent and
A13: lim s1 in X;
A14: f1/*s1 is convergent & f2/*s1 is convergent by A1,A11,A12,A13,Th42;
then
A15: (f1/*s1)-(f2/*s1) is convergent by NORMSP_1:20;
A16: rng s1 c= dom f1 /\ dom f2 by A2,A11;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A11,A12,A13
,Th42;
then (f1-f2)/.(lim s1) = lim (f1/*s1) - lim (f2/*s1) by A10,A13,
VFUNCT_1:def 2
.= lim (f1/*s1 - f2/*s1) by A14,NORMSP_1:26
.= lim ((f1-f2)/*s1) by A16,Th24;
hence
(f1-f2)/*s1 is convergent & (f1-f2)/.(lim s1)=lim((f1-f2)/*s1) by A16,A15
,Th24;
end;
hence thesis by A10,Th42;
end;
theorem Th64:
for f1,f2 be PartFunc of RNS,CNS st f1 is_continuous_on X & f2
is_continuous_on X holds f1+f2 is_continuous_on X & f1-f2 is_continuous_on X
proof
let f1,f2 be PartFunc of RNS,CNS;
assume
A1: f1 is_continuous_on X & f2 is_continuous_on X;
then X c= dom f1 & X c= dom f2;
then
A2: X c= dom f1 /\ dom f2 by XBOOLE_1:19;
then
A3: X c= dom (f1+f2) by VFUNCT_1:def 1;
now
let s1 be sequence of RNS;
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f1/*s1 is convergent & f2/*s1 is convergent by A1,A4,A5,A6,Th43;
then
A8: (f1/*s1)+(f2/*s1) is convergent by CLVECT_1:113;
A9: rng s1 c= dom f1 /\ dom f2 by A2,A4;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A4,A5,A6
,Th43;
then (f1+f2)/.(lim s1) = lim (f1/*s1) + lim (f2/*s1) by A3,A6,
VFUNCT_1:def 1
.= lim (f1/*s1 + f2/*s1) by A7,CLVECT_1:119
.= lim ((f1+f2)/*s1) by A9,Th25;
hence
(f1+f2)/*s1 is convergent & (f1+f2)/.(lim s1)=lim((f1+f2)/*s1) by A9,A8
,Th25;
end;
hence f1+f2 is_continuous_on X by A3,Th43;
A10: X c= dom (f1-f2) by A2,VFUNCT_1:def 2;
now
let s1 be sequence of RNS;
assume that
A11: rng s1 c= X and
A12: s1 is convergent and
A13: lim s1 in X;
A14: f1/*s1 is convergent & f2/*s1 is convergent by A1,A11,A12,A13,Th43;
then
A15: (f1/*s1)-(f2/*s1) is convergent by CLVECT_1:114;
A16: rng s1 c= dom f1 /\ dom f2 by A2,A11;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A11,A12,A13
,Th43;
then (f1-f2)/.(lim s1) = lim (f1/*s1) - lim (f2/*s1) by A10,A13,
VFUNCT_1:def 2
.= lim (f1/*s1 - f2/*s1) by A14,CLVECT_1:120
.= lim ((f1-f2)/*s1) by A16,Th25;
hence
(f1-f2)/*s1 is convergent & (f1-f2)/.(lim s1)=lim((f1-f2)/*s1) by A16,A15
,Th25;
end;
hence thesis by A10,Th43;
end;
theorem
for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_continuous_on X & f2
is_continuous_on X1 holds f1+f2 is_continuous_on X /\ X1 & f1-f2
is_continuous_on X /\ X1
proof
let f1,f2 be PartFunc of CNS1,CNS2;
assume f1 is_continuous_on X & f2 is_continuous_on X1;
then f1 is_continuous_on X /\ X1 & f2 is_continuous_on X /\ X1 by Th56,
XBOOLE_1:17;
hence thesis by Th62;
end;
theorem
for f1,f2 be PartFunc of CNS,RNS st f1 is_continuous_on X & f2
is_continuous_on X1 holds f1+f2 is_continuous_on X /\ X1 & f1-f2
is_continuous_on X /\ X1
proof
let f1,f2 be PartFunc of CNS,RNS;
assume f1 is_continuous_on X & f2 is_continuous_on X1;
then f1 is_continuous_on X /\ X1 & f2 is_continuous_on X /\ X1 by Th57,
XBOOLE_1:17;
hence thesis by Th63;
end;
theorem
for f1,f2 be PartFunc of RNS,CNS st f1 is_continuous_on X & f2
is_continuous_on X1 holds f1+f2 is_continuous_on X /\ X1 & f1-f2
is_continuous_on X /\ X1
proof
let f1,f2 be PartFunc of RNS,CNS;
assume f1 is_continuous_on X & f2 is_continuous_on X1;
then f1 is_continuous_on X /\ X1 & f2 is_continuous_on X /\ X1 by Th58,
XBOOLE_1:17;
hence thesis by Th64;
end;
theorem Th68:
for f be PartFunc of CNS1,CNS2 st f is_continuous_on X holds z
(#)f is_continuous_on X
proof
let f be PartFunc of CNS1,CNS2;
assume
A1: f is_continuous_on X;
then
A2: X c= dom f;
then
A3: X c= dom(z(#)f) by VFUNCT_2:def 2;
now
let s1 be sequence of CNS1;
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f/*s1 is convergent by A1,A4,A5,A6,Th41;
then
A8: z*(f/*s1) is convergent by CLVECT_1:116;
f/.(lim s1) = lim (f/*s1) by A1,A4,A5,A6,Th41;
then (z(#)f)/.(lim s1) = z * lim (f/*s1) by A3,A6,VFUNCT_2:def 2
.= lim (z*(f/*s1)) by A7,CLVECT_1:122
.= lim ((z(#)f)/*s1) by A2,A4,Th26,XBOOLE_1:1;
hence
(z(#)f)/*s1 is convergent & (z(#)f)/.(lim s1)=lim((z(#)f)/*s1) by A2,A4,A8
,Th26,XBOOLE_1:1;
end;
hence thesis by A3,Th41;
end;
theorem Th69:
for f be PartFunc of CNS,RNS st f is_continuous_on X holds r(#)f
is_continuous_on X
proof
let f be PartFunc of CNS,RNS;
assume
A1: f is_continuous_on X;
then
A2: X c= dom f;
then
A3: X c= dom(r(#)f) by VFUNCT_1:def 4;
now
let s1 be sequence of CNS;
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f/*s1 is convergent by A1,A4,A5,A6,Th42;
then
A8: r*(f/*s1) is convergent by NORMSP_1:22;
f/.(lim s1) = lim (f/*s1) by A1,A4,A5,A6,Th42;
then (r(#)f)/.(lim s1) = r * lim (f/*s1) by A3,A6,VFUNCT_1:def 4
.= lim (r*(f/*s1)) by A7,NORMSP_1:28
.= lim ((r(#)f)/*s1) by A2,A4,Th27,XBOOLE_1:1;
hence
(r(#)f)/*s1 is convergent & (r(#)f)/.(lim s1)=lim((r(#)f)/*s1) by A2,A4,A8
,Th27,XBOOLE_1:1;
end;
hence thesis by A3,Th42;
end;
theorem Th70:
for f be PartFunc of RNS,CNS st f is_continuous_on X holds z(#)f
is_continuous_on X
proof
let f be PartFunc of RNS,CNS;
assume
A1: f is_continuous_on X;
then
A2: X c= dom f;
then
A3: X c= dom(z(#)f) by VFUNCT_2:def 2;
now
let s1 be sequence of RNS;
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f/*s1 is convergent by A1,A4,A5,A6,Th43;
then
A8: z*(f/*s1) is convergent by CLVECT_1:116;
f/.(lim s1) = lim (f/*s1) by A1,A4,A5,A6,Th43;
then (z(#)f)/.(lim s1) = z * lim (f/*s1) by A3,A6,VFUNCT_2:def 2
.= lim (z*(f/*s1)) by A7,CLVECT_1:122
.= lim ((z(#)f)/*s1) by A2,A4,Th28,XBOOLE_1:1;
hence
(z(#)f)/*s1 is convergent & (z(#)f)/.(lim s1)=lim((z(#)f)/*s1) by A2,A4,A8
,Th28,XBOOLE_1:1;
end;
hence thesis by A3,Th43;
end;
theorem Th71:
for f be PartFunc of CNS1,CNS2 st f is_continuous_on X holds ||.
f.|| is_continuous_on X & -f is_continuous_on X
proof
let f be PartFunc of CNS1,CNS2;
assume
A1: f is_continuous_on X;
thus ||.f.|| is_continuous_on X
proof
A2: X c= dom f by A1;
hence
A3: X c= dom (||.f.|| ) by NORMSP_0:def 3;
let r be Point of CNS1;
assume
A4: r in X;
then
A5: f|X is_continuous_in r by A1;
thus (||.f.|| )|X is_continuous_in r
proof
A6: r in dom (||.f.|| ) /\ X by A3,A4,XBOOLE_0:def 4;
hence r in dom ((||.f.|| )|X) by RELAT_1:61;
let s1 be sequence of CNS1;
assume that
A7: rng s1 c= dom ((||.f.|| )|X) and
A8: s1 is convergent & lim s1 = r;
rng s1 c= dom (||.f.|| ) /\ X by A7,RELAT_1:61;
then rng s1 c= dom f /\ X by NORMSP_0:def 3;
then
A9: rng s1 c= dom (f|X) by RELAT_1:61;
then
A10: (f|X)/.r = lim ((f|X)/*s1) by A5,A8;
now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A11: s1.n in rng s1 by FUNCT_1:3;
then s1.n in dom (f|X) by A9;
then
A12: s1.n in dom f /\ X by RELAT_1:61;
then
A13: s1.n in X by XBOOLE_0:def 4;
s1.n in dom f by A12,XBOOLE_0:def 4;
then
A14: s1.n in dom (||.f.|| ) by NORMSP_0:def 3;
thus (||.(f|X)/*s1.||).n = ||. ((f|X)/*s1).n .|| by NORMSP_0:def 4
.=||.(f|X)/.(s1.n).|| by A9,FUNCT_2:109
.=||.f/.(s1.n).|| by A9,A11,PARTFUN2:15
.=(||.f.|| ).(s1.n) by A14,NORMSP_0:def 3
.=((||.f.|| )|X).(s1.n) by A13,FUNCT_1:49
.=((||.f.|| )|X)/.(s1.n) by A7,A11,PARTFUN1:def 6
.=(((||.f.|| )|X)/*s1).n by A7,FUNCT_2:109;
end;
then
A15: ||.(f|X)/*s1.|| = ((||.f.|| )|X)/*s1 by FUNCT_2:63;
A16: (f|X)/*s1 is convergent by A5,A8,A9;
hence ((||.f.|| )|X)/*s1 is convergent by A15,CLVECT_1:117;
||.(f|X)/.r.|| = ||.f/.r.|| by A2,A4,PARTFUN2:17
.= (||.f.|| ).r by A3,A4,NORMSP_0:def 3
.= (||.f.|| )/.r by A3,A4,PARTFUN1:def 6
.= ((||.f.|| )|X)/.r by A6,PARTFUN2:16;
hence thesis by A16,A10,A15,CLOPBAN1:19;
end;
end;
(-1r)(#)f is_continuous_on X by A1,Th68;
hence thesis by VFUNCT_2:23;
end;
theorem Th72:
for f be PartFunc of CNS,RNS st f is_continuous_on X holds ||.f
.|| is_continuous_on X & -f is_continuous_on X
proof
let f be PartFunc of CNS,RNS;
assume
A1: f is_continuous_on X;
thus ||.f.|| is_continuous_on X
proof
A2: X c= dom f by A1;
hence
A3: X c= dom (||.f.|| ) by NORMSP_0:def 3;
let r be Point of CNS;
assume
A4: r in X;
then
A5: f|X is_continuous_in r by A1;
thus (||.f.|| )|X is_continuous_in r
proof
A6: r in dom (||.f.|| ) /\ X by A3,A4,XBOOLE_0:def 4;
hence r in dom ((||.f.|| )|X) by RELAT_1:61;
let s1 be sequence of CNS;
assume that
A7: rng s1 c= dom ((||.f.|| )|X) and
A8: s1 is convergent & lim s1 = r;
rng s1 c= dom (||.f.|| ) /\ X by A7,RELAT_1:61;
then rng s1 c= dom f /\ X by NORMSP_0:def 3;
then
A9: rng s1 c= dom (f|X) by RELAT_1:61;
then
A10: (f|X)/.r = lim ((f|X)/*s1) by A5,A8;
now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A11: s1.n in rng s1 by FUNCT_1:3;
then s1.n in dom (f|X) by A9;
then
A12: s1.n in dom f /\ X by RELAT_1:61;
then
A13: s1.n in X by XBOOLE_0:def 4;
s1.n in dom f by A12,XBOOLE_0:def 4;
then
A14: s1.n in dom (||.f.|| ) by NORMSP_0:def 3;
thus (||.(f|X)/*s1.||).n = ||. ((f|X)/*s1).n .|| by NORMSP_0:def 4
.=||.(f|X)/.(s1.n).|| by A9,FUNCT_2:109
.=||.f/.(s1.n).|| by A9,A11,PARTFUN2:15
.=(||.f.|| ).(s1.n) by A14,NORMSP_0:def 3
.=((||.f.|| )|X).(s1.n) by A13,FUNCT_1:49
.=((||.f.|| )|X)/.(s1.n) by A7,A11,PARTFUN1:def 6
.=(((||.f.|| )|X)/*s1).n by A7,FUNCT_2:109;
end;
then
A15: ||.(f|X)/*s1.|| = ((||.f.|| )|X)/*s1 by FUNCT_2:63;
A16: (f|X)/*s1 is convergent by A5,A8,A9;
hence ((||.f.|| )|X)/*s1 is convergent by A15,NORMSP_1:23;
||.(f|X)/.r.|| = ||.f/.r.|| by A2,A4,PARTFUN2:17
.= (||.f.|| ).r by A3,A4,NORMSP_0:def 3
.= (||.f.|| )/.r by A3,A4,PARTFUN1:def 6
.= ((||.f.|| )|X)/.r by A6,PARTFUN2:16;
hence thesis by A16,A10,A15,LOPBAN_1:20;
end;
end;
(-1)(#)f is_continuous_on X by A1,Th69;
hence thesis by VFUNCT_1:23;
end;
theorem Th73:
for f be PartFunc of RNS,CNS st f is_continuous_on X holds ||.f
.|| is_continuous_on X & -f is_continuous_on X
proof
let f be PartFunc of RNS,CNS;
assume
A1: f is_continuous_on X;
thus ||.f.|| is_continuous_on X
proof
A2: X c= dom f by A1;
hence
A3: X c= dom (||.f.|| ) by NORMSP_0:def 3;
let r be Point of RNS;
assume
A4: r in X;
then
A5: f|X is_continuous_in r by A1;
thus (||.f.|| )|X is_continuous_in r
proof
A6: r in dom (||.f.|| ) /\ X by A3,A4,XBOOLE_0:def 4;
hence r in dom ((||.f.|| )|X) by RELAT_1:61;
let s1 be sequence of RNS;
assume that
A7: rng s1 c= dom ((||.f.|| )|X) and
A8: s1 is convergent & lim s1 = r;
rng s1 c= dom (||.f.|| ) /\ X by A7,RELAT_1:61;
then rng s1 c= dom f /\ X by NORMSP_0:def 3;
then
A9: rng s1 c= dom (f|X) by RELAT_1:61;
then
A10: (f|X)/.r = lim ((f|X)/*s1) by A5,A8;
now
let n;
dom s1 = NAT by FUNCT_2:def 1;
then
A11: s1.n in rng s1 by FUNCT_1:3;
then s1.n in dom (f|X) by A9;
then
A12: s1.n in dom f /\ X by RELAT_1:61;
then
A13: s1.n in X by XBOOLE_0:def 4;
s1.n in dom f by A12,XBOOLE_0:def 4;
then
A14: s1.n in dom (||.f.|| ) by NORMSP_0:def 3;
thus (||.(f|X)/*s1.||).n = ||. ((f|X)/*s1).n .|| by NORMSP_0:def 4
.=||.(f|X)/.(s1.n).|| by A9,FUNCT_2:109
.=||.f/.(s1.n).|| by A9,A11,PARTFUN2:15
.=(||.f.|| ).(s1.n) by A14,NORMSP_0:def 3
.=((||.f.|| )|X).(s1.n) by A13,FUNCT_1:49
.=((||.f.|| )|X)/.(s1.n) by A7,A11,PARTFUN1:def 6
.=(((||.f.|| )|X)/*s1).n by A7,FUNCT_2:109;
end;
then
A15: ||.(f|X)/*s1.|| = ((||.f.|| )|X)/*s1 by FUNCT_2:63;
A16: (f|X)/*s1 is convergent by A5,A8,A9;
hence ((||.f.|| )|X)/*s1 is convergent by A15,CLVECT_1:117;
||.(f|X)/.r.|| = ||.f/.r.|| by A2,A4,PARTFUN2:17
.= (||.f.|| ).r by A3,A4,NORMSP_0:def 3
.= (||.f.|| )/.r by A3,A4,PARTFUN1:def 6
.= ((||.f.|| )|X)/.r by A6,PARTFUN2:16;
hence thesis by A16,A10,A15,CLOPBAN1:19;
end;
end;
(-1r)(#)f is_continuous_on X by A1,Th70;
hence thesis by VFUNCT_2:23;
end;
theorem
for f be PartFunc of CNS1,CNS2 st f is total & (for x1,x2 be Point of
CNS1 holds f/.(x1+x2) = f/.x1 + f/.x2) & (ex x0 be Point of CNS1 st f
is_continuous_in x0) holds f is_continuous_on the carrier of CNS1
proof
let f be PartFunc of CNS1,CNS2;
assume that
A1: f is total and
A2: for x1,x2 be Point of CNS1 holds f/.(x1+x2) = f/.x1 + f/.x2;
A3: dom f = the carrier of CNS1 by A1,PARTFUN1:def 2;
given x0 be Point of CNS1 such that
A4: f is_continuous_in x0;
f/.x0 + 0.CNS2 = f/.x0 by RLVECT_1:4
.= f/.(x0+0.CNS1) by RLVECT_1:4
.= f/.x0+f/.0.CNS1 by A2;
then
A5: f/.0.CNS1 = 0.CNS2 by RLVECT_1:8;
A6: now
let x1 be Point of CNS1;
0.CNS2 = f/.(x1+-x1) by A5,RLVECT_1:5
.= f/.x1+f/.(-x1) by A2;
hence -(f/.x1)=f/.(-x1) by RLVECT_1:6;
end;
A7: now
let x1,x2 be Point of CNS1;
thus f/.(x1-x2)=f/.(x1+-x2) by RLVECT_1:def 11
.= f/.x1 + f/.(-x2) by A2
.= f/.x1 +- f/.x2 by A6
.= f/.x1 - f/.x2 by RLVECT_1:def 11;
end;
now
let x1 be Point of CNS1;
let r be Real;
assume that
x1 in the carrier of CNS1 and
A8: r>0;
set y=x1-x0;
consider s such that
A9: 0<s and
A10: for x1 be Point of CNS1 st x1 in dom f & ||. x1- x0 .|| <s holds
||. f/.x1- f/.x0 .|| <r by A4,A8,Th8;
take s;
thus s>0 by A9;
let x2 be Point of CNS1 such that
x2 in the carrier of CNS1 and
A11: ||. x2-x1 .||<s;
A12: y+x0 =x1-(x0-x0) by RLVECT_1:29
.=x1- 0.CNS1 by RLVECT_1:15
.=x1 by RLVECT_1:13;
then
A13: ||.x2-y-x0.||=||.x2-x1.|| by RLVECT_1:27;
||.f/.x2-f/.x1.|| = ||.f/.x2-(f/.y+f/.x0).|| by A2,A12
.= ||.f/.x2-f/.y-f/.x0 .|| by RLVECT_1:27
.= ||.f/.(x2-y)-f/.x0.|| by A7;
hence ||.f/.x2-f/.x1.||<r by A3,A10,A11,A13;
end;
hence thesis by A3,Th44;
end;
theorem
for f be PartFunc of CNS,RNS st f is total & (for x1,x2 be Point of
CNS holds f/.(x1+x2) = f/.x1 + f/.x2) & (ex x0 be Point of CNS st f
is_continuous_in x0) holds f is_continuous_on the carrier of CNS
proof
let f be PartFunc of CNS,RNS;
assume that
A1: f is total and
A2: for x1,x2 be Point of CNS holds f/.(x1+x2) = f/.x1 + f/.x2;
A3: dom f = the carrier of CNS by A1,PARTFUN1:def 2;
given x0 be Point of CNS such that
A4: f is_continuous_in x0;
f/.x0 + 0.RNS = f/.x0 by RLVECT_1:4
.= f/.(x0+0.CNS) by RLVECT_1:4
.= f/.x0+f/.0.CNS by A2;
then
A5: f/.0.CNS = 0.RNS by RLVECT_1:8;
A6: now
let x1 be Point of CNS;
0.RNS = f/.(x1+-x1) by A5,RLVECT_1:5
.= f/.x1+f/.(-x1) by A2;
hence -(f/.x1)=f/.(-x1) by RLVECT_1:6;
end;
A7: now
let x1,x2 be Point of CNS;
thus f/.(x1-x2)=f/.(x1+-x2) by RLVECT_1:def 11
.= f/.x1 + f/.(-x2) by A2
.= f/.x1 +- f/.x2 by A6
.= f/.x1 - f/.x2 by RLVECT_1:def 11;
end;
now
let x1 be Point of CNS;
let r be Real;
assume that
x1 in the carrier of CNS and
A8: r>0;
set y=x1-x0;
consider s such that
A9: 0<s and
A10: for x1 be Point of CNS st x1 in dom f & ||. x1- x0 .|| <s holds
||. f/.x1- f/.x0 .|| <r by A4,A8,Th9;
take s;
thus s>0 by A9;
let x2 be Point of CNS such that
x2 in the carrier of CNS and
A11: ||. x2-x1 .||<s;
A12: y+x0 =x1-(x0-x0) by RLVECT_1:29
.=x1- 0.CNS by RLVECT_1:15
.=x1 by RLVECT_1:13;
then
A13: ||.x2-y-x0.||=||.x2-x1.|| by RLVECT_1:27;
||.f/.x2-f/.x1.|| = ||.f/.x2-(f/.y+f/.x0).|| by A2,A12
.= ||.f/.x2-f/.y-f/.x0 .|| by RLVECT_1:27
.= ||.f/.(x2-y)-f/.x0.|| by A7;
hence ||.f/.x2-f/.x1.||<r by A3,A10,A11,A13;
end;
hence thesis by A3,Th45;
end;
theorem
for f be PartFunc of RNS,CNS st f is total & (for x1,x2 be Point of
RNS holds f/.(x1+x2) = f/.x1 + f/.x2) & (ex x0 be Point of RNS st f
is_continuous_in x0) holds f is_continuous_on the carrier of RNS
proof
let f be PartFunc of RNS,CNS;
assume that
A1: f is total and
A2: for x1,x2 be Point of RNS holds f/.(x1+x2) = f/.x1 + f/.x2;
A3: dom f = the carrier of RNS by A1,PARTFUN1:def 2;
given x0 be Point of RNS such that
A4: f is_continuous_in x0;
f/.x0 + 0.CNS = f/.x0 by RLVECT_1:4
.= f/.(x0+0.RNS) by RLVECT_1:4
.= f/.x0+f/.0.RNS by A2;
then
A5: f/.0.RNS = 0.CNS by RLVECT_1:8;
A6: now
let x1 be Point of RNS;
0.CNS = f/.(x1+-x1) by A5,RLVECT_1:5
.= f/.x1+f/.(-x1) by A2;
hence -(f/.x1)=f/.(-x1) by RLVECT_1:6;
end;
A7: now
let x1,x2 be Point of RNS;
thus f/.(x1-x2)=f/.(x1+-x2) by RLVECT_1:def 11
.= f/.x1 + f/.(-x2) by A2
.= f/.x1 +- f/.x2 by A6
.= f/.x1 - f/.x2 by RLVECT_1:def 11;
end;
now
let x1 be Point of RNS;
let r be Real;
assume that
x1 in the carrier of RNS and
A8: r>0;
set y=x1-x0;
consider s such that
A9: 0<s and
A10: for x1 be Point of RNS st x1 in dom f & ||. x1- x0 .|| <s holds
||. f/.x1- f/.x0 .|| <r by A4,A8,Th10;
take s;
thus s>0 by A9;
let x2 be Point of RNS such that
x2 in the carrier of RNS and
A11: ||. x2-x1 .||<s;
A12: y+x0 =x1-(x0-x0) by RLVECT_1:29
.=x1- 0.RNS by RLVECT_1:15
.=x1 by RLVECT_1:13;
then
A13: ||.x2-y-x0.||=||.x2-x1.|| by RLVECT_1:27;
||.f/.x2-f/.x1.|| = ||.f/.x2-(f/.y+f/.x0).|| by A2,A12
.= ||.f/.x2-f/.y-f/.x0 .|| by RLVECT_1:27
.= ||.f/.(x2-y)-f/.x0.|| by A7;
hence ||.f/.x2-f/.x1.||<r by A3,A10,A11,A13;
end;
hence thesis by A3,Th46;
end;
theorem Th77:
for f be PartFunc of CNS1,CNS2 st dom f is compact & f
is_continuous_on (dom f) holds (rng f) is compact
proof
let f be PartFunc of CNS1,CNS2;
assume that
A1: dom f is compact and
A2: f is_continuous_on (dom f);
now
let s1 be sequence of CNS2 such that
A3: rng s1 c= rng f;
defpred P[set,set] means $2 in dom f & f/.$2=s1.$1;
A4: for n ex p be Point of CNS1 st P[n,p]
proof
let n;
dom s1 = NAT by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:3;
then consider p be Point of CNS1 such that
A5: p in dom f & s1.n = f.p by A3,PARTFUN1:3;
take p;
thus thesis by A5,PARTFUN1:def 6;
end;
consider q1 be sequence of CNS1 such that
A6: for n holds P[n,q1.n]from FUNCT_2:sch 3(A4);
now
let x be object;
assume x in rng q1;
then consider n being Nat such that
A7: x = q1.n by Th7;
n in NAT by ORDINAL1:def 12;
hence x in dom f by A6,A7;
end;
then
A8: rng q1 c= dom f;
then consider s2 be sequence of CNS1 such that
A9: s2 is subsequence of q1 and
A10: s2 is convergent and
A11: (lim s2) in dom f by A1;
take q2 = f/*s2;
rng s2 c= rng q1 by A9,VALUED_0:21;
then
A12: rng s2 c= dom f by A8;
now
let n;
f/.(q1.n)=s1.n by A6;
hence (f/*q1).n= s1.n by A8,FUNCT_2:109;
end;
then
A13: f/*q1=s1 by FUNCT_2:63;
f|(dom f) is_continuous_in (lim s2) by A2,A11;
then
A14: f is_continuous_in (lim s2) by RELAT_1:68;
then f/.(lim s2) = lim (f/*s2) by A10,A12;
hence
q2 is subsequence of s1 & q2 is convergent & (lim q2) in rng f by A8,A13,A9
,A10,A14,A12,PARTFUN2:2,VALUED_0:22;
end;
hence thesis;
end;
theorem Th78:
for f be PartFunc of CNS,RNS st dom f is compact & f
is_continuous_on (dom f) holds (rng f) is compact
proof
let f be PartFunc of CNS,RNS;
assume that
A1: dom f is compact and
A2: f is_continuous_on (dom f);
now
let s1 be sequence of RNS such that
A3: rng s1 c= rng f;
defpred P[set,set] means $2 in dom f & f/.$2=s1.$1;
A4: for n ex p be Point of CNS st P[n,p]
proof
let n;
dom s1 = NAT by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:3;
then consider p be Point of CNS such that
A5: p in dom f & s1.n = f.p by A3,PARTFUN1:3;
take p;
thus thesis by A5,PARTFUN1:def 6;
end;
consider q1 be sequence of CNS such that
A6: for n holds P[n,q1.n]from FUNCT_2:sch 3(A4);
now
let x be object;
assume x in rng q1;
then consider n being Nat such that
A7: x = q1.n by Th7;
n in NAT by ORDINAL1:def 12;
hence x in dom f by A6,A7;
end;
then
A8: rng q1 c= dom f;
then consider s2 be sequence of CNS such that
A9: s2 is subsequence of q1 and
A10: s2 is convergent and
A11: (lim s2) in dom f by A1;
take q2 = f/*s2;
rng s2 c= rng q1 by A9,VALUED_0:21;
then
A12: rng s2 c= dom f by A8;
now
let n;
f/.(q1.n)=s1.n by A6;
hence (f/*q1).n= s1.n by A8,FUNCT_2:109;
end;
then
A13: f/*q1=s1 by FUNCT_2:63;
f|(dom f) is_continuous_in (lim s2) by A2,A11;
then
A14: f is_continuous_in (lim s2) by RELAT_1:68;
then f/.(lim s2) = lim (f/*s2) by A10,A12;
hence
q2 is subsequence of s1 & q2 is convergent & (lim q2) in rng f by A8,A13,A9
,A10,A14,A12,PARTFUN2:2,VALUED_0:22;
end;
hence thesis;
end;
theorem Th79:
for f be PartFunc of RNS,CNS st dom f is compact & f
is_continuous_on (dom f) holds (rng f) is compact
proof
let f be PartFunc of RNS,CNS;
assume that
A1: dom f is compact and
A2: f is_continuous_on (dom f);
now
let s1 be sequence of CNS such that
A3: rng s1 c= rng f;
defpred P[set,set] means $2 in dom f & f/.$2=s1.$1;
A4: for n ex p be Point of RNS st P[n,p]
proof
let n;
dom s1 = NAT by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:3;
then consider p be Point of RNS such that
A5: p in dom f & s1.n = f.p by A3,PARTFUN1:3;
take p;
thus thesis by A5,PARTFUN1:def 6;
end;
consider q1 be sequence of RNS such that
A6: for n holds P[n,q1.n]from FUNCT_2:sch 3(A4);
now
let x be object;
assume x in rng q1;
then consider n being Nat such that
A7: x = q1.n by NFCONT_1:6;
n in NAT by ORDINAL1:def 12;
hence x in dom f by A6,A7;
end;
then
A8: rng q1 c= dom f;
then consider s2 be sequence of RNS such that
A9: s2 is subsequence of q1 and
A10: s2 is convergent and
A11: (lim s2) in dom f by A1;
take q2 = f/*s2;
rng s2 c= rng q1 by A9,VALUED_0:21;
then
A12: rng s2 c= dom f by A8;
now
let n;
f/.(q1.n)=s1.n by A6;
hence (f/*q1).n= s1.n by A8,FUNCT_2:109;
end;
then
A13: f/*q1=s1 by FUNCT_2:63;
f|(dom f) is_continuous_in (lim s2) by A2,A11;
then
A14: f is_continuous_in (lim s2) by RELAT_1:68;
then f/.(lim s2) = lim (f/*s2) by A10,A12;
hence
q2 is subsequence of s1 & q2 is convergent & (lim q2) in rng f by A8,A13,A9
,A10,A14,A12,PARTFUN2:2,VALUED_0:22;
end;
hence thesis;
end;
theorem
for f be PartFunc of the carrier of CNS,COMPLEX st dom f is compact &
f is_continuous_on (dom f) holds (rng f) is compact
proof
let f be PartFunc of the carrier of CNS,COMPLEX;
assume that
A1: dom f is compact and
A2: f is_continuous_on (dom f);
now
let s1 be Complex_Sequence such that
A3: rng s1 c= rng f;
defpred P[set,set] means $2 in dom f & f/.$2=s1.$1;
A4: for n ex p be Point of CNS st P[n,p]
proof
let n;
dom s1 = NAT by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:3;
then consider p be Point of CNS such that
A5: p in dom f & s1.n = f.p by A3,PARTFUN1:3;
take p;
thus thesis by A5,PARTFUN1:def 6;
end;
consider q1 be sequence of CNS such that
A6: for n holds P[n,q1.n]from FUNCT_2:sch 3(A4);
now
let x be object;
assume x in rng q1;
then consider n being Nat such that
A7: x = q1.n by Th7;
n in NAT by ORDINAL1:def 12;
hence x in dom f by A6,A7;
end;
then
A8: rng q1 c= dom f;
then consider s2 be sequence of CNS such that
A9: s2 is subsequence of q1 and
A10: s2 is convergent and
A11: (lim s2) in dom f by A1;
take q2 = f/*s2;
rng s2 c= rng q1 by A9,VALUED_0:21;
then
A12: rng s2 c= dom f by A8;
now
let n;
f/.(q1.n)=s1.n by A6;
hence (f/*q1).n= s1.n by A8,FUNCT_2:109;
end;
then
A13: f/*q1=s1 by FUNCT_2:63;
f|(dom f) is_continuous_in (lim s2) by A2,A11;
then
A14: f is_continuous_in (lim s2) by RELAT_1:68;
then f/.(lim s2) = lim (f/*s2) by A10,A12;
hence
q2 is subsequence of s1 & q2 is convergent & (lim q2) in rng f by A8,A13,A9
,A10,A14,A12,PARTFUN2:2,VALUED_0:22;
end;
hence thesis by CFCONT_1:def 3;
end;
theorem Th81:
for f be PartFunc of the carrier of CNS,REAL st dom f is
compact & f is_continuous_on (dom f) holds (rng f) is compact
proof
let f be PartFunc of the carrier of CNS,REAL;
assume that
A1: dom f is compact and
A2: f is_continuous_on (dom f);
now
let s1 be Real_Sequence such that
A3: rng s1 c= rng f;
defpred P[set,set] means $2 in dom f & f/.$2=s1.$1;
A4: for n ex p be Point of CNS st P[n,p]
proof
let n;
dom s1 = NAT by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:3;
then consider p be Point of CNS such that
A5: p in dom f & s1.n = f.p by A3,PARTFUN1:3;
take p;
thus thesis by A5,PARTFUN1:def 6;
end;
consider q1 be sequence of CNS such that
A6: for n holds P[n,q1.n]from FUNCT_2:sch 3(A4);
now
let x be object;
assume x in rng q1;
then consider n being Nat such that
A7: x = q1.n by Th7;
n in NAT by ORDINAL1:def 12;
hence x in dom f by A6,A7;
end;
then
A8: rng q1 c= dom f;
then consider s2 be sequence of CNS such that
A9: s2 is subsequence of q1 and
A10: s2 is convergent and
A11: (lim s2) in dom f by A1;
take q2 = f/*s2;
rng s2 c= rng q1 by A9,VALUED_0:21;
then
A12: rng s2 c= dom f by A8;
now
let n;
f/.(q1.n)=s1.n by A6;
hence (f/*q1).n= s1.n by A8,FUNCT_2:109;
end;
then
A13: f/*q1=s1 by FUNCT_2:63;
f|(dom f) is_continuous_in (lim s2) by A2,A11;
then
A14: f is_continuous_in (lim s2) by RELAT_1:68;
then f/.(lim s2) = lim (f/*s2) by A10,A12;
hence q2 is subsequence of s1 & q2 is convergent & (lim q2) in (rng f) by
A8,A13,A9,A10,A14,A12,PARTFUN2:2,VALUED_0:22;
end;
hence thesis by RCOMP_1:def 3;
end;
theorem
for f be PartFunc of the carrier of RNS,COMPLEX st dom f is compact &
f is_continuous_on (dom f) holds (rng f) is compact
proof
let f be PartFunc of the carrier of RNS,COMPLEX;
assume that
A1: dom f is compact and
A2: f is_continuous_on (dom f);
now
let s1 be Complex_Sequence such that
A3: rng s1 c= rng f;
defpred P[set,set] means $2 in dom f & f/.$2=s1.$1;
A4: for n ex p be Point of RNS st P[n,p]
proof
let n;
dom s1 = NAT by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:3;
then consider p be Point of RNS such that
A5: p in dom f & s1.n = f.p by A3,PARTFUN1:3;
take p;
thus thesis by A5,PARTFUN1:def 6;
end;
consider q1 be sequence of RNS such that
A6: for n holds P[n,q1.n] from FUNCT_2:sch 3(A4);
now
let x be object;
assume x in rng q1;
then consider n being Nat such that
A7: x = q1.n by NFCONT_1:6;
n in NAT by ORDINAL1:def 12;
hence x in dom f by A6,A7;
end;
then
A8: rng q1 c= dom f;
then consider s2 be sequence of RNS such that
A9: s2 is subsequence of q1 and
A10: s2 is convergent and
A11: (lim s2) in dom f by A1;
take q2 = f/*s2;
rng s2 c= rng q1 by A9,VALUED_0:21;
then
A12: rng s2 c= dom f by A8;
now
let n;
f/.(q1.n)=s1.n by A6;
hence (f/*q1).n= s1.n by A8,FUNCT_2:109;
end;
then
A13: f/*q1=s1 by FUNCT_2:63;
f|(dom f) is_continuous_in (lim s2) by A2,A11;
then
A14: f is_continuous_in (lim s2) by RELAT_1:68;
then f/.(lim s2) = lim (f/*s2) by A10,A12;
hence
q2 is subsequence of s1 & q2 is convergent & (lim q2) in rng f by A8,A13,A9
,A10,A14,A12,PARTFUN2:2,VALUED_0:22;
end;
hence thesis by CFCONT_1:def 3;
end;
theorem
for Y be Subset of CNS1, f be PartFunc of CNS1,CNS2 st Y c= dom f & Y
is compact & f is_continuous_on Y holds (f.:Y) is compact
proof
let Y be Subset of CNS1;
let f be PartFunc of CNS1,CNS2;
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f is_continuous_on Y;
A4: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A1,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A4;
let r be Point of CNS1;
assume r in Y;
then f|Y is_continuous_in r by A3;
hence thesis by RELAT_1:72;
end;
then rng (f|Y) is compact by A2,A4,Th77;
hence thesis by RELAT_1:115;
end;
theorem
for Y be Subset of CNS, f be PartFunc of CNS,RNS st Y c= dom f & Y is
compact & f is_continuous_on Y holds (f.:Y) is compact
proof
let Y be Subset of CNS;
let f be PartFunc of CNS,RNS;
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f is_continuous_on Y;
A4: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A1,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A4;
let r be Point of CNS;
assume r in Y;
then f|Y is_continuous_in r by A3;
hence thesis by RELAT_1:72;
end;
then rng (f|Y) is compact by A2,A4,Th78;
hence thesis by RELAT_1:115;
end;
theorem
for Y be Subset of RNS, f be PartFunc of RNS,CNS st Y c= dom f & Y is
compact & f is_continuous_on Y holds (f.:Y) is compact
proof
let Y be Subset of RNS;
let f be PartFunc of RNS,CNS;
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f is_continuous_on Y;
A4: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A1,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A4;
let r be Point of RNS;
assume r in Y;
then f|Y is_continuous_in r by A3;
hence thesis by RELAT_1:72;
end;
then rng (f|Y) is compact by A2,A4,Th79;
hence thesis by RELAT_1:115;
end;
theorem Th86:
for f be PartFunc of the carrier of CNS,REAL st dom f<>{} & (
dom f) is compact & f is_continuous_on (dom f) holds ex x1,x2 be Point of CNS
st x1 in dom f & x2 in dom f & f/.x1 = upper_bound (rng f) & f/.x2 =
lower_bound (rng f)
proof
let f be PartFunc of the carrier of CNS,REAL;
assume dom f <> {} & dom f is compact & f is_continuous_on (dom f);
then
A1: rng f <> {} & rng f is compact by Th81,RELAT_1:42;
then consider x being Element of CNS such that
A2: x in dom f & upper_bound (rng f) = f.x by PARTFUN1:3,RCOMP_1:14;
take x;
consider y being Element of CNS such that
A3: y in dom f & lower_bound (rng f ) = f.y by A1,PARTFUN1:3,RCOMP_1:14;
take y;
thus thesis by A2,A3,PARTFUN1:def 6;
end;
theorem Th87:
for f be PartFunc of CNS1,CNS2 st dom f<>{} & (dom f) is
compact & f is_continuous_on (dom f) holds ex x1,x2 be Point of CNS1 st x1 in
dom f & x2 in dom f & ||.f.||/.x1 = upper_bound (rng ||.f.||) & ||.f.||/.x2 =
lower_bound (rng ||.f.||)
proof
let f be PartFunc of CNS1,CNS2 such that
A1: dom f <> {} and
A2: dom f is compact and
A3: f is_continuous_on (dom f);
A4: dom f = dom ||.f.|| by NORMSP_0:def 3;
dom ||.f.|| is compact by A2,NORMSP_0:def 3;
then
A5: rng ||.f.|| is compact by A3,A4,Th71,Th81;
A6: rng ||.f.|| <> {} by A1,A4,RELAT_1:42;
then consider x being Element of CNS1 such that
A7: x in dom ||.f.|| & upper_bound (rng ||.f.||) = ||.f.||.x by A5,PARTFUN1:3
,RCOMP_1:14;
consider y being Element of CNS1 such that
A8: y in dom ||.f.|| & lower_bound (rng ||.f.||) = ||.f.||.y by A6,A5,
PARTFUN1:3,RCOMP_1:14;
take x;
take y;
thus thesis by A7,A8,NORMSP_0:def 3,PARTFUN1:def 6;
end;
theorem Th88:
for f be PartFunc of CNS,RNS st dom f<>{} & (dom f) is compact
& f is_continuous_on (dom f) holds ex x1,x2 be Point of CNS st x1 in dom f & x2
in dom f & ||.f.||/.x1 = upper_bound (rng ||.f.||) & ||.f.||/.x2 = lower_bound
(rng ||.f.||)
proof
let f be PartFunc of CNS,RNS such that
A1: dom f <> {} and
A2: dom f is compact and
A3: f is_continuous_on (dom f);
A4: dom f = dom ||.f.|| by NORMSP_0:def 3;
dom ||.f.|| is compact by A2,NORMSP_0:def 3;
then
A5: rng ||.f.|| is compact by A3,A4,Th72,Th81;
A6: rng ||.f.|| <> {} by A1,A4,RELAT_1:42;
then consider x being Element of CNS such that
A7: x in dom ||.f.|| & upper_bound (rng ||.f.||) = ||.f.||.x by A5,PARTFUN1:3
,RCOMP_1:14;
consider y being Element of CNS such that
A8: y in dom ||.f.|| & lower_bound (rng ||.f.||) = ||.f.||.y by A6,A5,
PARTFUN1:3,RCOMP_1:14;
take x;
take y;
thus thesis by A7,A8,NORMSP_0:def 3,PARTFUN1:def 6;
end;
theorem Th89:
for f be PartFunc of RNS,CNS st dom f<>{} & (dom f) is compact
& f is_continuous_on (dom f) holds ex x1,x2 be Point of RNS st x1 in dom f & x2
in dom f & ||.f.||/.x1 = upper_bound (rng ||.f.||) & ||.f.||/.x2 = lower_bound
(rng ||.f.||)
proof
let f be PartFunc of RNS,CNS such that
A1: dom f <> {} and
A2: dom f is compact and
A3: f is_continuous_on (dom f);
A4: dom f = dom ||.f.|| by NORMSP_0:def 3;
dom ||.f.|| is compact by A2,NORMSP_0:def 3;
then
A5: rng ||.f.|| is compact by A3,A4,Th73,NFCONT_1:31;
A6: rng ||.f.|| <> {} by A1,A4,RELAT_1:42;
then consider x being Element of RNS such that
A7: x in dom ||.f.|| & upper_bound (rng ||.f.||) = ||.f.||.x by A5,PARTFUN1:3
,RCOMP_1:14;
consider y being Element of RNS such that
A8: y in dom ||.f.|| & lower_bound (rng ||.f.||) = ||.f.||.y by A6,A5,
PARTFUN1:3,RCOMP_1:14;
take x;
take y;
thus thesis by A7,A8,NORMSP_0:def 3,PARTFUN1:def 6;
end;
theorem Th90:
for f be PartFunc of CNS1,CNS2 holds (||.f.||)|X = ||.(f|X).||
proof
let f be PartFunc of CNS1,CNS2;
A1: dom ((||.f.||)|X) = dom (||.f.||) /\ X by RELAT_1:61
.= dom f /\ X by NORMSP_0:def 3
.= dom (f|X) by RELAT_1:61
.= dom ( ||.(f|X).||) by NORMSP_0:def 3;
now
let c be Point of CNS1;
assume
A2: c in dom ((||.f.||)|X);
then
A3: c in dom (f|X) by A1,NORMSP_0:def 3;
c in dom (||.f.||) /\ X by A2,RELAT_1:61;
then
A4: c in dom (||.f.||) by XBOOLE_0:def 4;
thus ((||.f.||)|X).c = (||.f.||).c by A2,FUNCT_1:47
.= ||.f/.c.|| by A4,NORMSP_0:def 3
.= ||.(f|X)/.c.|| by A3,PARTFUN2:15
.= ||.(f|X).||.c by A1,A2,NORMSP_0:def 3;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th91:
for f be PartFunc of CNS,RNS holds (||.f.||)|X = ||.(f|X).||
proof
let f be PartFunc of CNS,RNS;
A1: dom ((||.f.||)|X) = dom (||.f.||) /\ X by RELAT_1:61
.= dom f /\ X by NORMSP_0:def 3
.= dom (f|X) by RELAT_1:61
.= dom ( ||.(f|X).||) by NORMSP_0:def 3;
now
let c be Point of CNS;
assume
A2: c in dom ((||.f.||)|X);
then
A3: c in dom (f|X) by A1,NORMSP_0:def 3;
c in dom (||.f.||) /\ X by A2,RELAT_1:61;
then
A4: c in dom (||.f.||) by XBOOLE_0:def 4;
thus ((||.f.||)|X).c = (||.f.||).c by A2,FUNCT_1:47
.= ||.f/.c.|| by A4,NORMSP_0:def 3
.= ||.(f|X)/.c.|| by A3,PARTFUN2:15
.= ||.(f|X).||.c by A1,A2,NORMSP_0:def 3;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th92:
for f be PartFunc of RNS,CNS holds (||.f.||)|X = ||.(f|X).||
proof
let f be PartFunc of RNS,CNS;
A1: dom ((||.f.||)|X) = dom (||.f.||) /\ X by RELAT_1:61
.= dom f /\ X by NORMSP_0:def 3
.= dom (f|X) by RELAT_1:61
.= dom ( ||.(f|X).||) by NORMSP_0:def 3;
now
let c be Point of RNS;
assume
A2: c in dom ((||.f.||)|X);
then
A3: c in dom (f|X) by A1,NORMSP_0:def 3;
c in dom (||.f.||) /\ X by A2,RELAT_1:61;
then
A4: c in dom (||.f.||) by XBOOLE_0:def 4;
thus ((||.f.||)|X).c = (||.f.||).c by A2,FUNCT_1:47
.= ||.f/.c.|| by A4,NORMSP_0:def 3
.= ||.(f|X)/.c.|| by A3,PARTFUN2:15
.= ||.(f|X).||.c by A1,A2,NORMSP_0:def 3;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem
for f be PartFunc of CNS1,CNS2, Y be Subset of CNS1 st Y<>{} & Y c=
dom f & Y is compact & f is_continuous_on Y holds ex x1,x2 be Point of CNS1 st
x1 in Y & x2 in Y & ||.f.||/.x1 = upper_bound (||.f.||.:Y) & ||.f.||/.x2 =
lower_bound (||.f.||.:Y)
proof
let f be PartFunc of CNS1,CNS2;
let Y be Subset of CNS1 such that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f is_continuous_on Y;
A5: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A2,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A5;
let r be Point of CNS1;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 be Point of CNS1 such that
A6: x1 in dom (f|Y) and
A7: x2 in dom (f|Y) and
A8: ||.(f|Y).||/.x1 = upper_bound (rng ||.(f|Y).||) & ||.(f|Y).||/.x2 =
lower_bound (rng ||.(f|Y).||) by A1,A3,A5,Th87;
A9: dom f = dom ||.f.|| by NORMSP_0:def 3;
take x1,x2;
thus x1 in Y & x2 in Y by A5,A6,A7;
A10: ||.f.||.:Y =rng ( ||.f.|| | Y) by RELAT_1:115
.=rng( ||.(f|Y).|| ) by Th90;
A11: x2 in dom ||.(f|Y).|| by A7,NORMSP_0:def 3;
then
A12: ||.(f|Y).||/.x2 =||.(f|Y).||.x2 by PARTFUN1:def 6
.=||. (f|Y)/.x2.|| by A11,NORMSP_0:def 3
.=||. f/.x2.|| by A7,PARTFUN2:15
.=||. f.||.x2 by A2,A5,A7,A9,NORMSP_0:def 3
.=||. f.||/.x2 by A2,A5,A7,A9,PARTFUN1:def 6;
A13: x1 in dom ||.(f|Y).|| by A6,NORMSP_0:def 3;
then ||.(f|Y).||/.x1 =||.(f|Y).||.x1 by PARTFUN1:def 6
.=||. (f|Y)/.x1.|| by A13,NORMSP_0:def 3
.=||. f/.x1.|| by A6,PARTFUN2:15
.=||. f.||.x1 by A2,A5,A6,A9,NORMSP_0:def 3
.=||. f.||/.x1 by A2,A5,A6,A9,PARTFUN1:def 6;
hence thesis by A8,A12,A10;
end;
theorem
for f be PartFunc of CNS,RNS,Y be Subset of CNS st Y<>{} & Y c= dom f
& Y is compact & f is_continuous_on Y holds ex x1,x2 be Point of CNS st x1 in Y
& x2 in Y & ||.f.||/.x1 = upper_bound (||.f.||.:Y) & ||.f.||/.x2 = lower_bound
(||.f.||.:Y)
proof
let f be PartFunc of CNS,RNS;
let Y be Subset of CNS such that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f is_continuous_on Y;
A5: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A2,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A5;
let r be Point of CNS;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 be Point of CNS such that
A6: x1 in dom (f|Y) and
A7: x2 in dom (f|Y) and
A8: ||.(f|Y).||/.x1 = upper_bound (rng ||.(f|Y).||) & ||.(f|Y).||/.x2 =
lower_bound (rng ||.(f|Y).||) by A1,A3,A5,Th88;
A9: dom f = dom ||.f.|| by NORMSP_0:def 3;
take x1,x2;
thus x1 in Y & x2 in Y by A5,A6,A7;
A10: ||.f.||.:Y =rng ( ||.f.|| | Y) by RELAT_1:115
.=rng( ||.(f|Y).|| ) by Th91;
A11: x2 in dom ||.(f|Y).|| by A7,NORMSP_0:def 3;
then
A12: ||.(f|Y).||/.x2 =||.(f|Y).||.x2 by PARTFUN1:def 6
.=||. (f|Y)/.x2.|| by A11,NORMSP_0:def 3
.=||. f/.x2.|| by A7,PARTFUN2:15
.=||. f.||.x2 by A2,A5,A7,A9,NORMSP_0:def 3
.=||. f.||/.x2 by A2,A5,A7,A9,PARTFUN1:def 6;
A13: x1 in dom ||.(f|Y).|| by A6,NORMSP_0:def 3;
then ||.(f|Y).||/.x1 =||.(f|Y).||.x1 by PARTFUN1:def 6
.=||. (f|Y)/.x1.|| by A13,NORMSP_0:def 3
.=||. f/.x1.|| by A6,PARTFUN2:15
.=||. f.||.x1 by A2,A5,A6,A9,NORMSP_0:def 3
.=||. f.||/.x1 by A2,A5,A6,A9,PARTFUN1:def 6;
hence thesis by A8,A12,A10;
end;
theorem
for f be PartFunc of RNS,CNS,Y be Subset of RNS st Y<>{} & Y c= dom f
& Y is compact & f is_continuous_on Y holds ex x1,x2 be Point of RNS st x1 in Y
& x2 in Y & ||.f.||/.x1 = upper_bound (||.f.||.:Y) & ||.f.||/.x2 = lower_bound
(||.f.||.:Y)
proof
let f be PartFunc of RNS,CNS;
let Y be Subset of RNS such that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f is_continuous_on Y;
A5: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A2,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A5;
let r be Point of RNS;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 be Point of RNS such that
A6: x1 in dom (f|Y) and
A7: x2 in dom (f|Y) and
A8: ||.(f|Y).||/.x1 = upper_bound (rng ||.(f|Y).||) & ||.(f|Y).||/.x2 =
lower_bound (rng ||.(f|Y).||) by A1,A3,A5,Th89;
A9: dom f = dom ||.f.|| by NORMSP_0:def 3;
take x1,x2;
thus x1 in Y & x2 in Y by A5,A6,A7;
A10: ||.f.||.:Y =rng ( ||.f.|| | Y) by RELAT_1:115
.=rng( ||.(f|Y).|| ) by Th92;
A11: x2 in dom ||.(f|Y).|| by A7,NORMSP_0:def 3;
then
A12: ||.(f|Y).||/.x2 =||.(f|Y).||.x2 by PARTFUN1:def 6
.=||. (f|Y)/.x2.|| by A11,NORMSP_0:def 3
.=||. f/.x2.|| by A7,PARTFUN2:15
.=||. f.||.x2 by A2,A5,A7,A9,NORMSP_0:def 3
.=||. f.||/.x2 by A2,A5,A7,A9,PARTFUN1:def 6;
A13: x1 in dom ||.(f|Y).|| by A6,NORMSP_0:def 3;
then ||.(f|Y).||/.x1 =||.(f|Y).||.x1 by PARTFUN1:def 6
.=||. (f|Y)/.x1.|| by A13,NORMSP_0:def 3
.=||. f/.x1.|| by A6,PARTFUN2:15
.=||. f.||.x1 by A2,A5,A6,A9,NORMSP_0:def 3
.=||. f.||/.x1 by A2,A5,A6,A9,PARTFUN1:def 6;
hence thesis by A8,A12,A10;
end;
theorem
for f be PartFunc of the carrier of CNS,REAL, Y be Subset of CNS st Y
<>{} & Y c= dom f & Y is compact & f is_continuous_on Y holds ex x1,x2 be Point
of CNS st x1 in Y & x2 in Y & f/.x1 = upper_bound (f.:Y) & f/.x2 = lower_bound
(f.:Y)
proof
let f be PartFunc of the carrier of CNS,REAL;
let Y be Subset of CNS such that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f is_continuous_on Y;
A5: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A2,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A5;
let r be Point of CNS;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 be Point of CNS such that
A6: x1 in dom (f|Y) & x2 in dom (f|Y) and
A7: (f|Y)/.x1 = upper_bound (rng (f|Y)) & (f|Y)/.x2 = lower_bound (rng
(f|Y)) by A1,A3,A5,Th86;
take x1,x2;
thus x1 in Y & x2 in Y by A5,A6;
(f|Y)/.x1 =f/.x1 & (f|Y)/.x2 =f/.x2 by A6,PARTFUN2:15;
hence thesis by A7,RELAT_1:115;
end;
definition
let CNS1,CNS2 be ComplexNormSpace;
let X be set;
let f be PartFunc of CNS1,CNS2;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 0 < r & for
x1,x2 be Point of CNS1 st x1 in X & x2 in X holds ||.f/.x1-f/.x2.||<=r*||.x1-x2
.||;
end;
definition
let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let X be set;
let f be PartFunc of CNS,RNS;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 0 < r & for
x1,x2 be Point of CNS st x1 in X & x2 in X holds ||.f/.x1-f/.x2.||<=r*||.x1-x2
.||;
end;
definition
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let X be set;
let f be PartFunc of RNS,CNS;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 0 < r & for
x1,x2 be Point of RNS st x1 in X & x2 in X holds ||.f/.x1-f/.x2.||<=r*||.x1-x2
.||;
end;
definition
let CNS be ComplexNormSpace;
let X be set;
let f be PartFunc of the carrier of CNS,COMPLEX;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 0<r & for x1,
x2 be Point of CNS st x1 in X & x2 in X holds |.(f/.x1-f/.x2).|<=r*||.x1-x2.||;
end;
definition
let CNS be ComplexNormSpace;
let X be set;
let f be PartFunc of the carrier of CNS,REAL;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 0<r & for x1,
x2 be Point of CNS st x1 in X & x2 in X holds |.f/.x1-f/.x2.|<=r*||.x1-x2.||;
end;
definition
let RNS be RealNormSpace;
let X be set;
let f be PartFunc of the carrier of RNS,COMPLEX;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 0<r & for x1,
x2 be Point of RNS st x1 in X & x2 in X holds |.(f/.x1-f/.x2).|<=r*||.x1-x2.||;
end;
theorem Th97:
for f be PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X & X1
c= X holds f is_Lipschitzian_on X1
proof
let f be PartFunc of CNS1,CNS2;
assume that
A1: f is_Lipschitzian_on X and
A2: X1 c= X;
X c= dom f by A1;
hence X1 c= dom f by A2;
consider s be Real such that
A3: 0<s and
A4: for x1,x2 be Point of CNS1 st x1 in X & x2 in X holds ||. f/.x1-f/.
x2.||<=s*||. x1-x2.|| by A1;
take s;
thus 0<s by A3;
let x1,x2 be Point of CNS1;
assume x1 in X1 & x2 in X1;
hence thesis by A2,A4;
end;
theorem Th98:
for f be PartFunc of CNS,RNS st f is_Lipschitzian_on X & X1 c=
X holds f is_Lipschitzian_on X1
proof
let f be PartFunc of CNS,RNS;
assume that
A1: f is_Lipschitzian_on X and
A2: X1 c= X;
X c= dom f by A1;
hence X1 c= dom f by A2;
consider s be Real such that
A3: 0<s and
A4: for x1,x2 be Point of CNS st x1 in X & x2 in X holds ||. f/.x1-f/.x2
.||<=s*||. x1-x2.|| by A1;
take s;
thus 0<s by A3;
let x1,x2 be Point of CNS;
assume x1 in X1 & x2 in X1;
hence thesis by A2,A4;
end;
theorem Th99:
for f be PartFunc of RNS,CNS st f is_Lipschitzian_on X & X1 c=
X holds f is_Lipschitzian_on X1
proof
let f be PartFunc of RNS,CNS;
assume that
A1: f is_Lipschitzian_on X and
A2: X1 c= X;
X c= dom f by A1;
hence X1 c= dom f by A2;
consider s be Real such that
A3: 0<s and
A4: for x1,x2 be Point of RNS st x1 in X & x2 in X holds ||. f/.x1-f/.x2
.||<=s*||. x1-x2.|| by A1;
take s;
thus 0<s by A3;
let x1,x2 be Point of RNS;
assume x1 in X1 & x2 in X1;
hence thesis by A2,A4;
end;
theorem
for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X & f2
is_Lipschitzian_on X1 holds f1+f2 is_Lipschitzian_on X /\ X1
proof
let f1,f2 be PartFunc of CNS1,CNS2;
assume that
A1: f1 is_Lipschitzian_on X and
A2: f2 is_Lipschitzian_on X1;
A3: f1 is_Lipschitzian_on X /\ X1 by A1,Th97,XBOOLE_1:17;
then consider s be Real such that
A4: 0 < s and
A5: for x1,x2 be Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f1/.x1-f1/.x2.||<=s*||. x1-x2 .||;
A6: f2 is_Lipschitzian_on X /\ X1 by A2,Th97,XBOOLE_1:17;
then
A7: X /\ X1 c= dom f2;
X /\ X1 c= dom f1 by A3;
then X /\ X1 c= dom f1 /\ dom f2 by A7,XBOOLE_1:19;
hence
A8: X /\ X1 c= dom (f1+f2) by VFUNCT_1:def 1;
consider g be Real such that
A9: 0<g and
A10: for x1,x2 be Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f2/.x1-f2/.x2 .||<=g*||. x1-x2 .|| by A6;
take p=s+g;
0+0<s+g by A4,A9;
hence 0<p;
let x1,x2 be Point of CNS1;
assume that
A11: x1 in X/\X1 and
A12: x2 in X/\X1;
A13: ||. f2/.x1-f2/.x2.||<=g*||. x1-x2.|| by A10,A11,A12;
||. f1/.x1-f1/.x2.||<=s*||. x1-x2.|| by A5,A11,A12;
then
A14: ||. f1/.x1-f1/.x2.||+||. f2/.x1-f2/.x2.|| <= s*||. x1-x2.||+g*||. x1-
x2.|| by A13,XREAL_1:7;
||. (f1+f2)/.x1-(f1+f2)/.x2 .|| = ||. f1/.x1 + f2/.x1-(f1+f2)/.x2.|| by A8
,A11,VFUNCT_1:def 1
.= ||. f1/.x1 + f2/.x1 - (f1/.x2+f2/.x2) .|| by A8,A12,VFUNCT_1:def 1
.= ||. f1/.x1 + (f2/.x1 - (f1/.x2+f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 + (f2/.x1 - f1/.x2-f2/.x2).|| by RLVECT_1:27
.= ||. f1/.x1 + (-f1/.x2 + f2/.x1-f2/.x2).|| by RLVECT_1:def 11
.= ||. f1/.x1 + (-f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 +- f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 3
.= ||. f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 11;
then ||. (f1+f2)/.x1-(f1+f2)/.x2.|| <=||. f1/.x1-f1/.x2.||+||. f2/.x1-f2 /.
x2.|| by CLVECT_1:def 13;
hence thesis by A14,XXREAL_0:2;
end;
theorem
for f1,f2 be PartFunc of CNS,RNS st f1 is_Lipschitzian_on X & f2
is_Lipschitzian_on X1 holds f1+f2 is_Lipschitzian_on X /\ X1
proof
let f1,f2 be PartFunc of CNS,RNS;
assume that
A1: f1 is_Lipschitzian_on X and
A2: f2 is_Lipschitzian_on X1;
A3: f1 is_Lipschitzian_on X /\ X1 by A1,Th98,XBOOLE_1:17;
then consider s be Real such that
A4: 0 < s and
A5: for x1,x2 be Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f1/.x1-f1/.x2.||<=s*||. x1-x2 .||;
A6: f2 is_Lipschitzian_on X /\ X1 by A2,Th98,XBOOLE_1:17;
then
A7: X /\ X1 c= dom f2;
X /\ X1 c= dom f1 by A3;
then X /\ X1 c= dom f1 /\ dom f2 by A7,XBOOLE_1:19;
hence
A8: X /\ X1 c= dom (f1+f2) by VFUNCT_1:def 1;
consider g be Real such that
A9: 0<g and
A10: for x1,x2 be Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f2/.x1-f2/.x2 .||<=g*||. x1-x2 .|| by A6;
take p=s+g;
0+0<s+g by A4,A9;
hence 0<p;
let x1,x2 be Point of CNS;
assume that
A11: x1 in X/\X1 and
A12: x2 in X/\X1;
A13: ||. f2/.x1-f2/.x2.||<=g*||. x1-x2.|| by A10,A11,A12;
||. f1/.x1-f1/.x2.||<=s*||. x1-x2.|| by A5,A11,A12;
then
A14: ||. f1/.x1-f1/.x2.||+||. f2/.x1-f2/.x2.|| <= s*||. x1-x2.||+g*||. x1-
x2.|| by A13,XREAL_1:7;
||. (f1+f2)/.x1-(f1+f2)/.x2 .|| = ||. f1/.x1 + f2/.x1-(f1+f2)/.x2.|| by A8
,A11,VFUNCT_1:def 1
.= ||. f1/.x1 + f2/.x1 - (f1/.x2+f2/.x2) .|| by A8,A12,VFUNCT_1:def 1
.= ||. f1/.x1 + (f2/.x1 - (f1/.x2+f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 + (f2/.x1 - f1/.x2-f2/.x2).|| by RLVECT_1:27
.= ||. f1/.x1 + (-f1/.x2 + f2/.x1-f2/.x2).|| by RLVECT_1:def 11
.= ||. f1/.x1 + (-f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 +- f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 3
.= ||. f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 11;
then ||. (f1+f2)/.x1-(f1+f2)/.x2.|| <=||. f1/.x1-f1/.x2.||+||. f2/.x1-f2 /.
x2.|| by NORMSP_1:def 1;
hence thesis by A14,XXREAL_0:2;
end;
theorem
for f1,f2 be PartFunc of RNS,CNS st f1 is_Lipschitzian_on X & f2
is_Lipschitzian_on X1 holds f1+f2 is_Lipschitzian_on X /\ X1
proof
let f1,f2 be PartFunc of RNS,CNS;
assume that
A1: f1 is_Lipschitzian_on X and
A2: f2 is_Lipschitzian_on X1;
A3: f1 is_Lipschitzian_on X /\ X1 by A1,Th99,XBOOLE_1:17;
then consider s be Real such that
A4: 0 < s and
A5: for x1,x2 be Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f1/.x1-f1/.x2.||<=s*||. x1-x2 .||;
A6: f2 is_Lipschitzian_on X /\ X1 by A2,Th99,XBOOLE_1:17;
then
A7: X /\ X1 c= dom f2;
X /\ X1 c= dom f1 by A3;
then X /\ X1 c= dom f1 /\ dom f2 by A7,XBOOLE_1:19;
hence
A8: X /\ X1 c= dom (f1+f2) by VFUNCT_1:def 1;
consider g be Real such that
A9: 0<g and
A10: for x1,x2 be Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f2/.x1-f2/.x2 .||<=g*||. x1-x2 .|| by A6;
take p=s+g;
0+0<s+g by A4,A9;
hence 0<p;
let x1,x2 be Point of RNS;
assume that
A11: x1 in X/\X1 and
A12: x2 in X/\X1;
A13: ||. f2/.x1-f2/.x2.||<=g*||. x1-x2.|| by A10,A11,A12;
||. f1/.x1-f1/.x2.||<=s*||. x1-x2.|| by A5,A11,A12;
then
A14: ||. f1/.x1-f1/.x2.||+||. f2/.x1-f2/.x2.|| <= s*||. x1-x2.||+g*||. x1-
x2.|| by A13,XREAL_1:7;
||. (f1+f2)/.x1-(f1+f2)/.x2 .|| = ||. f1/.x1 + f2/.x1-(f1+f2)/.x2.|| by A8
,A11,VFUNCT_1:def 1
.= ||. f1/.x1 + f2/.x1 - (f1/.x2+f2/.x2) .|| by A8,A12,VFUNCT_1:def 1
.= ||. f1/.x1 + (f2/.x1 - (f1/.x2+f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 + (f2/.x1 - f1/.x2-f2/.x2).|| by RLVECT_1:27
.= ||. f1/.x1 + (-f1/.x2 + f2/.x1-f2/.x2).|| by RLVECT_1:def 11
.= ||. f1/.x1 + (-f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 +- f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 3
.= ||. f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 11;
then ||. (f1+f2)/.x1-(f1+f2)/.x2.|| <=||. f1/.x1-f1/.x2.||+||. f2/.x1-f2 /.
x2.|| by CLVECT_1:def 13;
hence thesis by A14,XXREAL_0:2;
end;
theorem
for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X & f2
is_Lipschitzian_on X1 holds f1-f2 is_Lipschitzian_on X /\ X1
proof
let f1,f2 be PartFunc of CNS1,CNS2;
assume that
A1: f1 is_Lipschitzian_on X and
A2: f2 is_Lipschitzian_on X1;
A3: f1 is_Lipschitzian_on X /\ X1 by A1,Th97,XBOOLE_1:17;
then consider s be Real such that
A4: 0<s and
A5: for x1,x2 be Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f1/.x1-f1/.x2.||<=s*||. x1-x2.||;
A6: f2 is_Lipschitzian_on X /\ X1 by A2,Th97,XBOOLE_1:17;
then
A7: X /\ X1 c= dom f2;
X /\ X1 c= dom f1 by A3;
then X /\ X1 c= dom f1 /\ dom f2 by A7,XBOOLE_1:19;
hence
A8: X /\ X1 c= dom (f1-f2) by VFUNCT_1:def 2;
consider g be Real such that
A9: 0<g and
A10: for x1,x2 be Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f2/.x1-f2/.x2.||<=g*||. x1-x2.|| by A6;
take p=s+g;
0+0<s+g by A4,A9;
hence 0<p;
let x1,x2 be Point of CNS1;
assume that
A11: x1 in X/\X1 and
A12: x2 in X/\X1;
A13: ||. f2/.x1-f2/.x2.||<=g*||. x1-x2.|| by A10,A11,A12;
||. f1/.x1-f1/.x2.||<=s*||. x1-x2.|| by A5,A11,A12;
then
A14: ||. f1/.x1-f1/.x2.||+||. f2/.x1-f2/.x2.||<= s*||. x1-x2.||+g*||. x1-x2
.|| by A13,XREAL_1:7;
||. (f1-f2)/.x1-(f1-f2)/.x2.|| = ||. f1/.x1 - f2/.x1-(f1-f2)/.x2.|| by A8,A11
,VFUNCT_1:def 2
.= ||. f1/.x1 - f2/.x1 - (f1/.x2-f2/.x2).|| by A8,A12,VFUNCT_1:def 2
.= ||. f1/.x1 - (f2/.x1 + (f1/.x2-f2/.x2)).|| by RLVECT_1:27
.= ||. f1/.x1 - (f1/.x2 + f2/.x1-f2/.x2).|| by RLVECT_1:28
.= ||. f1/.x1 - (f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| by RLVECT_1:27;
then ||. (f1-f2)/.x1-(f1-f2)/.x2.|| <=||. f1/.x1-f1/.x2.||+||. f2/.x1-f2 /.
x2.|| by CLVECT_1:104;
hence thesis by A14,XXREAL_0:2;
end;
theorem
for f1,f2 be PartFunc of CNS,RNS st f1 is_Lipschitzian_on X & f2
is_Lipschitzian_on X1 holds f1-f2 is_Lipschitzian_on X /\ X1
proof
let f1,f2 be PartFunc of CNS,RNS;
assume that
A1: f1 is_Lipschitzian_on X and
A2: f2 is_Lipschitzian_on X1;
A3: f1 is_Lipschitzian_on X /\ X1 by A1,Th98,XBOOLE_1:17;
then consider s be Real such that
A4: 0<s and
A5: for x1,x2 be Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f1/.x1-f1/.x2.||<=s*||. x1-x2.||;
A6: f2 is_Lipschitzian_on X /\ X1 by A2,Th98,XBOOLE_1:17;
then
A7: X /\ X1 c= dom f2;
X /\ X1 c= dom f1 by A3;
then X /\ X1 c= dom f1 /\ dom f2 by A7,XBOOLE_1:19;
hence
A8: X /\ X1 c= dom (f1-f2) by VFUNCT_1:def 2;
consider g be Real such that
A9: 0<g and
A10: for x1,x2 be Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f2/.x1-f2/.x2.||<=g*||. x1-x2.|| by A6;
take p=s+g;
0+0<s+g by A4,A9;
hence 0<p;
let x1,x2 be Point of CNS;
assume that
A11: x1 in X/\X1 and
A12: x2 in X/\X1;
A13: ||. f2/.x1-f2/.x2.||<=g*||. x1-x2.|| by A10,A11,A12;
||. f1/.x1-f1/.x2.||<=s*||. x1-x2.|| by A5,A11,A12;
then
A14: ||. f1/.x1-f1/.x2.||+||. f2/.x1-f2/.x2.||<= s*||. x1-x2.||+g*||. x1-x2
.|| by A13,XREAL_1:7;
||. (f1-f2)/.x1-(f1-f2)/.x2.|| = ||. f1/.x1 - f2/.x1-(f1-f2)/.x2.|| by A8,A11
,VFUNCT_1:def 2
.= ||. f1/.x1 - f2/.x1 - (f1/.x2-f2/.x2).|| by A8,A12,VFUNCT_1:def 2
.= ||. f1/.x1 - (f2/.x1 + (f1/.x2-f2/.x2)).|| by RLVECT_1:27
.= ||. f1/.x1 - (f1/.x2 + f2/.x1-f2/.x2).|| by RLVECT_1:28
.= ||. f1/.x1 - (f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| by RLVECT_1:27;
then ||. (f1-f2)/.x1-(f1-f2)/.x2.|| <=||. f1/.x1-f1/.x2.||+||. f2/.x1-f2 /.
x2.|| by NORMSP_1:3;
hence thesis by A14,XXREAL_0:2;
end;
theorem
for f1,f2 be PartFunc of RNS,CNS st f1 is_Lipschitzian_on X & f2
is_Lipschitzian_on X1 holds f1-f2 is_Lipschitzian_on X /\ X1
proof
let f1,f2 be PartFunc of RNS,CNS;
assume that
A1: f1 is_Lipschitzian_on X and
A2: f2 is_Lipschitzian_on X1;
A3: f1 is_Lipschitzian_on X /\ X1 by A1,Th99,XBOOLE_1:17;
then consider s be Real such that
A4: 0<s and
A5: for x1,x2 be Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f1/.x1-f1/.x2.||<=s*||. x1-x2.||;
A6: f2 is_Lipschitzian_on X /\ X1 by A2,Th99,XBOOLE_1:17;
then
A7: X /\ X1 c= dom f2;
X /\ X1 c= dom f1 by A3;
then X /\ X1 c= dom f1 /\ dom f2 by A7,XBOOLE_1:19;
hence
A8: X /\ X1 c= dom (f1-f2) by VFUNCT_1:def 2;
consider g be Real such that
A9: 0<g and
A10: for x1,x2 be Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 holds
||. f2/.x1-f2/.x2.||<=g*||. x1-x2.|| by A6;
take p=s+g;
0+0<s+g by A4,A9;
hence 0<p;
let x1,x2 be Point of RNS;
assume that
A11: x1 in X/\X1 and
A12: x2 in X/\X1;
A13: ||. f2/.x1-f2/.x2.||<=g*||. x1-x2.|| by A10,A11,A12;
||. f1/.x1-f1/.x2.||<=s*||. x1-x2.|| by A5,A11,A12;
then
A14: ||. f1/.x1-f1/.x2.||+||. f2/.x1-f2/.x2.||<= s*||. x1-x2.||+g*||. x1-x2
.|| by A13,XREAL_1:7;
||. (f1-f2)/.x1-(f1-f2)/.x2.|| = ||. f1/.x1 - f2/.x1-(f1-f2)/.x2.|| by A8,A11
,VFUNCT_1:def 2
.= ||. f1/.x1 - f2/.x1 - (f1/.x2-f2/.x2).|| by A8,A12,VFUNCT_1:def 2
.= ||. f1/.x1 - (f2/.x1 + (f1/.x2-f2/.x2)).|| by RLVECT_1:27
.= ||. f1/.x1 - (f1/.x2 + f2/.x1-f2/.x2).|| by RLVECT_1:28
.= ||. f1/.x1 - (f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| by RLVECT_1:27;
then ||. (f1-f2)/.x1-(f1-f2)/.x2.|| <=||. f1/.x1-f1/.x2.||+||. f2/.x1-f2 /.
x2.|| by CLVECT_1:104;
hence thesis by A14,XXREAL_0:2;
end;
theorem Th106:
for f be PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
z(#)f is_Lipschitzian_on X
proof
let f be PartFunc of CNS1,CNS2;
assume
A1: f is_Lipschitzian_on X;
then consider s be Real such that
A2: 0 < s and
A3: for x1,x2 be Point of CNS1 st x1 in X & x2 in X holds ||. f/.x1-f/.
x2.||<=s*||. x1-x2.||;
X c= dom f by A1;
hence
A4: X c= dom (z(#)f) by VFUNCT_2:def 2;
now
per cases;
suppose
A5: z=0;
take s;
thus 0<s by A2;
let x1,x2 be Point of CNS1;
assume that
A6: x1 in X and
A7: x2 in X;
0<=||. x1-x2.|| by CLVECT_1:105;
then
A8: s*0<=s*||. x1-x2.|| by A2;
||. (z(#)f)/.x1-(z(#)f)/.x2.|| = ||. z*(f/.x1)-(z(#)f)/.x2.|| by A4,A6,
VFUNCT_2:def 2
.= ||. 0.CNS2-(z(#)f)/.x2.|| by A5,CLVECT_1:1
.= ||. 0.CNS2 - z*(f/.x2).|| by A4,A7,VFUNCT_2:def 2
.= ||. 0.CNS2-0.CNS2.|| by A5,CLVECT_1:1
.= ||. 0.CNS2.|| by RLVECT_1:13
.= 0 by CLVECT_1:102;
hence ||. (z(#)f)/.x1-(z(#)f)/.x2.|| <=s*||. x1-x2.|| by A8;
end;
suppose
A9: z<>0;
reconsider g = |.z.| *s as Real;
take g;
0<|.z.| by A9,COMPLEX1:47;
then 0*s<|.z.|*s by A2,XREAL_1:68;
hence 0<g;
let x1,x2 be Point of CNS1;
assume that
A10: x1 in X and
A11: x2 in X;
0<=|.z.| by COMPLEX1:46;
then
A12: |.z.|*||. f/.x1-f/.x2.|| <= |.z.|*(s*||. x1-x2.||) by A3,A10,A11,
XREAL_1:64;
||. (z(#)f)/.x1-(z(#)f)/.x2.|| = ||. z*(f/.x1)-(z(#)f)/.x2.|| by A4,A10,
VFUNCT_2:def 2
.= ||. z*(f/.x1) - z*(f/.x2).|| by A4,A11,VFUNCT_2:def 2
.= ||. z*(f/.x1 - f/.x2).|| by CLVECT_1:9
.= |.z.|*||. f/.x1 - f/.x2.|| by CLVECT_1:def 13;
hence ||. (z(#)f)/.x1-(z(#)f)/.x2.|| <= g*||. x1-x2.|| by A12;
end;
end;
hence thesis;
end;
theorem Th107:
for f be PartFunc of CNS,RNS st f is_Lipschitzian_on X holds r
(#)f is_Lipschitzian_on X
proof
let f be PartFunc of CNS,RNS;
assume
A1: f is_Lipschitzian_on X;
then consider s be Real such that
A2: 0 < s and
A3: for x1,x2 be Point of CNS st x1 in X & x2 in X holds ||. f/.x1-f/.x2
.||<=s*||. x1-x2.||;
X c= dom f by A1;
hence
A4: X c= dom (r(#)f) by VFUNCT_1:def 4;
now
per cases;
suppose
A5: r=0;
take s;
thus 0<s by A2;
let x1,x2 be Point of CNS;
assume that
A6: x1 in X and
A7: x2 in X;
0 <= ||. x1-x2.|| by CLVECT_1:105;
then
A8: s*0 <= s*||. x1-x2.|| by A2;
||. (r(#)f)/.x1-(r(#)f)/.x2.|| = ||. r*(f/.x1)-(r(#)f)/.x2.|| by A4,A6,
VFUNCT_1:def 4
.= ||. 0.RNS-(r(#)f)/.x2.|| by A5,RLVECT_1:10
.= ||. 0.RNS - r*(f/.x2).|| by A4,A7,VFUNCT_1:def 4
.= ||. 0.RNS-0.RNS.|| by A5,RLVECT_1:10
.= ||. 0.RNS.|| by RLVECT_1:13
.= 0 by NORMSP_1:1;
hence ||. (r(#)f)/.x1-(r(#)f)/.x2.|| <=s*||. x1-x2.|| by A8;
end;
suppose
A9: r<>0;
reconsider g = |.r.| *s as Real;
take g;
0<|.r.| by A9,COMPLEX1:47;
then 0*s<|.r.|*s by A2,XREAL_1:68;
hence 0<g;
let x1,x2 be Point of CNS;
assume that
A10: x1 in X and
A11: x2 in X;
0<=|.r.| by COMPLEX1:46;
then
A12: |.r.|*||. f/.x1-f/.x2.|| <= |.r.|*(s*||. x1-x2.||) by A3,A10,A11,
XREAL_1:64;
||. (r(#)f)/.x1-(r(#)f)/.x2.|| = ||. r*(f/.x1)-(r(#)f)/.x2.|| by A4,A10,
VFUNCT_1:def 4
.= ||. r*(f/.x1) - r*(f/.x2).|| by A4,A11,VFUNCT_1:def 4
.= ||. r*(f/.x1 - f/.x2).|| by RLVECT_1:34
.= |.r.|*||. f/.x1 - f/.x2.|| by NORMSP_1:def 1;
hence ||. (r(#)f)/.x1-(r(#)f)/.x2.|| <= g*||. x1-x2.|| by A12;
end;
end;
hence thesis;
end;
theorem Th108:
for f be PartFunc of RNS,CNS st f is_Lipschitzian_on X holds z
(#)f is_Lipschitzian_on X
proof
let f be PartFunc of RNS,CNS;
assume
A1: f is_Lipschitzian_on X;
then consider s be Real such that
A2: 0 < s and
A3: for x1,x2 be Point of RNS st x1 in X & x2 in X holds ||. f/.x1-f/.x2
.||<=s*||. x1-x2.||;
X c= dom f by A1;
hence
A4: X c= dom (z(#)f) by VFUNCT_2:def 2;
now
per cases;
suppose
A5: z=0;
take s;
thus 0<s by A2;
let x1,x2 be Point of RNS;
assume that
A6: x1 in X and
A7: x2 in X;
0<=||. x1-x2.|| by NORMSP_1:4;
then
A8: s*0<=s*||. x1-x2.|| by A2;
||. (z(#)f)/.x1-(z(#)f)/.x2.|| = ||. z*(f/.x1)-(z(#)f)/.x2.|| by A4,A6,
VFUNCT_2:def 2
.= ||. 0.CNS-(z(#)f)/.x2.|| by A5,CLVECT_1:1
.= ||. 0.CNS - z*(f/.x2).|| by A4,A7,VFUNCT_2:def 2
.= ||. 0.CNS-0.CNS.|| by A5,CLVECT_1:1
.= ||. 0.CNS.|| by RLVECT_1:13
.= 0 by CLVECT_1:102;
hence ||. (z(#)f)/.x1-(z(#)f)/.x2.|| <=s*||. x1-x2.|| by A8;
end;
suppose
A9: z<>0;
reconsider g = |.z.| *s as Real;
take g;
0<|.z.| by A9,COMPLEX1:47;
then 0*s<|.z.|*s by A2,XREAL_1:68;
hence 0<g;
let x1,x2 be Point of RNS;
assume that
A10: x1 in X and
A11: x2 in X;
0<=|.z.| by COMPLEX1:46;
then
A12: |.z.|*||. f/.x1-f/.x2.|| <= |.z.|*(s*||. x1-x2.||) by A3,A10,A11,
XREAL_1:64;
||. (z(#)f)/.x1-(z(#)f)/.x2.|| = ||. z*(f/.x1)-(z(#)f)/.x2.|| by A4,A10,
VFUNCT_2:def 2
.= ||. z*(f/.x1) - z*(f/.x2).|| by A4,A11,VFUNCT_2:def 2
.= ||. z*(f/.x1 - f/.x2).|| by CLVECT_1:9
.= |.z.|*||. f/.x1 - f/.x2.|| by CLVECT_1:def 13;
hence ||. (z(#)f)/.x1-(z(#)f)/.x2.|| <= g*||. x1-x2.|| by A12;
end;
end;
hence thesis;
end;
theorem
for f be PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds -f
is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X
proof
let f be PartFunc of CNS1,CNS2;
assume
A1: f is_Lipschitzian_on X;
then consider s be Real such that
A2: 0 < s and
A3: for x1,x2 be Point of CNS1 st x1 in X & x2 in X holds ||. f/.x1-f/.
x2.||<=s*||. x1-x2.||;
-f = (-1r)(#)f by VFUNCT_2:23;
hence -f is_Lipschitzian_on X by A1,Th106;
X c= dom f by A1;
hence
A4: X c= dom (||.f.|| ) by NORMSP_0:def 3;
take s;
thus 0<s by A2;
let x1,x2 be Point of CNS1;
assume that
A5: x1 in X and
A6: x2 in X;
|. (||.f.|| )/.x1-(||.f.|| )/.x2 .| = |. (||.f.|| ).x1-(||.f.|| )/.x2
.| by A4,A5,PARTFUN1:def 6
.= |. (||.f.|| ).x1-(||.f.|| ).x2 .| by A4,A6,PARTFUN1:def 6
.= |. ||. f/.x1.||-(||.f.|| ).x2 .| by A4,A5,NORMSP_0:def 3
.= |.||. f/.x1.|| - ||. f/.x2 .||.| by A4,A6,NORMSP_0:def 3;
then
A7: |. (||.f.|| )/.x1-(||.f.|| )/.x2 .| <= ||. f/.x1-f/.x2.|| by CLVECT_1:110;
||. f/.x1-f/.x2 .|| <= s*||. x1-x2.|| by A3,A5,A6;
hence thesis by A7,XXREAL_0:2;
end;
theorem
for f be PartFunc of CNS,RNS st f is_Lipschitzian_on X holds -f
is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X
proof
let f be PartFunc of CNS,RNS;
assume
A1: f is_Lipschitzian_on X;
then consider s be Real such that
A2: 0 < s and
A3: for x1,x2 be Point of CNS st x1 in X & x2 in X holds ||. f/.x1-f/.x2
.||<=s*||. x1-x2.||;
-f = (-1)(#)f by VFUNCT_1:23;
hence -f is_Lipschitzian_on X by A1,Th107;
X c= dom f by A1;
hence
A4: X c= dom (||.f.|| ) by NORMSP_0:def 3;
take s;
thus 0<s by A2;
let x1,x2 be Point of CNS;
assume that
A5: x1 in X and
A6: x2 in X;
|. (||.f.|| )/.x1-(||.f.|| )/.x2 .| = |. (||.f.|| ).x1-(||.f.|| )/.x2
.| by A4,A5,PARTFUN1:def 6
.= |. (||.f.|| ).x1-(||.f.|| ).x2 .| by A4,A6,PARTFUN1:def 6
.= |. ||. f/.x1.||-(||.f.|| ).x2 .| by A4,A5,NORMSP_0:def 3
.= |.||. f/.x1.|| - ||. f/.x2 .||.| by A4,A6,NORMSP_0:def 3;
then
A7: |. (||.f.|| )/.x1-(||.f.|| )/.x2 .| <= ||. f/.x1-f/.x2.|| by NORMSP_1:9;
||. f/.x1-f/.x2 .|| <= s*||. x1-x2.|| by A3,A5,A6;
hence thesis by A7,XXREAL_0:2;
end;
theorem
for f be PartFunc of RNS,CNS st f is_Lipschitzian_on X holds -f
is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X
proof
let f be PartFunc of RNS,CNS;
assume
A1: f is_Lipschitzian_on X;
then consider s be Real such that
A2: 0 < s and
A3: for x1,x2 be Point of RNS st x1 in X & x2 in X holds ||. f/.x1-f/.x2
.||<=s*||. x1-x2.||;
-f = (-1r)(#)f by VFUNCT_2:23;
hence -f is_Lipschitzian_on X by A1,Th108;
X c= dom f by A1;
hence
A4: X c= dom (||.f.|| ) by NORMSP_0:def 3;
take s;
thus 0<s by A2;
let x1,x2 be Point of RNS;
assume that
A5: x1 in X and
A6: x2 in X;
|. (||.f.|| )/.x1-(||.f.|| )/.x2 .| = |. (||.f.|| ).x1-(||.f.|| )/.x2
.| by A4,A5,PARTFUN1:def 6
.= |. (||.f.|| ).x1-(||.f.|| ).x2 .| by A4,A6,PARTFUN1:def 6
.= |. ||. f/.x1.||-(||.f.|| ).x2 .| by A4,A5,NORMSP_0:def 3
.= |.||. f/.x1.|| - ||. f/.x2 .||.| by A4,A6,NORMSP_0:def 3;
then
A7: |. (||.f.|| )/.x1-(||.f.|| )/.x2 .| <= ||. f/.x1-f/.x2.|| by CLVECT_1:110;
||. f/.x1-f/.x2 .|| <= s*||. x1-x2.|| by A3,A5,A6;
hence thesis by A7,XXREAL_0:2;
end;
theorem Th112:
for X be set, f be PartFunc of CNS1,CNS2 st X c= dom f & f|X is
constant holds f is_Lipschitzian_on X
proof
let X be set;
let f be PartFunc of CNS1,CNS2;
assume that
A1: X c= dom f and
A2: f|X is constant;
now
let x1,x2 be Point of CNS1;
assume that
A3: x1 in X and
A4: x2 in X;
A5: x1 in X /\ dom f & x2 in X /\ dom f by A1,A3,A4,XBOOLE_0:def 4;
f/.x1= f.x1 by A1,A3,PARTFUN1:def 6
.= f.x2 by A2,A5,PARTFUN2:58
.= f/.x2 by A1,A4,PARTFUN1:def 6;
then ||. f/.x1-f/.x2.|| = ||. 0.CNS2 .|| by RLVECT_1:15
.= 0 by CLVECT_1:102;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2 .|| by CLVECT_1:105;
end;
hence thesis by A1;
end;
theorem Th113:
for X be set, f be PartFunc of CNS,RNS st X c= dom f & f|X is
constant holds f is_Lipschitzian_on X
proof
let X be set;
let f be PartFunc of CNS,RNS;
assume that
A1: X c= dom f and
A2: f|X is constant;
now
let x1,x2 be Point of CNS;
assume that
A3: x1 in X and
A4: x2 in X;
A5: x1 in X /\ dom f & x2 in X /\ dom f by A1,A3,A4,XBOOLE_0:def 4;
f/.x1= f.x1 by A1,A3,PARTFUN1:def 6
.= f.x2 by A2,A5,PARTFUN2:58
.= f/.x2 by A1,A4,PARTFUN1:def 6;
then ||. f/.x1-f/.x2.|| = ||. 0.RNS .|| by RLVECT_1:15
.= 0 by NORMSP_1:1;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2 .|| by CLVECT_1:105;
end;
hence thesis by A1;
end;
theorem Th114:
for X be set, f be PartFunc of RNS,CNS st X c= dom f & f|X is
constant holds f is_Lipschitzian_on X
proof
let X be set;
let f be PartFunc of RNS,CNS;
assume that
A1: X c= dom f and
A2: f|X is constant;
now
let x1,x2 be Point of RNS;
assume that
A3: x1 in X and
A4: x2 in X;
A5: x1 in X /\ dom f & x2 in X /\ dom f by A1,A3,A4,XBOOLE_0:def 4;
f/.x1= f.x1 by A1,A3,PARTFUN1:def 6
.= f.x2 by A2,A5,PARTFUN2:58
.= f/.x2 by A1,A4,PARTFUN1:def 6;
then ||. f/.x1-f/.x2.|| = ||. 0.CNS .|| by RLVECT_1:15
.= 0 by CLVECT_1:102;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2 .|| by NORMSP_1:4;
end;
hence thesis by A1;
end;
theorem
for Y be Subset of CNS holds id Y is_Lipschitzian_on Y
proof
reconsider r=1 as Real;
let Y be Subset of CNS;
thus Y c= dom(id Y) by RELAT_1:45;
take r;
thus r>0;
let x1,x2 be Point of CNS;
assume that
A1: x1 in Y and
A2: x2 in Y;
||. (id Y)/.x1-(id Y)/.x2 .|| = ||. x1-(id Y)/.x2 .|| by A1,PARTFUN2:6
.= r*||. x1-x2 .|| by A2,PARTFUN2:6;
hence thesis;
end;
theorem Th116:
for f be PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
f is_continuous_on X
proof
let f be PartFunc of CNS1,CNS2;
assume
A1: f is_Lipschitzian_on X;
then consider r be Real such that
A2: 0 < r and
A3: for x1,x2 be Point of CNS1 st x1 in X & x2 in X holds ||. f/.x1-f/.
x2.||<=r*||. x1-x2.||;
A4: X c= dom f by A1;
then
A5: dom (f|X) = X by RELAT_1:62;
now
let x0 be Point of CNS1 such that
A6: x0 in X;
now
let g be Real such that
A7: 0<g;
reconsider s=g/r as Real;
take s9=s;
A8: now
let x1 be Point of CNS1;
assume that
A9: x1 in dom (f|X) and
A10: ||. x1- x0 .|| <s;
r*||. x1- x0 .|| <(g/r)*r by A2,A10,XREAL_1:68;
then
A11: r*||. x1- x0 .|| <g by A2,XCMPLX_1:87;
||. f/.x1- f/.x0 .|| <=r*||. x1- x0 .|| by A3,A5,A6,A9;
then ||. f/.x1- f/.x0 .|| <g by A11,XXREAL_0:2;
then ||. (f|X)/.x1-f/.x0 .||<g by A9,PARTFUN2:15;
hence ||. (f|X)/.x1-(f|X)/.x0 .||<g by A5,A6,PARTFUN2:15;
end;
0<r" & s9=g*r" by A2,XCMPLX_0:def 9;
hence 0<s9 & for x1 be Point of CNS1 st x1 in dom (f|X) & ||. x1- x0 .||
<s9 holds ||. (f|X)/.x1-(f|X)/.x0.||<g by A7,A8,XREAL_1:129;
end;
hence f|X is_continuous_in x0 by A5,A6,Th8;
end;
hence thesis by A4;
end;
theorem Th117:
for f be PartFunc of CNS,RNS st f is_Lipschitzian_on X holds f
is_continuous_on X
proof
let f be PartFunc of CNS,RNS;
assume
A1: f is_Lipschitzian_on X;
then consider r be Real such that
A2: 0 < r and
A3: for x1,x2 be Point of CNS st x1 in X & x2 in X holds ||. f/.x1-f/.x2
.||<=r*||. x1-x2.||;
A4: X c= dom f by A1;
then
A5: dom (f|X) = X by RELAT_1:62;
now
let x0 be Point of CNS such that
A6: x0 in X;
now
let g be Real such that
A7: 0<g;
reconsider s=g/r as Real;
take s9=s;
A8: now
let x1 be Point of CNS;
assume that
A9: x1 in dom (f|X) and
A10: ||. x1- x0 .|| <s;
r*||. x1- x0 .|| <(g/r)*r by A2,A10,XREAL_1:68;
then
A11: r*||. x1- x0 .|| <g by A2,XCMPLX_1:87;
||. f/.x1- f/.x0 .|| <=r*||. x1- x0 .|| by A3,A5,A6,A9;
then ||. f/.x1- f/.x0 .|| <g by A11,XXREAL_0:2;
then ||. (f|X)/.x1-f/.x0 .||<g by A9,PARTFUN2:15;
hence ||. (f|X)/.x1-(f|X)/.x0 .||<g by A5,A6,PARTFUN2:15;
end;
0<r" & s9=g*r" by A2,XCMPLX_0:def 9;
hence
0<s9 & for x1 be Point of CNS st x1 in dom (f|X) & ||. x1- x0 .|| <
s9 holds ||. (f|X)/.x1-(f|X)/.x0.||<g by A7,A8,XREAL_1:129;
end;
hence f|X is_continuous_in x0 by A5,A6,Th9;
end;
hence thesis by A4;
end;
theorem Th118:
for f be PartFunc of RNS,CNS st f is_Lipschitzian_on X holds f
is_continuous_on X
proof
let f be PartFunc of RNS,CNS;
assume
A1: f is_Lipschitzian_on X;
then consider r be Real such that
A2: 0 < r and
A3: for x1,x2 be Point of RNS st x1 in X & x2 in X holds ||. f/.x1-f/.x2
.||<=r*||. x1-x2.||;
A4: X c= dom f by A1;
then
A5: dom (f|X) = X by RELAT_1:62;
now
let x0 be Point of RNS such that
A6: x0 in X;
now
let g be Real such that
A7: 0<g;
reconsider s=g/r as Real;
take s9=s;
A8: now
let x1 be Point of RNS;
assume that
A9: x1 in dom (f|X) and
A10: ||. x1- x0 .|| <s;
r*||. x1- x0 .|| <(g/r)*r by A2,A10,XREAL_1:68;
then
A11: r*||. x1- x0 .|| <g by A2,XCMPLX_1:87;
||. f/.x1- f/.x0 .|| <=r*||. x1- x0 .|| by A3,A5,A6,A9;
then ||. f/.x1- f/.x0 .|| <g by A11,XXREAL_0:2;
then ||. (f|X)/.x1-f/.x0 .||<g by A9,PARTFUN2:15;
hence ||. (f|X)/.x1-(f|X)/.x0 .||<g by A5,A6,PARTFUN2:15;
end;
0<r" & s9=g*r" by A2,XCMPLX_0:def 9;
hence
0<s9 & for x1 be Point of RNS st x1 in dom (f|X) & ||. x1- x0 .|| <
s9 holds ||. (f|X)/.x1-(f|X)/.x0.||<g by A7,A8,XREAL_1:129;
end;
hence f|X is_continuous_in x0 by A5,A6,Th10;
end;
hence thesis by A4;
end;
theorem
for f be PartFunc of the carrier of CNS,COMPLEX st f
is_Lipschitzian_on X holds f is_continuous_on X
proof
let f be PartFunc of the carrier of CNS,COMPLEX;
assume
A1: f is_Lipschitzian_on X;
then consider r be Real such that
A2: 0 < r and
A3: for x1,x2 be Point of CNS st x1 in X & x2 in X holds |.(f/.x1-f/.x2)
.|<=r*||. x1-x2.||;
A4: X c= dom f by A1;
then
A5: dom (f|X) = X by RELAT_1:62;
now
let x0 be Point of CNS such that
A6: x0 in X;
now
let g be Real such that
A7: 0<g;
reconsider s=g/r as Real;
take s9=s;
A8: now
let x1 be Point of CNS;
assume that
A9: x1 in dom (f|X) and
A10: ||. x1- x0 .|| <s;
r*||. x1- x0 .|| <(g/r)*r by A2,A10,XREAL_1:68;
then
A11: r*||. x1- x0 .|| <g by A2,XCMPLX_1:87;
|.( f/.x1- f/.x0 ).| <=r*||. x1- x0 .|| by A3,A5,A6,A9;
then |.( f/.x1- f/.x0 ).| <g by A11,XXREAL_0:2;
then |.( (f|X)/.x1-f/.x0 ).| <g by A9,PARTFUN2:15;
hence |.( (f|X)/.x1-(f|X)/.x0 ).| <g by A5,A6,PARTFUN2:15;
end;
0<r" & s9=g*r" by A2,XCMPLX_0:def 9;
hence
0<s9 & for x1 be Point of CNS st x1 in dom (f|X) & ||. x1- x0 .|| <
s9 holds |.( (f|X)/.x1-(f|X)/.x0).| <g by A7,A8,XREAL_1:129;
end;
hence f|X is_continuous_in x0 by A5,A6,Th12;
end;
hence thesis by A4;
end;
theorem Th120:
for f be PartFunc of the carrier of CNS,REAL st f
is_Lipschitzian_on X holds f is_continuous_on X
proof
let f be PartFunc of the carrier of CNS,REAL;
assume
A1: f is_Lipschitzian_on X;
then consider r be Real such that
A2: 0 < r and
A3: for x1,x2 be Point of CNS st x1 in X & x2 in X holds |.f/.x1-f/.x2
.|<=r*||. x1-x2.||;
A4: X c= dom f by A1;
then
A5: dom (f|X) = X by RELAT_1:62;
now
let x0 be Point of CNS such that
A6: x0 in X;
now
let g be Real such that
A7: 0<g;
reconsider s=g/r as Real;
take s9=s;
A8: now
let x1 be Point of CNS;
assume that
A9: x1 in dom (f|X) and
A10: ||. x1- x0 .|| <s;
r*||. x1- x0 .|| <(g/r)*r by A2,A10,XREAL_1:68;
then
A11: r*||. x1- x0 .|| <g by A2,XCMPLX_1:87;
|. f/.x1- f/.x0 .| <=r*||. x1- x0 .|| by A3,A5,A6,A9;
then |. f/.x1- f/.x0 .| <g by A11,XXREAL_0:2;
then |. (f|X)/.x1-f/.x0 .| <g by A9,PARTFUN2:15;
hence |. (f|X)/.x1-(f|X)/.x0 .| <g by A5,A6,PARTFUN2:15;
end;
0<r" & s9=g*r" by A2,XCMPLX_0:def 9;
hence
0<s9 & for x1 be Point of CNS st x1 in dom (f|X) & ||. x1- x0 .|| <
s9 holds |. (f|X)/.x1-(f|X)/.x0.| <g by A7,A8,XREAL_1:129;
end;
hence f|X is_continuous_in x0 by A5,A6,Th11;
end;
hence thesis by A4;
end;
theorem
for f be PartFunc of the carrier of RNS,COMPLEX st f
is_Lipschitzian_on X holds f is_continuous_on X
proof
let f be PartFunc of the carrier of RNS,COMPLEX;
assume
A1: f is_Lipschitzian_on X;
then consider r be Real such that
A2: 0 < r and
A3: for x1,x2 be Point of RNS st x1 in X & x2 in X holds |.(f/.x1-f/.x2)
.|<=r*||. x1-x2.||;
A4: X c= dom f by A1;
then
A5: dom (f|X) = X by RELAT_1:62;
now
let x0 be Point of RNS such that
A6: x0 in X;
now
let g be Real such that
A7: 0<g;
reconsider s=g/r as Real;
take s9=s;
A8: now
let x1 be Point of RNS;
assume that
A9: x1 in dom (f|X) and
A10: ||. x1- x0 .|| <s;
r*||. x1- x0 .|| <(g/r)*r by A2,A10,XREAL_1:68;
then
A11: r*||. x1- x0 .|| <g by A2,XCMPLX_1:87;
|.( f/.x1- f/.x0 ).| <=r*||. x1- x0 .|| by A3,A5,A6,A9;
then |.( f/.x1- f/.x0 ).| <g by A11,XXREAL_0:2;
then |.( (f|X)/.x1-f/.x0 ).| <g by A9,PARTFUN2:15;
hence |.( (f|X)/.x1-(f|X)/.x0 ).| <g by A5,A6,PARTFUN2:15;
end;
0<r" & s9=g*r" by A2,XCMPLX_0:def 9;
hence
0<s9 & for x1 be Point of RNS st x1 in dom (f|X) & ||. x1- x0 .|| <
s9 holds |.( (f|X)/.x1-(f|X)/.x0).| <g by A7,A8,XREAL_1:129;
end;
hence f|X is_continuous_in x0 by A5,A6,Th13;
end;
hence thesis by A4;
end;
theorem
for f be PartFunc of CNS1,CNS2 st (ex r be Point of CNS2 st rng f = {r
}) holds f is_continuous_on dom f
proof
let f be PartFunc of CNS1,CNS2;
given r be Point of CNS2 such that
A1: rng f = {r};
now
let x1,x2 be Point of CNS1;
assume that
A2: x1 in dom f and
A3: x2 in dom f;
f.x2 in rng f by A3,FUNCT_1:def 3;
then f/.x2 in rng f by A3,PARTFUN1:def 6;
then
A4: f/.x2=r by A1,TARSKI:def 1;
f.x1 in rng f by A2,FUNCT_1:def 3;
then f/.x1 in rng f by A2,PARTFUN1:def 6;
then f/.x1=r by A1,TARSKI:def 1;
then ||. f/.x1-f/.x2.|| = ||. 0.CNS2 .|| by A4,RLVECT_1:15
.= 0 by CLVECT_1:102;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2.|| by CLVECT_1:105;
end;
then f is_Lipschitzian_on dom f;
hence thesis by Th116;
end;
theorem
for f be PartFunc of CNS,RNS st (ex r be Point of RNS st rng f = {r})
holds f is_continuous_on (dom f)
proof
let f be PartFunc of CNS,RNS;
given r be Point of RNS such that
A1: rng f = {r};
now
let x1,x2 be Point of CNS;
assume that
A2: x1 in dom f and
A3: x2 in dom f;
f.x2 in rng f by A3,FUNCT_1:def 3;
then f/.x2 in rng f by A3,PARTFUN1:def 6;
then
A4: f/.x2=r by A1,TARSKI:def 1;
f.x1 in rng f by A2,FUNCT_1:def 3;
then f/.x1 in rng f by A2,PARTFUN1:def 6;
then f/.x1=r by A1,TARSKI:def 1;
then ||. f/.x1-f/.x2.|| = ||. 0.RNS .|| by A4,RLVECT_1:15
.= 0 by NORMSP_1:1;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2.|| by CLVECT_1:105;
end;
then f is_Lipschitzian_on dom f;
hence thesis by Th117;
end;
theorem
for f be PartFunc of RNS,CNS st (ex r be Point of CNS st rng f = {r})
holds f is_continuous_on (dom f)
proof
let f be PartFunc of RNS,CNS;
given r be Point of CNS such that
A1: rng f = {r};
now
let x1,x2 be Point of RNS;
assume that
A2: x1 in dom f and
A3: x2 in dom f;
f.x2 in rng f by A3,FUNCT_1:def 3;
then f/.x2 in rng f by A3,PARTFUN1:def 6;
then
A4: f/.x2=r by A1,TARSKI:def 1;
f.x1 in rng f by A2,FUNCT_1:def 3;
then f/.x1 in rng f by A2,PARTFUN1:def 6;
then f/.x1=r by A1,TARSKI:def 1;
then ||. f/.x1-f/.x2.|| = ||. 0.CNS .|| by A4,RLVECT_1:15
.= 0 by CLVECT_1:102;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2.|| by NORMSP_1:4;
end;
then f is_Lipschitzian_on dom f;
hence thesis by Th118;
end;
theorem
for f be PartFunc of CNS1,CNS2 st X c= dom f & f|X is constant holds f
is_continuous_on X by Th112,Th116;
theorem
for f be PartFunc of CNS,RNS st X c= dom f & f|X is constant holds f
is_continuous_on X by Th113,Th117;
theorem
for f be PartFunc of RNS,CNS st X c= dom f & f|X is constant holds f
is_continuous_on X by Th114,Th118;
theorem Th128:
for f be PartFunc of CNS,CNS st (for x0 be Point of CNS st x0
in dom f holds f/.x0 = x0) holds f is_continuous_on dom f
proof
let f be PartFunc of CNS,CNS such that
A1: for x0 be Point of CNS st x0 in dom f holds f/.x0 = x0;
now
let x1,x2 be Point of CNS;
assume that
A2: x1 in dom f and
A3: x2 in dom f;
f/.x1 = x1 by A1,A2;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2.|| by A1,A3;
end;
then f is_Lipschitzian_on dom f;
hence thesis by Th116;
end;
theorem
for f be PartFunc of CNS,CNS st f = id dom f holds f is_continuous_on dom f
proof
let f be PartFunc of CNS,CNS;
assume
A1: f = id dom f;
now
let x0 be Point of CNS such that
A2: x0 in dom f;
thus f/.x0=f.x0 by A2,PARTFUN1:def 6
.= x0 by A1,A2,FUNCT_1:17;
end;
hence thesis by Th128;
end;
theorem
for f be PartFunc of CNS,CNS, Y be Subset of CNS st Y c= dom f & f|Y =
id Y holds f is_continuous_on Y
proof
let f be PartFunc of CNS,CNS;
let Y be Subset of CNS;
assume that
A1: Y c= dom f and
A2: f|Y = id Y;
now
let x1,x2 be Point of CNS;
assume that
A3: x1 in Y and
A4: x2 in Y;
x1 in dom f /\ Y by A1,A3,XBOOLE_0:def 4;
then
A5: x1 in dom (f|Y) by RELAT_1:61;
(f|Y).x1 = x1 by A2,A3,FUNCT_1:17;
then f.x1 = x1 by A5,FUNCT_1:47;
then
A6: f/.x1 = x1 by A1,A3,PARTFUN1:def 6;
x2 in dom f /\ Y by A1,A4,XBOOLE_0:def 4;
then
A7: x2 in dom (f|Y) by RELAT_1:61;
(f|Y).x2 = x2 by A2,A4,FUNCT_1:17;
then f.x2 = x2 by A7,FUNCT_1:47;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2.|| by A1,A4,A6,PARTFUN1:def 6;
end;
then f is_Lipschitzian_on Y by A1;
hence thesis by Th116;
end;
theorem
for f be PartFunc of CNS,CNS, z be Complex, p be Point of CNS st X c=
dom f & (for x0 be Point of CNS st x0 in X holds f/.x0 = z*x0+p) holds f
is_continuous_on X
proof
let f be PartFunc of CNS,CNS;
let z be Complex;
let p be Point of CNS;
assume that
A1: X c= dom f and
A2: for x0 be Point of CNS st x0 in X holds f/.x0 = z*x0+p;
now
0 + 0 < |.z.| + 1 by COMPLEX1:46,XREAL_1:8;
hence 0 < |.z.|+1;
let x1,x2 be Point of CNS;
assume x1 in X & x2 in X;
then f/.x1 = z*x1+p & f/.x2 = z*x2+p by A2;
then
A3: ||. f/.x1-f/.x2.|| = ||. z*x1+(p-(p+z*x2)).|| by RLVECT_1:28
.= ||. z*x1+(p-p-z*x2).|| by RLVECT_1:27
.= ||. z*x1+(0.CNS-z*x2).|| by RLVECT_1:15
.= ||. z*x1+-z*x2.|| by RLVECT_1:14
.= ||. z*x1-z*x2.|| by RLVECT_1:def 11
.= ||. z*(x1-x2).|| by CLVECT_1:9
.= |.z.|*||. x1-x2.|| by CLVECT_1:def 13;
0<=||. x1-x2.|| by CLVECT_1:105;
then ||. f/.x1-f/.x2.|| + 0 <= |.z.|*||. x1-x2.|| + 1*||. x1-x2.|| by A3,
XREAL_1:7;
hence ||. f/.x1-f/.x2.|| <= (|.z.|+1)*||. x1-x2.||;
end;
then f is_Lipschitzian_on X by A1;
hence thesis by Th116;
end;
theorem Th132:
for f be PartFunc of the carrier of CNS,REAL st (for x0 be
Point of CNS st x0 in dom f holds f/.x0 = ||. x0.|| ) holds f is_continuous_on
dom f
proof
let f be PartFunc of the carrier of CNS,REAL;
assume
A1: for x0 be Point of CNS st x0 in dom f holds f/.x0 = ||. x0 .||;
now
let x1,x2 be Point of CNS;
||. x2 .|| - ||. x1 .|| <= ||.x2 - x1.|| by CLVECT_1:109;
then ||. x2 .|| - ||. x1 .|| <= ||.x1 - x2.|| by CLVECT_1:108;
then
A2: ||. x1 .|| - ||. x2 .|| <= ||.x1 - x2.|| & -(-(||. x1 .|| - ||. x2 .||
)) >= - (||.x1 - x2.||) by CLVECT_1:109,XREAL_1:24;
assume x1 in dom f & x2 in dom f;
then f/.x1 = ||. x1 .|| & f/.x2 = ||. x2 .|| by A1;
hence |.f/.x1 - f/.x2.| <= 1*||. x1 - x2 .|| by A2,ABSVALUE:5;
end;
then f is_Lipschitzian_on dom f;
hence thesis by Th120;
end;
theorem
for f be PartFunc of the carrier of CNS,REAL st X c= dom f & (for x0
be Point of CNS st x0 in X holds f/.x0 = ||. x0.||) holds f is_continuous_on X
proof
let f be PartFunc of the carrier of CNS,REAL;
assume that
A1: X c= dom f and
A2: for x0 be Point of CNS st x0 in X holds f/.x0 = ||. x0 .||;
X=dom f /\ X by A1,XBOOLE_1:28;
then
A3: X=dom(f|X) by RELAT_1:61;
now
let x0 be Point of CNS;
assume
A4: x0 in dom(f|X);
hence (f|X)/.x0=f/.x0 by PARTFUN2:15
.=||. x0 .|| by A2,A3,A4;
end;
then f|X is_continuous_on X by A3,Th132;
hence thesis by Th54;
end;