:: Real Function Continuity
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-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, SEQ_1, PARTFUN1, RELAT_1, TARSKI, SEQ_2,
ORDINAL2, FUNCT_2, FUNCT_1, XBOOLE_0, XXREAL_0, NAT_1, ARYTM_3, CARD_1,
COMPLEX1, ARYTM_1, REAL_1, RCOMP_1, XXREAL_1, VALUED_1, ORDINAL4,
ZFMISC_1, VALUED_0, SEQ_4, XXREAL_2, SQUARE_1, SEQM_3, FCONT_1, JGRAPH_2,
FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, ZFMISC_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4,
SQUARE_1, PARTFUN2, RFUNCT_1, RCOMP_1, RECDEF_1, RFUNCT_2;
constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1, SEQ_2,
SEQM_3, SEQ_4, RCOMP_1, PARTFUN2, RFUNCT_1, RFUNCT_2, RECDEF_1, RELSET_1,
COMSEQ_2, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1,
RFUNCT_2, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, RELAT_1, RFUNCT_1,
SEQ_2, FUNCT_1, ZFMISC_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1;
equalities XBOOLE_0, SQUARE_1, RELAT_1, VALUED_1;
expansions TARSKI, FUNCT_1;
theorems TARSKI, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, ABSVALUE, SEQ_1, SEQ_2,
SEQM_3, SEQ_4, PARTFUN1, XREAL_0, PARTFUN2, RFUNCT_1, RFUNCT_2, RCOMP_1,
RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1,
COMPLEX1, XXREAL_0, ORDINAL1, VALUED_1, XXREAL_1, MEMBERED, XXREAL_2,
VALUED_0, NUMBERS;
schemes NAT_1, RECDEF_1, FUNCT_2;
begin
reserve n,m,k for Element of NAT;
reserve x, X,X1,Z,Z1 for set;
reserve s,g,r,p,x0,x1,x2 for Real;
reserve s1,s2,q1 for Real_Sequence;
reserve Y for Subset of REAL;
reserve f,f1,f2 for PartFunc of REAL,REAL;
definition
let f,x0;
pred f is_continuous_in x0 means
for s1 st rng s1 c= dom f & s1 is
convergent & lim s1 = x0 holds f/*s1 is convergent & f.x0 = lim (f/*s1);
end;
theorem Th1:
x0 in X & f is_continuous_in x0 implies f|X is_continuous_in x0
proof
assume that
A1: x0 in X and
A2: f is_continuous_in x0;
let s1 such that
A3: rng s1 c= dom(f|X) and
A4: s1 is convergent & lim s1 = x0;
dom(f|X) = X /\ dom f by RELAT_1:61;
then
A5: rng s1 c= dom f by A3,XBOOLE_1:18;
A6: (f|X)/*s1 = f/*s1 by A3,FUNCT_2:117;
hence (f|X)/*s1 is convergent by A2,A4,A5;
thus (f|X).x0 = f.x0 by A1,FUNCT_1:49
.= lim ((f|X)/*s1) by A2,A4,A5,A6;
end;
theorem
f is_continuous_in x0 iff for s1 st rng s1 c= dom f & s1 is convergent
& lim s1=x0 & (for n being Nat holds s1.n<>x0)
holds f/*s1 is convergent & f.x0=lim(f/*s1)
proof
thus f is_continuous_in x0 implies for s1 st rng s1 c= dom f & s1 is
convergent & lim s1=x0 &
(for n being Nat holds s1.n<>x0) holds f/*s1 is convergent & f.
x0=lim(f/*s1);
assume
A1: for s1 st rng s1 c=dom f & s1 is convergent & lim s1=x0 &
(for n being Nat holds s1.n<>x0) holds f/*s1 is convergent &
f.x0=lim(f/*s1);
let s2 such that
A2: rng s2 c=dom f and
A3: s2 is convergent & lim s2=x0;
now
per cases;
suppose
ex n st for m st n<=m holds s2.m=x0;
then consider N be Element of NAT such that
A4: for m st N<=m holds s2.m=x0;
A5: for n holds (s2^\N).n=x0
proof
let n;
s2.(n+N)=x0 by A4,NAT_1:12;
hence thesis by NAT_1:def 3;
end;
A6: f/*(s2^\N)=(f/*s2)^\N by A2,VALUED_0:27;
A7: rng (s2^\N) c= rng s2 by VALUED_0:21;
A8: now
let p be Real such that
A9: p>0;
reconsider zz=0 as Nat;
take n=zz;
let m be Nat such that
n<=m;
A10: m in NAT by ORDINAL1:def 12;
then |.(f/*(s2^\N)).m-f.x0.|=|.f.((s2^\N).m)-f.x0.|
by A2,A7,FUNCT_2:108,XBOOLE_1:1
.=|.f.x0-f.x0.| by A5,A10
.=0 by ABSVALUE:2;
hence |.(f/*(s2^\N)).m-f.x0.|<p by A9;
end;
then
A11: f/*(s2^\N) is convergent by SEQ_2:def 6;
then f.x0=lim((f/*s2)^\N) by A8,A6,SEQ_2:def 7;
hence thesis by A11,A6,SEQ_4:20,21;
end;
suppose
A12: for n ex m st n<=m & s2.m<>x0;
defpred P[Nat,set,set] means for n,m st $2=n & $3=m holds n<m
& s2.m<>x0 & for k st n<k & s2.k<>x0 holds m<=k;
defpred P1[set] means s2.$1<>x0;
ex m1 be Element of NAT st 0<=m1 & s2.m1<>x0 by A12;
then
A13: ex m be Nat st P1[m];
consider M be Nat such that
A14: P1[M] & for n be Nat st P1[n] holds M<=n from NAT_1:sch 5(A13);
reconsider M9 = M as Element of NAT by ORDINAL1:def 12;
A15: now
let n;
consider m such that
A16: n+1<=m & s2.m<>x0 by A12;
take m;
thus n<m & s2.m<>x0 by A16,NAT_1:13;
end;
A17: for n being Nat
for x be Element of NAT ex y be Element of NAT st P[n,x,y]
proof
let n be Nat;
let x be Element of NAT;
defpred P2[Nat] means x<$1 & s2.$1<>x0;
ex m st P2[m] by A15;
then
A18: ex m be Nat st P2[m];
consider l be Nat such that
A19: P2[l] & for k be Nat st P2[k] holds l<=k from NAT_1:sch 5(A18);
take l;
l in NAT by ORDINAL1:def 12;
hence thesis by A19;
end;
consider F be sequence of NAT such that
A20: F.0=M9 & for n be Nat holds P[n,F.n,F.(n+1)] from
RECDEF_1:sch 2(A17);
A21: rng F c= REAL by NUMBERS:19;
A22: rng F c= NAT;
A23: dom F=NAT by FUNCT_2:def 1;
then reconsider F as Real_Sequence by A21,RELSET_1:4;
A24: now
let n;
F.n in rng F by A23,FUNCT_1:def 3;
hence F.n is Element of NAT by A22;
end;
now
let n be Nat;
n in NAT by ORDINAL1:def 12;
then F.n is Element of NAT & F.(n+1) is Element of NAT by A24;
hence F.n<F.(n+1) by A20;
end;
then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A25: s2*F is convergent & lim (s2*F)=x0 by A3,SEQ_4:16,17;
A26: for n st s2.n<>x0 ex m st F.m=n
proof
defpred P3[set] means s2.$1<>x0 & for m holds F.m<>$1;
assume ex n st P3[n];
then
A27: ex n be Nat st P3[n];
consider M1 be Nat such that
A28: P3[M1] & for n be Nat st P3[n] holds M1<=n from NAT_1:sch 5(A27
);
defpred P4[Nat] means $1<M1 & s2.$1<>x0 & ex m st F.m=$1;
A29: ex n being Nat st P4[n]
proof
take M;
M<=M1 & M <> M1 by A14,A20,A28;
hence M<M1 by XXREAL_0:1;
thus s2.M<>x0 by A14;
take 0;
thus thesis by A20;
end;
A30: for n being Nat st P4[n] holds n<=M1;
consider MX be Nat such that
A31: P4[MX] & for n being Nat st P4[n] holds n<=MX from NAT_1:sch 6(
A30,A29);
A32: for k st MX<k & k<M1 holds s2.k=x0
proof
given k such that
A33: MX<k and
A34: k<M1 & s2.k<>x0;
now
per cases;
suppose
ex m st F.m=k;
hence contradiction by A31,A33,A34;
end;
suppose
for m holds F.m<>k;
hence contradiction by A28,A34;
end;
end;
hence contradiction;
end;
consider m such that
A35: F.m=MX by A31;
A36: MX<F.(m+1) & s2.(F.(m+1))<>x0 by A20,A35;
M1 in NAT by ORDINAL1:def 12;
then
A37: F.(m+1)<=M1 by A20,A28,A31,A35;
now
assume F.(m+1)<>M1;
then F.(m+1)<M1 by A37,XXREAL_0:1;
hence contradiction by A32,A36;
end;
hence contradiction by A28;
end;
A38: for n being Nat holds (s2*F).n<>x0
proof
defpred P4[Nat] means (s2*F).$1<>x0;
A39: for k being Nat st P4[k] holds P4[k+1]
proof
let k be Nat such that
(s2*F).k<>x0;
reconsider k as Element of NAT by ORDINAL1:def 12;
P[k,F.k,F.(k+1)] by A20;
then s2.(F.(k+1))<>x0;
hence thesis by FUNCT_2:15;
end;
A40: P4[0] by A14,A20,FUNCT_2:15;
thus for n being Nat holds P4[n] from NAT_1:sch 2(A40,A39);
end;
A41: rng (s2*F) c= rng s2 by VALUED_0:21;
then rng (s2*F) c= dom f by A2;
then
A42: f/*(s2*F) is convergent & f.x0=lim(f/*(s2*F)) by A1,A38,A25;
A43: now
let p be Real;
assume
A44: 0<p;
then consider n being Nat such that
A45: for m being Nat st n<=m holds |.(f/*(s2*F)).m-f.x0.|<p
by A42,SEQ_2:def 7;
reconsider k=F.n as Nat;
take k;
let m be Nat such that
A46: k<=m;
A47: m in NAT by ORDINAL1:def 12;
now
per cases;
suppose
s2.m=x0;
then |.(f/*s2).m-f.x0.|= |.f.x0-f.x0.| by A2,FUNCT_2:108,A47
.=0 by ABSVALUE:2;
hence |.(f/*s2).m-f.x0.|<p by A44;
end;
suppose
s2.m<>x0;
then consider l be Element of NAT such that
A48: m=F.l by A26,A47;
n<=l by A46,A48,SEQM_3:1;
then |.(f/*(s2*F)).l-f.x0.|<p by A45;
then |.f.((s2*F).l)-f.x0.|<p by A2,A41,FUNCT_2:108,XBOOLE_1:1;
then |.f.(s2.m)-f.x0.|<p by A48,FUNCT_2:15;
hence |.(f/*s2).m-f.x0.|<p by A2,FUNCT_2:108,A47;
end;
end;
hence |.(f/*s2).m-f.x0.|<p;
end;
hence f/*s2 is convergent by SEQ_2:def 6;
hence f.x0=lim(f/*s2) by A43,SEQ_2:def 7;
end;
end;
hence thesis;
end;
theorem Th3:
f is_continuous_in x0 iff for r st 0<r ex s st 0<s & for x1 st x1
in dom f & |.x1-x0.|<s holds |.f.x1-f.x0.|<r
proof
thus f is_continuous_in x0 implies for r st 0<r ex s st 0<s & for x1 st x1
in dom f & |.x1-x0.|<s holds |.f.x1-f.x0.|<r
proof
assume
A1: f is_continuous_in x0;
given r such that
A2: 0<r and
A3: for s holds not 0<s or ex x1 st x1 in dom f & |.x1-x0.|<s & not
|.f.x1-f.x0.|<r;
defpred P[Element of NAT,Real] means $2 in dom f & |.$2-x0.| < 1/(
$1+1) & not |.f.$2-f.x0.|<r;
A4: for n ex p being Element of REAL st P[n,p]
proof
let n;
0<(n+1)";
then 0<1/(n+1) by XCMPLX_1:215;
then consider p 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 such that
A6: for n holds P[n,s1.n] from FUNCT_2:sch 3(A4);
A7: rng s1 c= dom f
proof
let x be object;
assume x in rng s1;
then ex n st x=s1.n by FUNCT_2:113;
hence thesis by A6;
end;
A8: now
let n be Nat;
A9: n in NAT by ORDINAL1:def 12;
not |.f.(s1.n)-f.x0.|<r by A6,A9;
hence not |.(f/*s1).n-f.x0.|<r by A7,FUNCT_2:108,A9;
end;
A10: now
let s be Real;
assume
A11: 0<s;
consider n being Nat such that
A12: s"<n by SEQ_4:3;
s"+(0 qua Nat) <n+1 by A12,XREAL_1:8;
then 1/(n+1)<1/s" by A11,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 SEQ_2:def 6;
then lim s1=x0 by A10,SEQ_2: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,SEQ_2:def 7;
|.(f/*s1).n-f.x0.|<r by A16;
hence contradiction by A8;
end;
assume
A17: for r st 0<r ex s st 0<s & for x1 st x1 in dom f & |.x1-x0.|<s
holds |.f.x1-f.x0.|<r;
now
let s1 such that
A18: rng s1 c= dom f and
A19: s1 is convergent & lim s1 = x0;
A20: now
let p be Real;
assume 0<p;
then consider s such that
A21: 0<s and
A22: for x1 st x1 in dom f & |.x1-x0.|<s holds |.f.x1-f.x0.|<p by A17;
consider n being Nat such that
A23: for m being Nat st n<=m holds |.s1.m-x0.|<s
by A19,A21,SEQ_2:def 7;
take k=n;
let m be Nat;
A24: m in NAT by ORDINAL1:def 12;
assume k<=m;
then s1.m in rng s1 & |.s1.m-x0.|<s by A23,VALUED_0:28;
then |.f.(s1.m)-f.x0.|<p by A18,A22;
hence |.(f/*s1).m - f.x0.|<p by A18,FUNCT_2:108,A24;
end;
then f/*s1 is convergent by SEQ_2:def 6;
hence f/*s1 is convergent & f.x0 = lim (f/*s1) by A20,SEQ_2:def 7;
end;
hence thesis;
end;
theorem Th4:
for f,x0 holds f is_continuous_in x0 iff for N1 being
Neighbourhood of f.x0 ex N being Neighbourhood of x0 st for x1 st x1 in dom f &
x1 in N holds f.x1 in N1
proof
let f,x0;
thus f is_continuous_in x0 implies for N1 being Neighbourhood of f.x0 ex N
being Neighbourhood of x0 st for x1 st x1 in dom f & x1 in N holds f.x1 in N1
proof
assume
A1: f is_continuous_in x0;
let N1 be Neighbourhood of f.x0;
consider r such that
A2: 0<r and
A3: N1 = ].f.x0-r,f.x0+r.[ by RCOMP_1:def 6;
consider s such that
A4: 0<s and
A5: for x1 st x1 in dom f & |.x1-x0.|<s holds |.f.x1-f.x0.|<r by A1,A2,Th3;
reconsider N=].x0-s,x0+s.[ as Neighbourhood of x0 by A4,RCOMP_1:def 6;
take N;
let x1;
assume that
A6: x1 in dom f and
A7: x1 in N;
|.x1-x0.|<s by A7,RCOMP_1:1;
then |.f.x1-f.x0.|<r by A5,A6;
hence thesis by A3,RCOMP_1:1;
end;
assume
A8: for N1 being Neighbourhood of f.x0 ex N being Neighbourhood of x0
st for x1 st x1 in dom f & x1 in N holds f.x1 in N1;
now
let r;
assume 0<r;
then reconsider N1 = ].f.x0-r,f.x0+r.[ as Neighbourhood of f.x0 by
RCOMP_1:def 6;
consider N2 being Neighbourhood of x0 such that
A9: for x1 st x1 in dom f & x1 in N2 holds f.x1 in N1 by A8;
consider s such that
A10: 0<s and
A11: N2 = ].x0-s,x0+s.[ by RCOMP_1:def 6;
take s;
for x1 st x1 in dom f & |.x1-x0.|<s holds |.f.x1-f.x0.|<r
proof
let x1;
assume that
A12: x1 in dom f and
A13: |.x1-x0.|<s;
x1 in N2 by A11,A13,RCOMP_1:1;
then f.x1 in N1 by A9,A12;
hence thesis by RCOMP_1:1;
end;
hence 0<s & for x1 st x1 in dom f & |.x1-x0.|<s holds |.f.x1-f.x0.|<r by
A10;
end;
hence thesis by Th3;
end;
theorem Th5:
for f,x0 holds f is_continuous_in x0 iff for N1 being
Neighbourhood of f.x0 ex N being Neighbourhood of x0 st f.:N c= N1
proof
let f,x0;
thus f is_continuous_in x0 implies 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;
let N1 be Neighbourhood of f.x0;
consider N being Neighbourhood of x0 such that
A2: for x1 st x1 in dom f & x1 in N holds f.x1 in N1 by A1,Th4;
take N;
now
let r;
assume r in f.:N;
then ex x be Element of REAL st x in dom f & x in N & r=f.x by
PARTFUN2:59;
hence r in N1 by A2;
end;
hence thesis;
end;
assume
A3: 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
A4: f.:N c= N1 by A3;
take N;
let x1;
assume x1 in dom f & x1 in N;
then f.x1 in f.:N by FUNCT_1:def 6;
hence f.x1 in N1 by A4;
end;
hence thesis by Th4;
end;
theorem
(ex N be Neighbourhood of x0 st dom f /\ N = {x0}) implies f
is_continuous_in x0
proof
given N be Neighbourhood of x0 such that
A1: dom f /\ N = {x0};
x0 in dom f /\ N by A1,TARSKI:def 1;
then
A2: x0 in dom f by XBOOLE_0:def 4;
now
let N1 be Neighbourhood of f.x0;
take N;
A3: f.x0 in N1 by RCOMP_1:16;
f.:N = Im(f,x0) by A1,RELAT_1:112
.= {f.x0} by A2,FUNCT_1:59;
hence f.:N c= N1 by A3,ZFMISC_1:31;
end;
hence thesis by Th5;
end;
theorem Th7:
x0 in dom f1 /\ dom f2 & f1 is_continuous_in x0 & f2
is_continuous_in x0 implies f1+f2 is_continuous_in x0 & f1-f2 is_continuous_in
x0 & f1(#)f2 is_continuous_in x0
proof
assume
A1: x0 in dom f1 /\ dom f2;
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in x0;
now
let s1;
assume that
A4: rng s1 c= dom(f1+f2) and
A5: s1 is convergent & lim s1=x0;
A6: rng s1 c= dom f1 /\ dom f2 by A4,VALUED_1:def 1;
dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;
then dom (f1+f2) c= dom f2 by XBOOLE_1:17;
then
A7: rng s1 c= dom f2 by A4;
then
A8: f2/*s1 is convergent by A3,A5;
dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;
then dom (f1+f2) c= dom f1 by XBOOLE_1:17;
then
A9: rng s1 c= dom f1 by A4;
then
A10: f1/*s1 is convergent by A2,A5;
then f1/*s1+f2/*s1 is convergent by A8;
hence (f1+f2)/*s1 is convergent by A6,RFUNCT_2:8;
A11: f1.x0 = lim (f1/*s1) by A2,A5,A9;
A12: f2.x0 = lim (f2/*s1) by A3,A5,A7;
x0 in dom (f1+f2) by A1,VALUED_1:def 1;
hence (f1+f2).x0 = f1.x0 + f2.x0 by VALUED_1:def 1
.= lim (f1/*s1 + f2/*s1) by A10,A11,A8,A12,SEQ_2:6
.= lim ((f1+f2)/*s1) by A6,RFUNCT_2:8;
end;
hence f1+f2 is_continuous_in x0;
now
let s1;
assume that
A13: rng s1 c= dom(f1-f2) and
A14: s1 is convergent & lim s1=x0;
A15: rng s1 c= dom f1 /\ dom f2 by A13,VALUED_1:12;
dom (f1-f2) = dom f1 /\ dom f2 by VALUED_1:12;
then dom (f1-f2) c= dom f2 by XBOOLE_1:17;
then
A16: rng s1 c= dom f2 by A13;
then
A17: f2/*s1 is convergent by A3,A14;
dom (f1-f2) = dom f1 /\ dom f2 by VALUED_1:12;
then dom (f1-f2) c= dom f1 by XBOOLE_1:17;
then
A18: rng s1 c= dom f1 by A13;
then
A19: f1/*s1 is convergent by A2,A14;
then f1/*s1-f2/*s1 is convergent by A17;
hence (f1-f2)/*s1 is convergent by A15,RFUNCT_2:8;
A20: f1.x0 = lim (f1/*s1) by A2,A14,A18;
A21: f2.x0 = lim (f2/*s1) by A3,A14,A16;
x0 in dom (f1-f2) by A1,VALUED_1:12;
hence (f1-f2).x0 = f1.x0 - f2.x0 by VALUED_1:13
.= lim (f1/*s1 - f2/*s1) by A19,A20,A17,A21,SEQ_2:12
.= lim ((f1-f2)/*s1) by A15,RFUNCT_2:8;
end;
hence f1-f2 is_continuous_in x0;
let s1;
assume that
A22: rng s1 c= dom(f1(#) f2) and
A23: s1 is convergent & lim s1=x0;
dom (f1(#)f2) = dom f1 /\ dom f2 by VALUED_1:def 4;
then dom (f1(#)f2) c= dom f2 by XBOOLE_1:17;
then
A24: rng s1 c= dom f2 by A22;
then
A25: f2/*s1 is convergent by A3,A23;
A26: rng s1 c= dom f1 /\ dom f2 by A22,VALUED_1:def 4;
dom (f1(#)f2) = dom f1 /\ dom f2 by VALUED_1:def 4;
then dom (f1(#)f2) c= dom f1 by XBOOLE_1:17;
then
A27: rng s1 c= dom f1 by A22;
then
A28: f1/*s1 is convergent by A2,A23;
then (f1/*s1)(#)(f2/*s1) is convergent by A25;
hence (f1(#)f2)/*s1 is convergent by A26,RFUNCT_2:8;
A29: f1.x0 = lim (f1/*s1) by A2,A23,A27;
A30: f2.x0 = lim (f2/*s1) by A3,A23,A24;
thus (f1(#)f2).x0 = f1.x0 * f2.x0 by VALUED_1:5
.= lim ((f1/*s1)(#)(f2/*s1)) by A28,A29,A25,A30,SEQ_2:15
.= lim ((f1(#)f2)/*s1) by A26,RFUNCT_2:8;
end;
theorem Th8:
x0 in dom f & f is_continuous_in x0 implies r(#)f is_continuous_in x0
proof
assume x0 in dom f;
then
A1: x0 in dom (r(#)f) by VALUED_1:def 5;
assume
A2: f is_continuous_in x0;
let s1;
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,VALUED_1:def 5;
then
A6: f.x0 = lim (f/*s1) by A2,A4;
A7: f/*s1 is convergent by A2,A4,A5;
then r(#)(f/*s1) is convergent;
hence (r(#)f)/*s1 is convergent by A5,RFUNCT_2:9;
thus (r(#)f).x0 = r*f.x0 by A1,VALUED_1:def 5
.= lim (r(#)(f/*s1)) by A7,A6,SEQ_2:8
.= lim ((r(#)f)/*s1) by A5,RFUNCT_2:9;
end;
theorem
x0 in dom f & f is_continuous_in x0 implies abs(f) is_continuous_in x0
& -f is_continuous_in x0
proof
assume
A1: x0 in dom f;
assume
A2: f is_continuous_in x0;
now
let s1;
assume that
A3: rng s1 c= dom(abs(f)) and
A4: s1 is convergent & lim s1=x0;
A5: rng s1 c= dom f by A3,VALUED_1:def 11;
then
A6: f.x0 = lim (f/*s1) by A2,A4;
A7: f/*s1 is convergent by A2,A4,A5;
then abs(f/*s1) is convergent by SEQ_4:13;
hence (abs(f))/*s1 is convergent by A5,RFUNCT_2:10;
thus (abs(f)).x0 = |.f.x0.| by VALUED_1:18
.= lim (abs(f/*s1)) by A7,A6,SEQ_4:14
.= lim ((abs(f))/*s1) by A5,RFUNCT_2:10;
end;
hence abs(f) is_continuous_in x0;
thus thesis by A1,A2,Th8;
end;
theorem Th10:
f is_continuous_in x0 & f.x0<>0 implies f^ is_continuous_in x0
proof
assume that
A1: f is_continuous_in x0 and
A2: f.x0<>0;
not f.x0 in {0} by A2,TARSKI:def 1;
then
A3: not x0 in f"{0} by FUNCT_1:def 7;
let s1;
assume that
A4: rng s1 c= dom (f^) and
A5: s1 is convergent & lim s1=x0;
dom f \ f"{0} c= dom f & rng s1 c= dom f \ f"{0} by A4,RFUNCT_1:def 2
,XBOOLE_1:36;
then rng s1 c= dom f;
then
A6: f/*s1 is convergent & f.x0 = lim (f/*s1) by A1,A5;
then (f/*s1)" is convergent by A2,A4,RFUNCT_2:11,SEQ_2:21;
hence (f^)/*s1 is convergent by A4,RFUNCT_2:12;
x0 in dom f by A2,FUNCT_1:def 2;
then x0 in dom f \ f"{0} by A3,XBOOLE_0:def 5;
then x0 in dom (f^) by RFUNCT_1:def 2;
hence (f^).x0 = (f.x0)" by RFUNCT_1:def 2
.= lim ((f/*s1)") by A2,A4,A6,RFUNCT_2:11,SEQ_2:22
.= lim ((f^)/*s1) by A4,RFUNCT_2:12;
end;
theorem
x0 in dom f2 & f1 is_continuous_in x0 & f1.x0<>0 & f2 is_continuous_in
x0 implies f2/f1 is_continuous_in x0
proof
assume
A1: x0 in dom f2;
assume that
A2: f1 is_continuous_in x0 and
A3: f1.x0<>0 and
A4: f2 is_continuous_in x0;
not f1.x0 in {0} by A3,TARSKI:def 1;
then
A5: not x0 in f1"{0} by FUNCT_1:def 7;
x0 in dom f1 by A3,FUNCT_1:def 2;
then x0 in dom f1 \ f1"{0} by A5,XBOOLE_0:def 5;
then x0 in dom(f1^) by RFUNCT_1:def 2;
then
A6: x0 in dom(f1^) /\ dom f2 by A1,XBOOLE_0:def 4;
f1^ is_continuous_in x0 by A2,A3,Th10;
then f2(#)(f1^) is_continuous_in x0 by A4,A6,Th7;
hence thesis by RFUNCT_1:31;
end;
theorem Th12:
x0 in dom (f2*f1) & f1 is_continuous_in x0 & f2 is_continuous_in
f1.x0 implies f2*f1 is_continuous_in x0
proof
assume
A1: x0 in dom (f2*f1);
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in f1.x0;
let s1 such that
A4: rng s1 c= dom (f2*f1) and
A5: s1 is convergent & lim s1 = x0;
A6: dom (f2*f1) c= dom f1 by RELAT_1:25;
now
let x be object;
assume x in rng (f1/*s1);
then consider n such that
A7: x=(f1/*s1).n by FUNCT_2:113;
s1.n in rng s1 by VALUED_0:28;
then f1.(s1.n) in dom f2 by A4,FUNCT_1:11;
hence x in dom f2 by A4,A6,A7,FUNCT_2:108,XBOOLE_1:1;
end;
then
A8: rng (f1/*s1) c= dom f2;
now
let n;
s1.n in rng s1 by VALUED_0:28;
then
A9: s1.n in dom f1 by A4,FUNCT_1:11;
thus ((f2*f1)/*s1).n = (f2*f1).(s1.n) by A4,FUNCT_2:108
.= f2.(f1.(s1.n)) by A9,FUNCT_1:13
.= f2.((f1/*s1).n) by A4,A6,FUNCT_2:108,XBOOLE_1:1
.= (f2/*(f1/*s1)).n by A8,FUNCT_2:108;
end;
then
A10: f2/*(f1/*s1) = (f2*f1)/*s1 by FUNCT_2:63;
rng s1 c= dom f1 by A4,A6;
then
A11: f1/*s1 is convergent & f1.x0 = lim (f1/*s1) by A2,A5;
then f2.(f1.x0) = lim (f2/*(f1/*s1)) by A3,A8;
hence thesis by A1,A3,A11,A8,A10,FUNCT_1:12;
end;
definition
let f;
attr f is continuous means
:Def2:
for x0 st x0 in dom f holds f is_continuous_in x0;
end;
theorem Th13:
for X,f st X c= dom f holds f|X is continuous iff for s1 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 X,f such that
A1: X c= dom f;
thus f|X is continuous implies for s1 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
A2: f|X is continuous;
now
let s1 such that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X;
A6: dom (f|X) = dom f /\ X by RELAT_1:61
.= X by A1,XBOOLE_1:28;
then
A7: f|X is_continuous_in (lim s1) by A2,A5;
now
let n;
A8: s1.n in rng s1 by VALUED_0:28;
thus ((f|X)/*s1).n = (f|X).(s1.n) by A3,A6,FUNCT_2:108
.= f.(s1.n) by A3,A6,A8,FUNCT_1:47
.= (f/*s1).n by A1,A3,FUNCT_2:108,XBOOLE_1:1;
end;
then
A9: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
f.(lim s1) = (f|X).(lim s1) by A5,A6,FUNCT_1:47
.= lim (f/*s1) by A3,A4,A6,A7,A9;
hence
f/*s1 is convergent & f.(lim s1) = lim (f/*s1) by A3,A4,A6,A7,A9;
end;
hence thesis;
end;
assume
A10: for s1 st rng s1 c= X & s1 is convergent & lim s1 in X holds f/*s1
is convergent & f.(lim s1) = lim (f/*s1);
now
A11: dom (f|X) = dom f /\ X by RELAT_1:61
.= X by A1,XBOOLE_1:28;
let x1 such that
A12: x1 in dom(f|X);
now
let s1 such that
A13: rng s1 c= dom (f|X) and
A14: s1 is convergent and
A15: lim s1 = x1;
now
let n;
A16: s1.n in rng s1 by VALUED_0:28;
thus ((f|X)/*s1).n = (f|X).(s1.n) by A13,FUNCT_2:108
.= f.(s1.n) by A13,A16,FUNCT_1:47
.= (f/*s1).n by A1,A11,A13,FUNCT_2:108,XBOOLE_1:1;
end;
then
A17: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
(f|X).(lim s1) = f.(lim s1) by A12,A15,FUNCT_1:47
.= lim ((f|X)/*s1) by A10,A12,A11,A13,A14,A15,A17;
hence
(f|X)/*s1 is convergent & (f|X).x1 = lim ((f|X)/*s1) by A10,A12,A11,A13
,A14,A15,A17;
end;
hence f|X is_continuous_in x1;
end;
hence thesis;
end;
theorem Th14:
X c= dom f implies (f|X is continuous iff for x0,r st x0 in X &
0<r ex s st 0<s & for x1 st x1 in X & |.x1-x0.| < s holds |.f.x1-f.x0.| < r
)
proof
assume
A1: X c= dom f;
thus f|X is continuous implies for x0,r st x0 in X & 0<r ex s st 0<s & for
x1 st x1 in X & |.x1-x0.| < s holds |.f.x1-f.x0.| < r
proof
assume
A2: f|X is continuous;
let x0,r;
assume that
A3: x0 in X and
A4: 0<r;
x0 in dom(f|X) by A1,A3,RELAT_1:62;
then f|X is_continuous_in x0 by A2;
then consider s such that
A5: 0<s and
A6: for x1 st x1 in dom(f|X) & |.x1-x0.|<s holds |.(f|X).x1-(f|X).
x0.| <r by A4,Th3;
take s;
thus 0<s by A5;
let x1;
assume that
A7: x1 in X and
A8: |.x1-x0.|<s;
A9: dom (f|X) = dom f /\ X by RELAT_1:61
.= X by A1,XBOOLE_1:28;
then |.f.x1-f.x0.| = |.(f|X).x1 - f.x0.| by A7,FUNCT_1:47
.= |.(f|X).x1 - (f|X).x0.| by A3,A9,FUNCT_1:47;
hence thesis by A6,A9,A7,A8;
end;
assume
A10: for x0,r st x0 in X & 0<r ex s st 0<s & for x1 st x1 in X & |.x1-
x0.| < s holds |.f.x1-f.x0.| < r;
now
let x0 such that
A11: x0 in dom(f|X);
A12: x0 in X by A11;
for r st 0<r ex s st 0<s & for x1 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
A13: 0<s and
A14: for x1 st x1 in X & |.x1-x0.| < s holds |.f.x1-f.x0.| < r by A10,A12;
take s;
thus 0<s by A13;
let x1 such that
A15: x1 in dom(f|X) and
A16: |.x1-x0.|<s;
|.(f|X).x1-(f|X).x0.| = |.(f|X).x1 - f.x0.| by A11,FUNCT_1:47
.= |.f.x1-f.x0.| by A15,FUNCT_1:47;
hence thesis by A14,A15,A16;
end;
hence f|X is_continuous_in x0 by Th3;
end;
hence thesis;
end;
registration
cluster constant -> continuous for PartFunc of REAL,REAL;
coherence
proof
let f be PartFunc of REAL,REAL;
assume
A1: f is constant;
now
reconsider s = 1 as Real;
let x0,r;
assume that
A2: x0 in dom f and
A3: 0<r;
take s;
thus 0<s;
let x1;
assume
A4: x1 in dom f;
assume |.x1-x0.| < s;
f.x1 = f.x0 by A1,A2,A4;
hence |.f.x1-f.x0.| < r by A3,ABSVALUE:2;
end;
then f|dom f is continuous by Th14;
hence thesis;
end;
end;
registration
cluster continuous for PartFunc of REAL,REAL;
existence
proof
set f = the constant PartFunc of REAL,REAL;
take f;
thus thesis;
end;
end;
registration
let f be continuous PartFunc of REAL,REAL, X be set;
cluster f|X -> continuous for PartFunc of REAL,REAL;
coherence
proof
for x0 st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0;
assume
A1: x0 in dom(f|X);
then x0 in dom f by RELAT_1:57;
then
A2: f is_continuous_in x0 by Def2;
x0 in X by A1;
hence thesis by A2,Th1;
end;
hence thesis;
end;
end;
theorem
f|X is continuous iff f|X|X is continuous;
theorem Th16:
f|X is continuous & X1 c= X implies f|X1 is continuous
proof
assume
A1: f|X is continuous;
assume X1 c= X;
then f|X1 = f|X|X1 by RELAT_1:74;
hence thesis by A1;
end;
registration
cluster empty -> continuous for PartFunc of REAL,REAL;
coherence;
end;
registration
let f;
let X be trivial set;
cluster f|X -> continuous for PartFunc of REAL,REAL;
coherence
proof
per cases;
suppose
f|X is empty;
hence thesis;
end;
suppose
f|X is not empty;
then consider x0 such that
A1: x0 in dom(f|X qua PartFunc of REAL,REAL) by MEMBERED:9;
x0 in X by A1,RELAT_1:57;
then
A2: X = {x0} by ZFMISC_1:132;
now
let p;
assume p in dom(f|X);
then
A3: p in {x0} by A2;
thus f|X is_continuous_in p
proof
let s1;
assume that
A4: rng s1 c= dom(f|X) and
s1 is convergent and
lim s1=p;
A5: dom f /\ {x0} c= {x0} by XBOOLE_1:17;
rng s1 c= dom f /\ {x0} by A2,A4,RELAT_1:61;
then
A6: rng s1 c= {x0} by A5;
A7: now
let n;
s1.n in rng s1 by VALUED_0:28;
hence s1.n = x0 by A6,TARSKI:def 1;
end;
A8: p=x0 by A3,TARSKI:def 1;
A9: now
let g be Real such that
A10: 0<g;
reconsider n = 0 as Nat;
take n;
let m be Nat such that
n<=m;
A11: m in NAT by ORDINAL1:def 12;
|.((f|{x0})/*s1).m - (f|{x0}).p.| = |.(f|{x0}).(s1.m) - (f
|{x0}).x0.| by A2,A8,A4,FUNCT_2:108,A11
.= |.(f|{x0}).x0 - (f|{x0}).x0.| by A7,A11
.= 0 by ABSVALUE:2;
hence |.((f|{x0})/*s1).m - (f|{x0}).p.| < g by A10;
end;
hence (f|X)/*s1 is convergent by A2,SEQ_2:def 6;
hence thesis by A2,A9,SEQ_2:def 7;
end;
end;
hence thesis;
end;
end;
end;
theorem
f|{x0} is continuous;
registration
let f1,f2 be continuous PartFunc of REAL,REAL;
cluster f1+f2 -> continuous for PartFunc of REAL,REAL;
coherence
proof
set X = dom(f1+f2);
X c= dom f1 /\ dom f2 by VALUED_1:def 1;
then
A1: X c= dom f1 & X c= dom f2 by XBOOLE_1:18;
A2: f1|X is continuous & f2|X is continuous;
now
let s1;
assume that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X;
A6: f1/*s1 is convergent & f2/*s1 is convergent by A1,A2,A3,A4,A5,Th13;
then
A7: (f1/*s1)+(f2/*s1) is convergent;
A8: rng s1 c= dom f1 /\ dom f2 by A3,VALUED_1:def 1;
f1.(lim s1) = lim (f1/*s1) & f2.(lim s1) = lim (f2/*s1) by A1,A2,A3,A4,A5
,Th13;
then (f1+f2).(lim s1) = lim (f1/*s1) + lim (f2/*s1) by A5,VALUED_1:def 1
.= lim (f1/*s1 + f2/*s1) by A6,SEQ_2:6
.= lim ((f1+f2)/*s1) by A8,RFUNCT_2:8;
hence (f1+f2)/*s1 is convergent & (f1+f2).(lim s1)=lim((f1+f2)/*s1) by A8
,A7,RFUNCT_2:8;
end;
then (f1+f2)|X is continuous by Th13;
hence thesis;
end;
cluster f1-f2 -> continuous for PartFunc of REAL,REAL;
coherence
proof
set X = dom(f1-f2);
X c= dom f1 /\ dom f2 by VALUED_1:12;
then
A9: X c= dom f1 & X c= dom f2 by XBOOLE_1:18;
A10: f1|X is continuous & f2|X is continuous;
now
let s1;
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 A9,A10,A11,A12,A13,Th13;
then
A15: (f1/*s1)-(f2/*s1) is convergent;
A16: rng s1 c= dom f1 /\ dom f2 by A11,VALUED_1:12;
f1.(lim s1) = lim (f1/*s1) & f2.(lim s1) = lim (f2/*s1) by A9,A10,A11,A12
,A13,Th13;
then (f1-f2).(lim s1) = lim (f1/*s1) - lim (f2/*s1) by A13,VALUED_1:13
.= lim (f1/*s1 - f2/*s1) by A14,SEQ_2:12
.= lim ((f1-f2)/*s1) by A16,RFUNCT_2:8;
hence (f1-f2)/*s1 is convergent & (f1-f2).(lim s1)=lim((f1-f2)/*s1) by
A16,A15,RFUNCT_2:8;
end;
then (f1-f2)|X is continuous by Th13;
hence thesis;
end;
cluster f1(#)f2 -> continuous for PartFunc of REAL,REAL;
coherence
proof
set X = dom(f1(#)f2);
X c= dom f1 /\ dom f2 by VALUED_1:def 4;
then
A17: X c= dom f1 & X c= dom f2 by XBOOLE_1:18;
A18: f1|X is continuous & f2|X is continuous;
now
let s1;
assume that
A19: rng s1 c= X and
A20: s1 is convergent and
A21: lim s1 in X;
A22: f1/*s1 is convergent & f2/*s1 is convergent by A17,A18,A19,A20,A21,Th13;
then
A23: (f1/*s1)(#)(f2/*s1) is convergent;
A24: rng s1 c= dom f1 /\ dom f2 by A19,VALUED_1:def 4;
f1.(lim s1) = lim (f1/*s1) & f2.(lim s1) = lim (f2/*s1) by A17,A18,A19
,A20,A21,Th13;
then (f1(#)f2).(lim s1) = lim (f1/*s1) * lim (f2/*s1) by A21,
VALUED_1:def 4
.= lim ((f1/*s1)(#)(f2/*s1)) by A22,SEQ_2:15
.= lim ((f1(#)f2)/*s1) by A24,RFUNCT_2:8;
hence
(f1(#)f2)/*s1 is convergent & (f1(#)f2).(lim s1)=lim((f1(#)f2)/*s1)
by A24,A23,RFUNCT_2:8;
end;
then (f1(#)f2)|X is continuous by Th13;
hence thesis;
end;
end;
theorem Th18:
for X,f1,f2 st X c= dom f1 /\ dom f2 & f1|X is continuous & f2|X
is continuous holds (f1+f2)|X is continuous & (f1-f2)|X is continuous & (f1(#)
f2)|X is continuous
proof
let X,f1,f2 such that
A1: X c= dom f1 /\ dom f2;
assume
A2: f1|X is continuous & f2|X is continuous;
A3: X c= dom f1 & X c= dom f2 by A1,XBOOLE_1:18;
A4: now
let s1;
assume that
A5: rng s1 c= X and
A6: s1 is convergent & lim s1 in X;
A7: rng s1 c= dom f1 /\ dom f2 by A1,A5;
A8: f1/*s1 is convergent & f2/*s1 is convergent by A3,A2,A5,A6,Th13;
then
A9: (f1/*s1)(#)(f2/*s1) is convergent;
f1.(lim s1) = lim (f1/*s1) & f2.(lim s1) = lim (f2/*s1) by A3,A2,A5,A6,Th13
;
then (f1(#)f2).(lim s1) = lim (f1/*s1) * lim (f2/*s1) by VALUED_1:5
.= lim ((f1/*s1) (#) (f2/*s1)) by A8,SEQ_2:15
.= lim ((f1(#)f2)/*s1) by A7,RFUNCT_2:8;
hence (f1(#)f2)/*s1 is convergent & (f1(#)f2).(lim s1)=lim((f1(#) f2)/*s1)
by A7,A9,RFUNCT_2:8;
end;
A10: X c= dom (f1+f2) by A1,VALUED_1:def 1;
now
let s1;
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 A3,A2,A11,A12,A13,Th13;
then
A15: (f1/*s1)+(f2/*s1) is convergent;
A16: rng s1 c= dom f1 /\ dom f2 by A1,A11;
f1.(lim s1) = lim (f1/*s1) & f2.(lim s1) = lim (f2/*s1) by A3,A2,A11,A12
,A13,Th13;
then (f1+f2).(lim s1) = lim (f1/*s1) + lim (f2/*s1) by A10,A13,
VALUED_1:def 1
.= lim (f1/*s1 + f2/*s1) by A14,SEQ_2:6
.= lim ((f1+f2)/*s1) by A16,RFUNCT_2:8;
hence
(f1+f2)/*s1 is convergent & (f1+f2).(lim s1)=lim((f1+f2)/*s1) by A16,A15,
RFUNCT_2:8;
end;
hence (f1+f2)|X is continuous by A10,Th13;
A17: X c= dom (f1-f2) by A1,VALUED_1:12;
now
let s1;
assume that
A18: rng s1 c= X and
A19: s1 is convergent and
A20: lim s1 in X;
A21: f1/*s1 is convergent & f2/*s1 is convergent by A3,A2,A18,A19,A20,Th13;
then
A22: (f1/*s1)-(f2/*s1) is convergent;
A23: rng s1 c= dom f1 /\ dom f2 by A1,A18;
f1.(lim s1) = lim (f1/*s1) & f2.(lim s1) = lim (f2/*s1) by A3,A2,A18,A19
,A20,Th13;
then (f1-f2).(lim s1) = lim (f1/*s1) - lim (f2/*s1) by A17,A20,VALUED_1:13
.= lim (f1/*s1 - f2/*s1) by A21,SEQ_2:12
.= lim ((f1-f2)/*s1) by A23,RFUNCT_2:8;
hence
(f1-f2)/*s1 is convergent & (f1-f2).(lim s1)=lim((f1-f2)/*s1) by A23,A22,
RFUNCT_2:8;
end;
hence (f1-f2)|X is continuous by A17,Th13;
X c= dom (f1(#)f2) by A1,VALUED_1:def 4;
hence thesis by A4,Th13;
end;
theorem
for X,X1,f1,f2 st X c= dom f1 & X1 c= dom f2 & f1|X is continuous & f2
|X1 is continuous holds (f1+f2)|(X /\ X1) is continuous & (f1-f2)|(X /\ X1) is
continuous & (f1(#)f2)|(X /\ X1) is continuous
proof
let X,X1,f1,f2;
assume X c= dom f1 & X1 c= dom f2;
then
A1: X /\ X1 c= dom f1 /\ dom f2 by XBOOLE_1:27;
assume f1|X is continuous & f2|X1 is continuous;
then f1|(X /\ X1) is continuous & f2|(X /\ X1) is continuous by Th16,
XBOOLE_1:17;
hence thesis by A1,Th18;
end;
registration
let f be continuous PartFunc of REAL,REAL;
let r;
cluster r(#)f -> continuous for PartFunc of REAL,REAL;
coherence
proof
set X = dom f;
A1: X c= dom(r(#)f) by VALUED_1:def 5;
A2: f|X is continuous;
A3: now
let s1;
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f/*s1 is convergent by A2,A4,A5,A6,Th13;
then
A8: r(#)(f/*s1) is convergent;
f.(lim s1) = lim (f/*s1) by A2,A4,A5,A6,Th13;
then (r(#)f).(lim s1) = r * lim (f/*s1) by A1,A6,VALUED_1:def 5
.= lim (r(#)(f/*s1)) by A7,SEQ_2:8
.= lim ((r(#)f)/*s1) by A4,RFUNCT_2:9;
hence
(r(#)f)/*s1 is convergent & (r(#)f).(lim s1)=lim((r(#)f)/*s1) by A4,A8,
RFUNCT_2:9;
end;
dom(r(#)f) = X by VALUED_1:def 5;
then (r(#)f)|X = r(#)f;
hence thesis by A1,A3,Th13;
end;
end;
theorem Th20:
for r,X,f st X c= dom f & f|X is continuous holds (r(#)f)|X is continuous
proof
let r,X,f such that
A1: X c= dom f;
assume
A2: f|X is continuous;
A3: X c= dom(r(#)f) by A1,VALUED_1:def 5;
now
let s1;
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,A2,A4,A5,A6,Th13;
then
A8: r(#)(f/*s1) is convergent;
f.(lim s1) = lim (f/*s1) by A1,A2,A4,A5,A6,Th13;
then (r(#)f).(lim s1) = r * lim (f/*s1) by A3,A6,VALUED_1:def 5
.= lim (r(#)(f/*s1)) by A7,SEQ_2:8
.= lim ((r(#)f)/*s1) by A1,A4,RFUNCT_2:9,XBOOLE_1:1;
hence (r(#)f)/*s1 is convergent & (r(#)f).(lim s1)=lim((r(#)f)/*s1) by A1
,A4,A8,RFUNCT_2:9,XBOOLE_1:1;
end;
hence thesis by A3,Th13;
end;
theorem
X c= dom f & f|X is continuous implies (abs f)|X is continuous & (-f)|
X is continuous
proof
assume
A1: X c= dom f;
assume
A2: f|X is continuous;
thus (abs f)|X is continuous
proof
let r;
assume
A3: r in dom((abs f)|X);
then r in dom abs f by RELAT_1:57;
then
A4: r in dom f by VALUED_1:def 11;
r in X by A3;
then
A5: r in dom(f|X) by A4,RELAT_1:57;
then
A6: f|X is_continuous_in r by A2;
thus (abs(f))|X is_continuous_in r
proof
let s1;
assume that
A7: rng s1 c= dom ((abs(f))|X) and
A8: s1 is convergent & lim s1 = r;
rng s1 c= dom (abs(f)) /\ X by A7,RELAT_1:61;
then rng s1 c= dom f /\ X by VALUED_1:def 11;
then
A9: rng s1 c= dom (f|X) by RELAT_1:61;
now
let n;
A10: s1.n in rng s1 by VALUED_0:28;
then s1.n in dom (f|X) by A9;
then s1.n in dom f /\ X by RELAT_1:61;
then
A11: s1.n in X by XBOOLE_0:def 4;
thus (abs((f|X)/*s1)).n = |.((f|X)/*s1).n.| by SEQ_1:12
.=|.(f|X).(s1.n).| by A9,FUNCT_2:108
.=|.f.(s1.n).| by A9,A10,FUNCT_1:47
.=(abs(f)).(s1.n) by VALUED_1:18
.=((abs(f))|X).(s1.n) by A11,FUNCT_1:49
.=(((abs(f))|X)/*s1).n by A7,FUNCT_2:108;
end;
then
A12: abs((f|X)/*s1) = ((abs(f))|X)/*s1 by FUNCT_2:63;
A13: |.(f|X).r.| = |.f.r.| by A5,FUNCT_1:47
.= (abs(f)).r by VALUED_1:18
.= ((abs(f))|X).r by A3,FUNCT_1:47;
A14: (f|X)/*s1 is convergent by A6,A8,A9;
hence ((abs(f))|X)/*s1 is convergent by A12,SEQ_4:13;
(f|X).r = lim ((f|X)/*s1) by A6,A8,A9;
hence thesis by A14,A12,A13,SEQ_4:14;
end;
end;
thus thesis by A1,A2,Th20;
end;
theorem Th22:
f|X is continuous & f"{0} = {} implies f^|X is continuous
proof
assume that
A1: f|X is continuous and
A2: f"{0} = {};
A3: dom(f^) = dom f \ {} by A2,RFUNCT_1:def 2
.= dom f;
let r;
assume
A4: r in dom(f^|X);
then
A5: r in dom(f^) by RELAT_1:57;
r in X by A4;
then
A6: r in dom(f|X) by A3,A5,RELAT_1:57;
then
A7: f|X is_continuous_in r by A1;
now
A8: now
assume f.r = 0;
then f.r in {0} by TARSKI:def 1;
hence contradiction by A2,A3,A5,FUNCT_1:def 7;
end;
let s1;
assume that
A9: rng s1 c= dom((f^)|X) and
A10: s1 is convergent & lim s1= r;
rng s1 c= dom(f^) /\ X by A9,RELAT_1:61;
then
A11: rng s1 c= dom(f|X) by A3,RELAT_1:61;
then
A12: (f|X)/*s1 is convergent by A7,A10;
now
let n be Nat;
A13: s1.n in rng s1 by VALUED_0:28;
rng s1 c= dom f /\ X & dom f /\ X c= dom f by A3,A9,RELAT_1:61
,XBOOLE_1:17;
then
A14: rng s1 c= dom f;
A15: now
assume f.(s1.n)=0;
then f.(s1.n) in {0} by TARSKI:def 1;
hence contradiction by A2,A14,A13,FUNCT_1:def 7;
end;
n in NAT by ORDINAL1:def 12;
then ((f|X)/*s1).n = (f|X).(s1.n) by A11,FUNCT_2:108
.= f.(s1.n) by A11,A13,FUNCT_1:47;
hence ((f|X)/*s1).n <>0 by A15;
end;
then
A16: (f|X)/*s1 is non-zero by SEQ_1:5;
now
let n;
A17: s1.n in rng s1 by VALUED_0:28;
then s1.n in dom((f^)|X) by A9;
then s1.n in dom (f^) /\ X by RELAT_1:61;
then
A18: s1.n in dom (f^) by XBOOLE_0:def 4;
thus (((f^)|X)/*s1).n = ((f^)|X).(s1.n) by A9,FUNCT_2:108
.= (f^).(s1.n) by A9,A17,FUNCT_1:47
.= (f.(s1.n))" by A18,RFUNCT_1:def 2
.= ((f|X).(s1.n))" by A11,A17,FUNCT_1:47
.= (((f|X)/*s1).n)" by A11,FUNCT_2:108
.= (((f|X)/*s1)").n by VALUED_1:10;
end;
then
A19: ((f^)|X)/*s1 = ((f|X)/*s1)" by FUNCT_2:63;
A20: (f|X).r = f.r by A6,FUNCT_1:47;
then lim ((f|X)/*s1) <> 0 by A7,A10,A11,A8;
hence ((f^)|X)/*s1 is convergent by A12,A16,A19,SEQ_2:21;
(f|X).r = lim ((f|X)/*s1) by A7,A10,A11;
hence lim (((f^)|X)/*s1) = ((f|X).r)" by A12,A20,A8,A16,A19,SEQ_2:22
.= (f.r)" by A6,FUNCT_1:47
.= (f^).r by A5,RFUNCT_1:def 2
.= ((f^)|X).r by A4,FUNCT_1:47;
end;
hence thesis;
end;
theorem
f|X is continuous & (f|X)"{0} = {} implies f^|X is continuous
proof
assume that
A1: f|X is continuous and
A2: (f|X)"{0} = {};
f|X|X is continuous by A1;
then (f|X)^|X is continuous by A2,Th22;
then (f^)|X|X is continuous by RFUNCT_1:46;
hence thesis;
end;
theorem
X c= dom f1 /\ dom f2 & f1|X is continuous & f1"{0} = {} & f2|X is
continuous implies (f2/f1)|X is continuous
proof
assume
A1: X c= dom f1 /\ dom f2;
assume that
A2: f1|X is continuous and
A3: f1"{0} = {} and
A4: f2|X is continuous;
A5: dom(f1^) = dom f1 \ {} by A3,RFUNCT_1:def 2
.= dom f1;
(f1^)|X is continuous by A2,A3,Th22;
then (f2(#)(f1^))|X is continuous by A1,A4,A5,Th18;
hence thesis by RFUNCT_1:31;
end;
registration
let f1,f2 be continuous PartFunc of REAL,REAL;
cluster f2*f1 -> continuous for PartFunc of REAL,REAL;
coherence
proof
now
let x0;
assume
A1: x0 in dom(f2*f1);
then f1.x0 in dom f2 by FUNCT_1:11;
then
A2: f2 is_continuous_in f1.x0 by Def2;
x0 in dom f1 by A1,FUNCT_1:11;
then f1 is_continuous_in x0 by Def2;
hence f2*f1 is_continuous_in x0 by A1,A2,Th12;
end;
hence thesis;
end;
end;
theorem
f1|X is continuous & f2|(f1.:X) is continuous implies (f2*f1)|X is continuous
proof
(f2*f1)|X = (f2|(f1.:X))*(f1|X) by FUNCT_1:99;
hence thesis;
end;
theorem
f1|X is continuous & f2|X1 is continuous implies (f2*f1)|(X /\ (f1"X1)
) is continuous
proof
(f2|X1)*(f1|X) = (f2*f1)|(X /\ (f1"X1)) by FUNCT_1:100;
hence thesis;
end;
theorem
f is total & (for x1,x2 holds f.(x1+x2) = f.x1 + f.x2) & (ex x0 st f
is_continuous_in x0) implies f|REAL is continuous
proof
assume that
A1: f is total and
A2: for x1,x2 holds f.(x1+x2) = f.x1 + f.x2;
A3: dom f = REAL by A1,PARTFUN1:def 2;
given x0 such that
A4: f is_continuous_in x0;
A5: f.x0 + (0 qua Nat) = f.(x0+(0 qua Nat)) .= f.x0+f.0 by A2;
A6: now
let x1;
0 = f.(x1+-x1) by A5
.= f.x1+f.(-x1) by A2;
hence -(f.x1)=f.(-x1);
end;
A7: now
let x1,x2;
thus f.(x1-x2)=f.(x1+-x2) .= f.x1 + f.(-x2) by A2
.= f.x1 +- f.x2 by A6
.= f.x1 - f.x2;
end;
now
let x1,r;
assume that
x1 in REAL and
A8: r>0;
set y=x1-x0;
consider s such that
A9: 0<s and
A10: for x1 st x1 in dom f & |.x1-x0.|<s holds |.f.x1-f.x0.|<r by A4,A8,Th3;
take s;
thus s>0 by A9;
let x2 such that
x2 in REAL and
A11: |.x2-x1.|<s;
A12: x2-y in REAL & |.x2-y-x0.|=|.x2-x1.| by XREAL_0:def 1;
y+x0=x1;
then |.f.x2-f.x1.| = |.f.x2-(f.y+f.x0).| by A2
.= |.f.x2-f.y-f.x0.|
.= |.f.(x2-y)-f.x0.| by A7;
hence |.f.x2-f.x1.|<r by A3,A10,A11,A12;
end;
hence thesis by A3,Th14;
end;
theorem Th28:
for f st dom f is compact & f|dom f is continuous holds rng f is compact
proof
let f;
assume that
A1: dom f is compact and
A2: f|dom f is continuous;
now
let s1 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 being Element of REAL st P[n,p]
proof
let n;
s1.n in rng s1 by VALUED_0:28;
then consider p being Element of REAL such that
A5: p in dom f & s1.n=f.p by A3,PARTFUN1:3;
take p;
thus thesis by A5;
end;
consider q1 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 ex n st x = q1.n by FUNCT_2:113;
hence x in dom f by A6;
end;
then
A7: rng q1 c= dom f;
then consider s2 such that
A8: s2 is subsequence of q1 and
A9: s2 is convergent and
A10: (lim s2) in dom f by A1,RCOMP_1:def 3;
now
let n;
f.(q1.n)=s1.n by A6;
hence (f/*q1).n= s1.n by A7,FUNCT_2:108;
end;
then
A11: f/*q1=s1 by FUNCT_2:63;
take q2 = f/*s2;
lim s2 in dom(f|(dom f)) by A10;
then f|(dom f) is_continuous_in (lim s2) by A2;
then
A12: f is_continuous_in (lim s2);
rng s2 c= rng q1 by A8,VALUED_0:21;
then
A13: rng s2 c= dom f by A7;
then f.(lim s2) = lim (f/*s2) by A9,A12;
hence
q2 is subsequence of s1 & q2 is convergent & (lim q2) in rng f by A7,A11,A8
,A9,A10,A12,A13,FUNCT_1:def 3,VALUED_0:22;
end;
hence thesis by RCOMP_1:def 3;
end;
theorem
Y c= dom f & Y is compact & f|Y is continuous implies (f.:Y) is compact
proof
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f|Y is continuous;
A4: f|Y|Y is continuous by A3;
dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A1,XBOOLE_1:28;
then rng (f|Y) is compact by A2,A4,Th28;
hence thesis by RELAT_1:115;
end;
theorem Th30:
for f st dom f<>{} & (dom f) is compact & f|dom f is continuous
ex x1,x2 st x1 in dom f & x2 in dom f & f.x1 = upper_bound (rng f) & f.x2 =
lower_bound (rng f)
proof
let f;
assume dom f <> {} & dom f is compact & f|dom f is continuous;
then
A1: rng f <> {} & rng f is compact by Th28,RELAT_1:42;
then consider x being Element of REAL 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 REAL 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;
end;
::$N Extreme value theorem
theorem
for f,Y st Y<>{} & Y c= dom f & Y is compact & f|Y is continuous ex x1
,x2 st x1 in Y & x2 in Y & f.x1 = upper_bound (f.:Y) & f.x2 = lower_bound (f.:Y
)
proof
let f,Y such that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f|Y is continuous;
A5: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A2,XBOOLE_1:28;
f|Y|Y is continuous by A4;
then consider x1,x2 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,Th30;
take x1,x2;
thus x1 in Y & x2 in Y by A6;
f.x1=upper_bound(rng (f|Y)) & f.x2=lower_bound(rng (f|Y)) by A6,A7,FUNCT_1:47
;
hence thesis by RELAT_1:115;
end;
definition
let f;
attr f is Lipschitzian means
:Def3:
ex r st 0<r & for x1,x2 st x1 in dom f &
x2 in dom f holds |.f.x1-f.x2.|<=r*|.x1-x2.|;
end;
theorem Th32:
f|X is Lipschitzian iff ex r st 0<r & for x1,x2 st x1 in dom(f|X
) & x2 in dom(f|X) holds |.f.x1-f.x2.|<=r*|.x1-x2.|
proof
thus f|X is Lipschitzian implies ex r st 0<r & for x1,x2 st x1 in dom(f|X) &
x2 in dom(f|X) holds |.f.x1-f.x2.|<=r*|.x1-x2.|
proof
given r such that
A1: 0<r and
A2: for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X) holds |.(f|X).x1-(f
|X).x2.|<=r*|.x1-x2.|;
take r;
thus 0<r by A1;
let x1,x2;
assume
A3: x1 in dom(f|X) & x2 in dom(f|X);
then (f|X).x1 = f.x1 & (f|X).x2 = f.x2 by FUNCT_1:47;
hence thesis by A2,A3;
end;
given r such that
A4: 0<r and
A5: for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X) holds |.f.x1-f.x2.|<=r
*|.x1-x2.|;
take r;
thus 0<r by A4;
let x1,x2;
assume
A6: x1 in dom(f|X) & x2 in dom(f|X);
then (f|X).x1 = f.x1 & (f|X).x2 = f.x2 by FUNCT_1:47;
hence thesis by A5,A6;
end;
registration
cluster empty -> Lipschitzian for PartFunc of REAL,REAL;
coherence
proof
let f be PartFunc of REAL,REAL;
assume
A1: f is empty;
take 1;
thus thesis by A1;
end;
end;
registration
cluster empty for PartFunc of REAL,REAL;
existence
proof
take the empty PartFunc of REAL,REAL;
thus thesis;
end;
end;
registration
let f be Lipschitzian PartFunc of REAL,REAL, X be set;
cluster f|X -> Lipschitzian for PartFunc of REAL,REAL;
coherence
proof
consider r such that
A1: 0<r and
A2: for x1,x2 st x1 in dom f & x2 in dom f holds |.f.x1-f.x2.|<=r*|.x1-x2.|
by Def3;
now
let x1,x2;
assume x1 in dom(f|X) & x2 in dom(f|X);
then x1 in dom f & x2 in dom f by RELAT_1:57;
hence |.f.x1-f.x2.|<=r*|.x1-x2.| by A2;
end;
hence thesis by A1,Th32;
end;
end;
theorem
f|X is Lipschitzian & X1 c= X implies f|X1 is Lipschitzian
proof
assume that
A1: f|X is Lipschitzian and
A2: X1 c= X;
f|X1 = f|X|X1 by A2,RELAT_1:74;
hence thesis by A1;
end;
registration
let f1,f2 be Lipschitzian PartFunc of REAL,REAL;
cluster f1+f2 -> Lipschitzian for PartFunc of REAL,REAL;
coherence
proof
set X = dom f1, X1 = dom f2;
consider s such that
A1: 0<s and
A2: for x1,x2 st x1 in dom(f1|(X /\ X1)) & x2 in dom(f1|(X /\ X1))
holds |.f1.x1-f1.x2.|<=s*|.x1-x2.| by Th32;
consider g such that
A3: 0<g and
A4: for x1,x2 st x1 in dom(f2|(X /\ X1)) & x2 in dom(f2|(X /\ X1))
holds |.f2.x1-f2.x2.|<=g*|.x1-x2.| by Th32;
now
take p=s+g;
thus 0<p by A1,A3;
let x1,x2;
assume that
A5: x1 in dom(f1+f2) and
A6: x2 in dom(f1+f2);
|.(f1+f2).x1-(f1+f2).x2.| = |.f1.x1 + f2.x1-(f1+f2).x2.| by A5,
VALUED_1:def 1
.= |.f1.x1 + f2.x1 - (f1.x2+f2.x2).| by A6,VALUED_1:def 1
.= |.f1.x1 - f1.x2 + (f2.x1-f2.x2).|;
then
A7: |.(f1+f2).x1-(f1+f2).x2.|<=|.f1.x1-f1.x2.|+|.f2.x1-f2.x2.| by
COMPLEX1:56;
dom(f2|(X /\ X1)) = dom f2 /\ (X /\ X1) by RELAT_1:61
.= dom f2 /\ X1 /\ X by XBOOLE_1:16
.= dom(f1+f2) by VALUED_1:def 1;
then
A8: |.f2.x1-f2.x2.|<=g*|.x1-x2.| by A4,A5,A6;
dom(f1|(X /\ X1)) = dom f1 /\ (X /\ X1) by RELAT_1:61
.= dom f1 /\ X /\ X1 by XBOOLE_1:16
.= dom(f1+f2) by VALUED_1:def 1;
then |.f1.x1-f1.x2.|<=s*|.x1-x2.| by A2,A5,A6;
then |.f1.x1-f1.x2.|+|.f2.x1-f2.x2.|<= s*|.x1-x2.|+g*|.x1-x2.| by A8,
XREAL_1:7;
hence |.(f1+f2).x1-(f1+f2).x2.|<=p*|.x1-x2.| by A7,XXREAL_0:2;
end;
hence thesis;
end;
cluster f1-f2 -> Lipschitzian for PartFunc of REAL,REAL;
coherence
proof
set X = dom f1, X1 = dom f2;
consider s such that
A9: 0<s and
A10: for x1,x2 st x1 in dom(f1|(X /\ X1)) & x2 in dom(f1|(X /\ X1))
holds |.f1.x1-f1.x2.|<=s*|.x1-x2.| by Th32;
consider g such that
A11: 0<g and
A12: for x1,x2 st x1 in dom(f2|(X /\ X1)) & x2 in dom(f2|(X /\ X1))
holds |.f2.x1-f2.x2.|<=g*|.x1-x2.| by Th32;
now
take p=s+g;
thus 0<p by A9,A11;
let x1,x2;
assume that
A13: x1 in dom(f1-f2) and
A14: x2 in dom(f1-f2);
|.(f1-f2).x1-(f1-f2).x2.| = |.f1.x1 - f2.x1-(f1-f2).x2.| by A13,
VALUED_1:13
.= |.f1.x1 - f2.x1 - (f1.x2-f2.x2).| by A14,VALUED_1:13
.= |.f1.x1 - f1.x2 - (f2.x1-f2.x2).|;
then
A15: |.(f1-f2).x1-(f1-f2).x2.|<=|.f1.x1-f1.x2.|+|.f2.x1-f2.x2.| by
COMPLEX1:57;
dom(f2|(X /\ X1)) = dom f2 /\ (X /\ X1) by RELAT_1:61
.= dom f2 /\ X1 /\ X by XBOOLE_1:16
.= dom(f1-f2) by VALUED_1:12;
then
A16: |.f2.x1-f2.x2.|<=g*|.x1-x2.| by A12,A13,A14;
dom(f1|(X /\ X1)) = dom f1 /\ (X /\ X1) by RELAT_1:61
.= dom f1 /\ X /\ X1 by XBOOLE_1:16
.= dom(f1-f2) by VALUED_1:12;
then |.f1.x1-f1.x2.|<=s*|.x1-x2.| by A10,A13,A14;
then |.f1.x1-f1.x2.|+|.f2.x1-f2.x2.|<= s*|.x1-x2.|+g*|.x1-x2.| by A16
,XREAL_1:7;
hence |.(f1-f2).x1-(f1-f2).x2.|<=p*|.x1-x2.| by A15,XXREAL_0:2;
end;
hence thesis;
end;
end;
theorem
f1|X is Lipschitzian & f2|X1 is Lipschitzian implies (f1+f2)|(X /\ X1)
is Lipschitzian
proof
A1: f1|(X /\ X1) = f1|X|(X /\ X1) & f2|(X /\ X1) = f2|X1|(X /\ X1) by
RELAT_1:74,XBOOLE_1:17;
A2: (f1+f2)|(X /\ X1) = f1|(X /\ X1)+f2|(X /\ X1) by RFUNCT_1:44;
assume f1|X is Lipschitzian & f2|X1 is Lipschitzian;
hence thesis by A1,A2;
end;
theorem
f1|X is Lipschitzian & f2|X1 is Lipschitzian implies (f1-f2)|(X /\ X1)
is Lipschitzian
proof
A1: f1|(X /\ X1) = f1|X|(X /\ X1) & f2|(X /\ X1) = f2|X1|(X /\ X1) by
RELAT_1:74,XBOOLE_1:17;
A2: (f1-f2)|(X /\ X1) = f1|(X /\ X1)-f2|(X /\ X1) by RFUNCT_1:47;
assume f1|X is Lipschitzian & f2|X1 is Lipschitzian;
hence thesis by A1,A2;
end;
registration
let f1,f2 be bounded Lipschitzian PartFunc of REAL,REAL;
cluster f1 (#) f2 -> Lipschitzian for PartFunc of REAL,REAL;
coherence
proof
set X = dom f1, X1 = dom f2;
consider x1 such that
A1: for r be object st r in dom f1 holds |.f1.r.|<=x1 by RFUNCT_1:72;
consider x2 such that
A2: for r be object st r in dom f2 holds |.f2.r.|<=x2 by RFUNCT_1:72;
consider g such that
A3: 0<g and
A4: for x1,x2 st x1 in dom f2 & x2 in dom f2 holds |.f2.x1-f2.x2.|<=g
* |.x1-x2.| by Def3;
consider s such that
A5: 0<s and
A6: for x1,x2 st x1 in dom f1 & x2 in dom f1 holds |.f1.x1-f1.x2.|<=s
* |.x1-x2.| by Def3;
A7: now
let r;
assume r in dom(f1(#)f2);
then
A8: r in dom f1 /\ dom f2 by VALUED_1:def 4;
then r in dom f1 by XBOOLE_0:def 4;
then
A9: |.f1.r.|<=x1 by A1;
r in dom f2 by A8,XBOOLE_0:def 4;
then
A10: |.f2.r.|<=x2 by A2;
x1 <= |.x1.| by ABSVALUE:4;
hence |.f1.r.| <= |.x1.| by A9,XXREAL_0:2;
x2 <= |.x2.| by ABSVALUE:4;
hence |.f2.r.| <= |.x2.| by A10,XXREAL_0:2;
end;
now
take p = |.x1.|*g+|.x2.|*s+1;
A11: 0<=|.x1.| by COMPLEX1:46;
0<=|.x1.| & 0<=|.x2.| by COMPLEX1:46;
hence 0<p by A5,A3;
let y1,y2 be Real;
assume that
A12: y1 in dom(f1(#)f2) and
A13: y2 in dom(f1(#)f2);
A14: y2 in X /\ X1 by A13,VALUED_1:def 4;
then
A15: y2 in X by XBOOLE_0:def 4;
|.(f1.y1)*(f2.y1-f2.y2).|=|.f1.y1.|*|.f2.y1-f2.y2.| & 0 <=
|.f2.y1-f2. y2.| by COMPLEX1:46,65;
then
A16: |.(f1.y1)*(f2.y1-f2.y2).|<=|.x1.|*|.f2.y1-f2.y2.| by A7,A12,XREAL_1:64;
A17: y2 in X1 by A14,XBOOLE_0:def 4;
A18: y1 in X /\ X1 by A12,VALUED_1:def 4;
then y1 in X1 by XBOOLE_0:def 4;
then |.x1.|*|.f2.y1-f2.y2.|<=|.x1.|*(g*|.y1-y2.|) by A4,A17,A11,
XREAL_1:64;
then
A19: |.(f1.y1)*(f2.y1-f2.y2).|<=|.x1.|*g*|.y1-y2.| by A16,XXREAL_0:2;
0<=|.y1-y2.| by COMPLEX1:46;
then
A20: (|.x1.|*g+|.x2.|*s)*|.y1-y2.|+(0 qua Nat) <= (|.x1.|*g+|.x2.|*
s)*|.y1-y2.|+1*|.y1-y2.| by XREAL_1:7;
|.(f1(#)f2).y1-(f1(#)f2).y2.| = |.(f1.y1)*(f2.y1) - (f1(#) f2).
y2.| by VALUED_1:5
.= |.(f1.y1)*(f2.y1)+((f1.y1)*(f2.y2)-(f1.y1)*(f2.y2))-(f1.y2)*(f2
.y2).| by VALUED_1:5
.= |.(f1.y1)*((f2.y1)-(f2.y2))+((f1.y1)-(f1.y2))*(f2.y2).|;
then
A21: |.(f1(#)f2).y1-(f1(#)f2).y2.|<=|.(f1.y1)*((f2.y1)-(f2.y2)).| +
|.((f1.y1)-(f1.y2))*(f2.y2).| by COMPLEX1:56;
|.((f1.y1)-(f1.y2))*(f2.y2).|=|.f2.y2.|*|.(f1.y1)-(f1.y2).| & 0
<= |.f1 .y1-f1.y2.| by COMPLEX1:46,65;
then
A22: |.((f1.y1)-(f1.y2))*(f2.y2).|<=|.x2.|*|.f1.y1-f1.y2.| by A7,A13,
XREAL_1:64;
A23: 0<=|.x2.| by COMPLEX1:46;
y1 in X by A18,XBOOLE_0:def 4;
then |.x2.|*|.f1.y1-f1.y2.|<=|.x2.|*(s*|.y1-y2.|) by A6,A15,A23,
XREAL_1:64;
then |.((f1.y1)-(f1.y2))*(f2.y2).|<=|.x2.|*(s*|.y1-y2.|) by A22,
XXREAL_0:2;
then
|.(f1.y1)*(f2.y1-f2.y2).|+|.((f1.y1)-(f1.y2))*(f2.y2).| <= |.x1.|
*g*|.y1-y2.|+|.x2.|*s*|.y1-y2.| by A19,XREAL_1:7;
then |.(f1(#)f2).y1-(f1(#)f2).y2.|<= (|.x1.|*g+|.x2.|*s)*|.y1-y2.|
by A21,XXREAL_0:2;
hence |.(f1(#)f2).y1-(f1(#)f2).y2.|<=p*|.y1-y2.| by A20,XXREAL_0:2;
end;
hence thesis;
end;
end;
theorem
f1|X is Lipschitzian & f2|X1 is Lipschitzian & f1|Z is bounded & f2|Z1
is bounded implies (f1(#)f2)|(X /\ Z /\ X1 /\ Z1) is Lipschitzian
proof
A1: f1|(X /\ Z /\ X1 /\ Z1) = f1|(X1 /\ Z1 /\ (X /\ Z)) by XBOOLE_1:16
.= f1|(X1 /\ Z1 /\ X /\ Z) by XBOOLE_1:16
.= f1|Z|(X1 /\ Z1 /\ X) by RELAT_1:71;
A2: f1|(X /\ Z /\ X1 /\ Z1) = f1|(X1 /\ Z1 /\ (X /\ Z)) by XBOOLE_1:16
.= f1|(X1 /\ Z1 /\ Z /\ X) by XBOOLE_1:16
.= f1|X|(X1 /\ Z1 /\ Z) by RELAT_1:71;
A3: f2|(X /\ Z /\ X1 /\ Z1) = f2|(X /\ Z /\ Z1 /\ X1) by XBOOLE_1:16
.= f2|X1|(Z /\ X /\ Z1) by RELAT_1:71;
A4: (f1(#)f2)|(X /\ Z /\ X1 /\ Z1) = f1|(X /\ Z /\ X1 /\ Z1)(#)f2|(X /\ Z /\
X1 /\ Z1) & f2|(X /\ Z /\ X1 /\ Z1) = f2|Z1|(X /\ Z /\ X1) by RELAT_1:71
,RFUNCT_1:45;
assume f1|X is Lipschitzian & f2|X1 is Lipschitzian & f1|Z is bounded & f2|
Z1 is bounded;
hence thesis by A1,A2,A4,A3;
end;
registration
let f be Lipschitzian PartFunc of REAL, REAL;
let p;
cluster p(#)f -> Lipschitzian for PartFunc of REAL, REAL;
coherence
proof
consider s such that
A1: 0<s and
A2: for x1,x2 st x1 in dom f & x2 in dom f holds |.f.x1-f.x2.|<=s*|.x1-x2.|
by Def3;
per cases;
suppose
A3: p=0;
now
take s;
thus 0<s by A1;
let x1,x2;
assume that
A4: x1 in dom(p(#)f) and
A5: x2 in dom(p(#)f);
A6: 0<=|.x1-x2.| by COMPLEX1:46;
|.(p(#)f).x1-(p(#)f).x2.| = |.p*(f.x1)-(p(#)f).x2.| by A4,
VALUED_1:def 5
.= |.0 qua Nat - p*(f.x2).| by A3,A5,VALUED_1:def 5
.= 0 by A3,ABSVALUE:2;
hence |.(p(#)f).x1-(p(#)f).x2.|<=s*|.x1-x2.| by A1,A6;
end;
hence thesis;
end;
suppose
p<>0;
then 0<|.p.| by COMPLEX1:47;
then
A7: 0*s<|.p.|*s by A1,XREAL_1:68;
now
take g = |.p.|*s;
A8: 0<=|.p.| by COMPLEX1:46;
thus 0<g by A7;
let x1,x2;
assume that
A9: x1 in dom(p(#)f) and
A10: x2 in dom(p(#)f);
A11: |.(p(#)f).x1-(p(#)f).x2.| = |.p*(f.x1)-(p(#)f).x2.| by A9,
VALUED_1:def 5
.= |.p*(f.x1) - p*(f.x2).| by A10,VALUED_1:def 5
.= |.p*(f.x1 - f.x2).|
.= |.p.|*|.f.x1 - f.x2.| by COMPLEX1:65;
x1 in dom f & x2 in dom f by A9,A10,VALUED_1:def 5;
then |.p.|*|.f.x1-f.x2.|<=|.p.|*(s*|.x1-x2.|) by A2,A8,XREAL_1:64;
hence |.(p(#)f).x1-(p(#)f).x2.|<=g*|.x1-x2.| by A11;
end;
hence thesis;
end;
end;
end;
theorem
f|X is Lipschitzian & X c= dom f implies (p(#)f)|X is Lipschitzian
proof
(p(#)f)|X = p(#)(f|X) by RFUNCT_1:49;
hence thesis;
end;
registration
let f be Lipschitzian PartFunc of REAL, REAL;
cluster abs f -> Lipschitzian for PartFunc of REAL, REAL;
coherence
proof
consider s such that
A1: 0<s and
A2: for x1,x2 st x1 in dom f & x2 in dom f holds |.f.x1-f.x2.|<=s*
|.x1-x2.| by Def3;
now
take s;
thus 0<s by A1;
let x1,x2;
assume x1 in dom abs f & x2 in dom abs f;
then x1 in dom f & x2 in dom f by VALUED_1:def 11;
then
A3: |.f.x1-f.x2.|<=s*|.x1-x2.| by A2;
|.(abs(f)).x1-(abs(f)).x2.| = |.|.f.x1.|-(abs(f)).x2.| by VALUED_1:18
.= |.|.f.x1.|-|.f.x2.|.| by VALUED_1:18;
then |.(abs f).x1-(abs(f)).x2.| <= |.f.x1-f.x2.| by COMPLEX1:64;
hence |.(abs f).x1-(abs f).x2.|<=s*|.x1-x2.| by A3,XXREAL_0:2;
end;
hence thesis;
end;
end;
theorem
f|X is Lipschitzian implies -f|X is Lipschitzian & (abs f)|X is Lipschitzian
proof
assume
A1: f|X is Lipschitzian;
hence -f|X is Lipschitzian;
(abs f)|X = abs(f|X) by RFUNCT_1:46;
hence thesis by A1;
end;
registration
cluster constant -> Lipschitzian for PartFunc of REAL, REAL;
coherence
proof
let f be PartFunc of REAL, REAL such that
A1: f is constant;
now
let x1,x2;
assume x1 in dom f & x2 in dom f;
then f.x1 = f.x2 by A1;
then |.f.x1-f.x2.| = 0 by ABSVALUE:2;
hence |.f.x1-f.x2.| <= 1*|.x1-x2.| by COMPLEX1:46;
end;
hence thesis;
end;
end;
registration
let Y;
cluster id Y -> Lipschitzian for PartFunc of REAL,REAL;
coherence
proof
reconsider r=1 as Real;
id Y is Lipschitzian
proof
take r;
thus r>0;
let x1,x2;
assume that
A1: x1 in dom id Y and
A2: x2 in dom id Y;
A3: x2 in Y by A2;
x1 in Y by A1;
then |.(id Y).x1-(id Y).x2.| = |.x1-(id Y).x2.| by FUNCT_1:18
.= r*|.x1-x2.| by A3,FUNCT_1:18;
hence thesis;
end;
hence thesis;
end;
end;
registration
::$N Lipschitz continuity
cluster Lipschitzian -> continuous for PartFunc of REAL, REAL;
coherence
proof
let f be PartFunc of REAL, REAL;
set X = dom f;
assume f is Lipschitzian;
then consider r such that
A1: 0<r and
A2: for x1,x2 st x1 in X & x2 in X holds |.f.x1-f.x2.|<=r*|.x1-x2.|;
now
let x0 such that
A3: x0 in X;
for r st 0<r ex s st 0<s & for x1 st x1 in dom f & |.x1-x0.|<s
holds |.f.x1-f.x0.|<r
proof
let g such that
A4: 0<g;
set s=g/r;
take s9=s;
A5: now
let x1;
assume that
A6: x1 in dom f and
A7: |.x1-x0.|<s;
r*|.x1-x0.|<(g/r)*r by A1,A7,XREAL_1:68;
then
A8: r*|.x1-x0.|<g by A1,XCMPLX_1:87;
|.f.x1-f.x0.|<=r*|.x1-x0.| by A2,A3,A6;
hence |.f.x1-f.x0.|<g by A8,XXREAL_0:2;
end;
s9=g*r" by XCMPLX_0:def 9;
hence thesis by A1,A4,A5,XREAL_1:129;
end;
hence f is_continuous_in x0 by Th3;
end;
hence thesis;
end;
end;
theorem
for f st (ex r st rng f = {r}) holds f is continuous
proof
let f;
given r such that
A1: rng f = {r};
now
let x1,x2;
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
A4: f.x2=r by A1,TARSKI:def 1;
f.x1 in rng f by A2,FUNCT_1:def 3;
then f.x1=r by A1,TARSKI:def 1;
then |.f.x1-f.x2.| = 0 by A4,ABSVALUE:2;
hence |.f.x1-f.x2.| <= 1*|.x1-x2.| by COMPLEX1:46;
end;
then f is Lipschitzian;
hence thesis;
end;
theorem
for f st (for x0 st x0 in dom f holds f.x0 = x0) holds f is continuous
proof
let f such that
A1: for x0 st x0 in dom f holds f.x0 = x0;
now
let x1,x2;
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;
hence thesis;
end;
theorem Th41:
(for x0 st x0 in X holds f.x0 = r*x0+p) implies f|X is continuous
proof
assume
A1: for x0 st x0 in X holds f.x0 = r*x0+p;
A2: now
let x1,x2;
assume that
A3: x1 in dom(f|X) and
A4: x2 in dom(f|X);
x2 in X by A4;
then
A5: f.x2 = r*x2+p by A1;
A6: 0<=|.x1-x2.| by COMPLEX1:46;
x1 in X by A3;
then f.x1 = r*x1+p by A1;
then |.f.x1-f.x2.| = |.r*(x1-x2).| by A5
.= |.r.|*|.x1-x2.| by COMPLEX1:65;
then |.f.x1-f.x2.| + (0 qua Nat) <= |.r.|*|.x1-x2.| + 1*|.x1-x2.| by A6
,XREAL_1:7;
hence |.f.x1-f.x2.| <= (|.r.|+1)*|.x1-x2.|;
end;
(0 qua Nat)+(0 qua Nat)<|.r.|+1 by COMPLEX1:46,XREAL_1:8;
then f|X is Lipschitzian by A2,Th32;
hence thesis;
end;
theorem Th42:
(for x0 st x0 in dom f holds f.x0 = x0^2) implies f|dom f is continuous
proof
reconsider f1 = id dom f as PartFunc of REAL,REAL;
assume
A1: for x0 st x0 in dom f holds f.x0 = x0^2;
A2: now
let x0 be object;
assume
A3: x0 in dom f;
then reconsider x1 = x0 as Real;
thus f.x0 = x1^2 by A1,A3
.= f1.x1*x1 by A3,FUNCT_1:18
.= f1.x0*f1.x0 by A3,FUNCT_1:18;
end;
dom f1 /\ dom f1 = dom f;
then f = f1(#)f1 by A2,VALUED_1:def 4;
hence thesis;
end;
theorem
X c= dom f & (for x0 st x0 in X holds f.x0 = x0^2) implies f|X is continuous
proof
assume that
A1: X c= dom f and
A2: for x0 st x0 in X holds f.x0=x0^2;
X=dom f /\ X by A1,XBOOLE_1:28;
then
A3: X=dom(f|X) by RELAT_1:61;
now
let x0;
assume
A4: x0 in dom(f|X);
then f.x0=x0^2 by A2;
hence (f|X).x0=x0^2 by A4,FUNCT_1:47;
end;
then f|X|X is continuous by A3,Th42;
hence thesis;
end;
theorem Th44:
(for x0 st x0 in dom f holds f.x0 = |.x0.|) implies f is continuous
proof
assume
A1: for x0 st x0 in dom f holds f.x0 = |.x0.|;
now
let x1,x2;
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 COMPLEX1:64;
end;
then f is Lipschitzian;
hence thesis;
end;
theorem
(for x0 st x0 in X holds f.x0 = |.x0.|) implies f|X is continuous
proof
assume that
A1: for x0 st x0 in X holds f.x0 = |.x0.|;
now
let x0;
assume
A2: x0 in dom(f|X);
then f.x0=|.x0.| by A1;
hence (f|X).x0=|.x0.| by A2,FUNCT_1:47;
end;
hence thesis by Th44;
end;
theorem Th46:
f|X is monotone & (ex p,g st p<=g & f.:X=[.p,g.]) implies f|X is continuous
proof
assume
A1: f|X is monotone;
given p,g such that
A2: p<=g and
A3: f.:X=[.p,g.];
reconsider p, g as Real;
now
per cases by A2,XXREAL_0:1;
suppose
p=g;
then f.:X = {p} by A3,XXREAL_1:17;
then rng (f|X)= {p} by RELAT_1:115;
then f|X is constant;
hence thesis;
end;
suppose
A4: p<g;
now
per cases by A1,RFUNCT_2:def 5;
suppose
f|X is non-decreasing;
then
A5: f|X|X is non-decreasing;
for x0 st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
A6: [.p,g.] = ].p,g.[ \/ {p,g} by A2,XXREAL_1:128;
let x0;
A7: (f|X).:X = f.:X by RELAT_1:129;
assume
A8: x0 in dom(f|X);
A9: (f|X).x0 in (f|X).:X by A8,FUNCT_1:def 6;
reconsider x0 as Real;
(f|X).x0 in [.p,g.] by A3,A9,RELAT_1:129;
then
A10: (f|X).x0 in ].p,g.[ or (f|X).x0 in {p,g} by A6,XBOOLE_0:def 3;
now
let N1 be Neighbourhood of (f|X).x0;
now
per cases by A10,TARSKI:def 2;
suppose
(f|X).x0 in ].p,g.[;
then consider N2 being Neighbourhood of (f|X).x0 such that
A11: N2 c= ].p,g.[ by RCOMP_1:18;
A12: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider N3 being Neighbourhood of (f|X).x0 such that
A13: N3 c= N1 and
A14: N3 c= N2 by RCOMP_1:17;
consider r such that
A15: r>0 and
A16: N3 = ].(f|X).x0-r,(f|X).x0+r.[ by RCOMP_1:def 6;
reconsider r as Real;
A17: (f|X).x0+r/2 < (f|X).x0+r/2+r/2 by A15,XREAL_1:29,215;
set M2 = (f|X).x0+r/2;
A18: (f|X).x0 < (f|X).x0+r/2 by A15,XREAL_1:29,215;
A19: (f|X).x0 < (f|X).x0+r by A15,XREAL_1:29;
then (f|X).x0-r < (f|X).x0+r-r by XREAL_1:9;
then (f|X).x0-r < (f|X).x0+r/2 by A18,XXREAL_0:2;
then
(f|X).x0+r/2 in {s: (f|X).x0-r<s & s<(f
|X).x0+r} by A17;
then
A20: M2 in ].(f|X).x0-r,(f|X).x0+r.[ by RCOMP_1:def 2;
then M2 in N2 by A14,A16;
then M2 in ].p,g.[ by A11;
then consider x2 be Element of REAL such that
A21: x2 in dom (f|X) & x2 in X and
A22: M2=(f|X).x2 by A3,A7,A12,PARTFUN2:59;
A23: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
set M1 = (f|X).x0-r/2;
A24: (f|X).x0-r < (f|X).x0-r + r/2 by A15,XREAL_1:29,215;
(f|X).x0-r/2 < (f|X).x0 by A18,XREAL_1:19;
then (f|X).x0-r/2 < (f|X).x0+r by A19,XXREAL_0:2;
then
(f|X).x0-r/2 in {s: (f|X).x0-r<s & s<(f
|X).x0+r} by A24;
then
A25: M1 in ].(f|X).x0-r,(f|X).x0+r.[ by RCOMP_1:def 2;
then M1 in N2 by A14,A16;
then M1 in ].p,g.[ by A11;
then consider x1 be Element of REAL such that
A26: x1 in dom (f|X) & x1 in X and
A27: M1=(f|X).x1 by A3,A7,A23,PARTFUN2:59;
A28: (f|X).x0 < (f|X).x0 + r/2 by A15,XREAL_1:29,215;
then
A29: M1<(f|X).x0 by XREAL_1:19;
A30: now
assume
A31: x0<x1;
x0 in X /\ dom(f|X) & x1 in X /\ dom(f|X) by A8,A26,
XBOOLE_0:def 4;
hence contradiction by A5,A27,A29,A31,RFUNCT_2:22;
end;
A32: M2>(f|X).x0 by A15,XREAL_1:29,215;
A33: now
assume
A34: x2<x0;
x0 in X /\ dom(f|X) & x2 in X /\ dom(f|X) by A8,A21,
XBOOLE_0:def 4;
hence contradiction by A5,A22,A32,A34,RFUNCT_2:22;
end;
x0<>x2 by A15,A22,XREAL_1:29,215;
then x0<x2 by A33,XXREAL_0:1;
then
A35: x2-x0>0 by XREAL_1:50;
set R = min(x0-x1,x2-x0);
A36: R<=x2-x0 by XXREAL_0:17;
x1<>x0 by A27,A28,XREAL_1:19;
then x1<x0 by A30,XXREAL_0:1;
then x0-x1>0 by XREAL_1:50;
then R>0 by A35,XXREAL_0:15;
then reconsider N=].x0-R,x0+R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A37: x in dom(f|X) and
A38: x in N;
A39: x in X /\ dom(f|X) by A37,XBOOLE_1:28;
x in {s :x0-R<s & s<x0+R} by A38,RCOMP_1:def 2;
then
A40: ex s st s=x & x0-R<s & s<x0+R;
then x0<R+x by XREAL_1:19;
then
A41: x0-x<R+x-x by XREAL_1:9;
R<=x0- x1 by XXREAL_0:17;
then x0-x<x0-x1 by A41,XXREAL_0:2;
then -(x0-x)>-(x0-x1) by XREAL_1:24;
then
A42: x-x0+x0>x1-x0+x0 by XREAL_1:6;
x1 in X /\ dom(f|X) by A26,XBOOLE_0:def 4;
then
A43: (f|X).x1 <= (f|X).x by A5,A42,A39,RFUNCT_2:22;
x-x0<R by A40,XREAL_1:19;
then x-x0<x2-x0 by A36,XXREAL_0:2;
then
A44: x-x0+x0<x2-x0+x0 by XREAL_1:6;
x2 in X /\ dom(f|X) by A21,XBOOLE_0:def 4;
then (f|X).x <= (f|X).x2 by A5,A44,A39,RFUNCT_2:22;
then (f|X).x in {s : M1<=s & s<=M2} by A27,A22
,A43;
then
A45: (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
[.M1,M2.] c= ].(f|X).x0-r,(f|X).x0+r.[ by A25,A20,
XXREAL_2:def 12;
then (f|X).x in N3 by A16,A45;
hence (f|X).x in N1 by A13;
end;
suppose
A46: (f|X).x0 = p;
then consider r such that
A47: r>0 and
A48: N1 = ].p-r,p+r.[ by RCOMP_1:def 6;
reconsider r as Real;
set R=min(r,g-p)/2;
g-p>0 by A4,XREAL_1:50;
then
A49: min(r,g-p)>0 by A47,XXREAL_0:15;
then
A50: R<min(r,g-p) by XREAL_1:216;
min(r,g-p) <= r by XXREAL_0:17;
then
A51: R<r by A50,XXREAL_0:2;
then
A52: p+R<p+r by XREAL_1:6;
A53: p-R<p by A49,XREAL_1:44,215;
-r<-R by A51,XREAL_1:24;
then
A54: p+-r<p+-R by XREAL_1:6;
p<p+r by A47,XREAL_1:29;
then p-R<p+r by A53,XXREAL_0:2;
then p-R in {s : p-r<s & s<p+r} by A54;
then
A55: p-R in ].p-r,p+r.[ by RCOMP_1:def 2;
A56: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
A57: p<p+R by A49,XREAL_1:29,215;
min(r,g-p) <= g-p by XXREAL_0:17;
then R<g-p by A50,XXREAL_0:2;
then p+R<g by XREAL_1:20;
then p+R in {s : p<s & s<g} by A57;
then p+R in ].p,g.[ by RCOMP_1:def 2;
then consider x1 be Element of REAL such that
A58: x1 in dom (f|X) & x1 in X and
A59: p+R=(f|X).x1 by A3,A7,A56,PARTFUN2:59;
A60: x1 in X /\ dom(f|X) by A58,XBOOLE_0:def 4;
now
assume
A61: x1<x0;
x0 in X /\ dom(f|X) & x1 in X /\ dom(f|X) by A8,A58,
XBOOLE_0:def 4;
hence contradiction by A5,A46,A57,A59,A61,RFUNCT_2:22;
end;
then x0<x1 by A46,A57,A59,XXREAL_0:1;
then reconsider
N=].x0-(x1-x0),x0+(x1-x0).[ as Neighbourhood of
x0 by RCOMP_1:def 6,XREAL_1:50;
take N;
let x be Real such that
A62: x in dom(f|X) and
A63: x in N;
x in {s : x0-(x1-x0)<s & s<x0+(x1-x0)}
by A63,RCOMP_1:def 2;
then
A64: ex s st s=x & x0-(x1-x0)<s & s<x0+(x1-x0);
(f|X).x in [.p,g.] by A3,A7,A62,FUNCT_1:def 6;
then (f|X).x in {s : p<=s & s<=g} by
RCOMP_1:def 1;
then ex s st s=(f|X).x & p<=s & s<=g;
then
A65: p-R<=(f|X).x by A53,XXREAL_0:2;
x in X /\ dom(f|X) by A62,XBOOLE_0:def 4;
then (f|X).x<=p+R by A5,A59,A60,A64,RFUNCT_2:22;
then (f|X).x in {s : p-R<=s & s<= p+R} by A65;
then
A66: (f|X).x in [.p-R,p+R.] by RCOMP_1:def 1;
p-r<p by A47,XREAL_1:44;
then p-r<p+R by A57,XXREAL_0:2;
then p+R in {s : p-r<s & s<p+r} by A52;
then p+R in ].p-r,p+r.[ by RCOMP_1:def 2;
then [.p-R,p+R.] c= N1 by A48,A55,XXREAL_2:def 12;
hence (f|X).x in N1 by A66;
end;
suppose
A67: (f|X).x0 = g;
A68: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider r such that
A69: r>0 and
A70: N1 = ].g-r,g+r.[ by A67,RCOMP_1:def 6;
reconsider r as Real;
set R=min(r,g-p)/2;
g-p>0 by A4,XREAL_1:50;
then
A71: min(r,g-p)>0 by A69,XXREAL_0:15;
then
A72: R<min(r,g-p) by XREAL_1:216;
A73: g-R<g by A71,XREAL_1:44,215;
min(r,g-p) <= g-p by XXREAL_0:17;
then R<g-p by A72,XXREAL_0:2;
then R+p<g by XREAL_1:20;
then g-R>p by XREAL_1:20;
then g-R in {s : p<s & s<g} by A73;
then g-R in ].p,g.[ by RCOMP_1:def 2;
then consider x1 being Element of REAL such that
A74: x1 in dom (f|X) & x1 in X and
A75: g-R=(f|X).x1 by A3,A7,A68,PARTFUN2:59;
A76: now
assume
A77: x0<x1;
x0 in X /\ dom(f|X) & x1 in X /\ dom(f|X) by A8,A74,
XBOOLE_0:def 4;
hence contradiction by A5,A67,A73,A75,A77,RFUNCT_2:22;
end;
min(r,g-p) <= r by XXREAL_0:17;
then
A78: R<r by A72,XXREAL_0:2;
then
A79: g+R<g+r by XREAL_1:6;
-r<-R by A78,XREAL_1:24;
then
A80: g+-r<g+-R by XREAL_1:6;
g<g+r by A69,XREAL_1:29;
then g-R<g+r by A73,XXREAL_0:2;
then g-R in {s : g-r<s & s<g+r} by A80;
then
A81: g-R in ].g-r,g+r.[ by RCOMP_1:def 2;
A82: x1 in X /\ dom(f|X) by A74,XBOOLE_0:def 4;
A83: g<g+R by A71,XREAL_1:29,215;
x1<>x0 by A67,A71,A75,XREAL_1:44,215;
then x1<x0 by A76,XXREAL_0:1;
then reconsider
N=].x0-(x0-x1),x0+(x0-x1).[ as Neighbourhood of
x0 by RCOMP_1:def 6,XREAL_1:50;
take N;
let x be Real such that
A84: x in dom(f|X) and
A85: x in N;
x in {s : x0-(x0-x1)<s & s<x0+(x0-x1)}
by A85,RCOMP_1:def 2;
then
A86: ex s st s=x & x0-(x0-x1)<s & s<x0+(x0-x1);
(f|X).x in [.p,g.] by A3,A7,A84,FUNCT_1:def 6;
then (f|X).x in {s : p<=s & s<=g} by
RCOMP_1:def 1;
then ex s st s=(f|X).x & p<=s & s<=g;
then
A87: (f|X).x<=g+R by A83,XXREAL_0:2;
x in X /\ dom(f|X) by A84,XBOOLE_0:def 4;
then g-R<=(f|X).x by A5,A75,A82,A86,RFUNCT_2:22;
then (f|X).x in {s : g-R<=s & s<= g+R} by A87;
then
A88: ( f|X).x in [.g-R,g+R.] by RCOMP_1:def 1;
g-r<g by A69,XREAL_1:44;
then g-r<g+R by A83,XXREAL_0:2;
then g+R in {s : g-r<s & s<g+r} by A79;
then g+R in ].g-r,g+r.[ by RCOMP_1:def 2;
then [.g-R,g+R.] c= N1 by A70,A81,XXREAL_2:def 12;
hence (f|X).x in N1 by A88;
end;
end;
then consider N being Neighbourhood of x0 such that
A89: for x1 being Real st x1 in dom(f|X) & x1 in N holds (f|X) .x1 in N1;
take N;
thus for x1 be Real st x1 in dom(f|X) & x1 in N holds (f|
X).x1 in N1 by A89;
end;
hence thesis by Th4;
end;
hence thesis;
end;
suppose
f|X is non-increasing;
then
A90: f|X|X is non-increasing;
for x0 st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
A91: [.p,g.] = ].p,g.[ \/ {p,g} by A2,XXREAL_1:128;
let x0;
A92: (f|X).:X = f.:X by RELAT_1:129;
assume
A93: x0 in dom(f|X);
A94: (f|X).x0 in (f|X).:X by A93,FUNCT_1:def 6;
reconsider x0 as Real;
(f|X).x0 in [.p,g.] by A3,A94,RELAT_1:129;
then
A95: (f|X).x0 in ].p,g.[ or (f|X).x0 in {p,g} by A91,XBOOLE_0:def 3;
now
let N1 be Neighbourhood of (f|X).x0;
now
per cases by A95,TARSKI:def 2;
suppose
(f|X).x0 in ].p,g.[;
then consider N2 being Neighbourhood of (f|X).x0 such that
A96: N2 c= ].p,g.[ by RCOMP_1:18;
A97: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider N3 being Neighbourhood of (f|X).x0 such that
A98: N3 c= N1 and
A99: N3 c= N2 by RCOMP_1:17;
consider r such that
A100: r>0 and
A101: N3 = ].(f|X).x0-r,(f|X).x0+r.[ by RCOMP_1:def 6;
reconsider r as Real;
A102: (f|X).x0+r/2 < (f|X).x0+r/2+r/2 by A100,XREAL_1:29,215;
set M2 = (f|X).x0+r/2;
A103: (f|X).x0 < (f|X).x0+r/2 by A100,XREAL_1:29,215;
A104: (f|X).x0 < (f|X).x0+r by A100,XREAL_1:29;
then (f|X).x0-r < (f|X).x0+r-r by XREAL_1:9;
then (f|X).x0-r < (f|X).x0+r/2 by A103,XXREAL_0:2;
then (f|X).x0+r/2 in {s : (f|X).x0-r<s & s<(
f|X).x0+r} by A102;
then
A105: M2 in ].(f|X).x0-r,(f|X).x0+r.[ by RCOMP_1:def 2;
then M2 in N2 by A99,A101;
then M2 in ].p,g.[ by A96;
then consider x2 being Element of REAL such that
A106: x2 in dom (f|X) & x2 in X and
A107: M2=(f|X).x2 by A3,A92,A97,PARTFUN2:59;
A108: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
set M1 = (f|X).x0-r/2;
A109: (f|X).x0-r < (f|X).x0-r + r/2 by A100,XREAL_1:29,215;
(f|X).x0-r/2 < (f|X).x0 by A103,XREAL_1:19;
then (f|X).x0-r/2 < (f|X).x0+r by A104,XXREAL_0:2;
then (f|X).x0-r/2 in {s : (f|X).x0-r<s & s<(
f|X).x0+r} by A109;
then
A110: M1 in ].(f|X).x0-r,(f|X).x0+r.[ by RCOMP_1:def 2;
then M1 in N2 by A99,A101;
then M1 in ].p,g.[ by A96;
then consider x1 being Element of REAL such that
A111: x1 in dom (f|X) & x1 in X and
A112: M1=(f|X).x1 by A3,A92,A108,PARTFUN2:59;
A113: (f|X).x0 < (f|X).x0 + r/2 by A100,XREAL_1:29,215;
then
A114: M1<(f|X).x0 by XREAL_1:19;
A115: now
assume
A116: x0>x1;
x0 in X /\ dom(f|X) & x1 in X /\ dom(f|X) by A93,A111,
XBOOLE_0:def 4;
hence contradiction by A90,A112,A114,A116,RFUNCT_2:23;
end;
A117: M2>(f|X).x0 by A100,XREAL_1:29,215;
A118: now
assume
A119: x2>x0;
x0 in X /\ dom(f|X) & x2 in X /\ dom(f|X) by A93,A106,
XBOOLE_0:def 4;
hence contradiction by A90,A107,A117,A119,RFUNCT_2:23;
end;
x0<>x2 by A100,A107,XREAL_1:29,215;
then x0>x2 by A118,XXREAL_0:1;
then
A120: x0-x2>0 by XREAL_1:50;
set R = min(x1-x0,x0-x2);
A121: R<=x1-x0 by XXREAL_0:17;
x1<>x0 by A112,A113,XREAL_1:19;
then x1>x0 by A115,XXREAL_0:1;
then x1-x0>0 by XREAL_1:50;
then R>0 by A120,XXREAL_0:15;
then reconsider N=].x0-R,x0+R.[ as Neighbourhood of x0 by
RCOMP_1:def 6;
take N;
let x be Real;
assume that
A122: x in dom(f|X) and
A123: x in N;
A124: x in X /\ dom(f|X) by A122,XBOOLE_1:28;
x in {s :x0-R<s & s<x0+R} by A123,
RCOMP_1:def 2;
then
A125: ex s st s=x & x0-R<s & s<x0+R;
then x0<R+x by XREAL_1:19;
then
A126: x0-x<R+x-x by XREAL_1:9;
x-x0<R by A125,XREAL_1:19;
then x-x0<x1-x0 by A121,XXREAL_0:2;
then
A127: x-x0+x0<x1-x0+x0 by XREAL_1:6;
x1 in X /\ dom(f|X) by A111,XBOOLE_0:def 4;
then
A128: (f|X).x1 <= (f|X).x by A90,A127,A124,RFUNCT_2:23;
R<=x0- x2 by XXREAL_0:17;
then x0-x<x0-x2 by A126,XXREAL_0:2;
then -(x0-x)>-(x0-x2) by XREAL_1:24;
then
A129: x-x0+x0>x2-x0+x0 by XREAL_1:6;
x2 in X /\ dom(f|X) by A106,XBOOLE_0:def 4;
then (f|X).x <= (f|X).x2 by A90,A129,A124,RFUNCT_2:23;
then (f|X).x in {s : M1<=s & s<=M2} by A112
,A107,A128;
then
A130: (f|X).x in [.M1,M2.] by RCOMP_1:def 1;
[.M1,M2.] c= ].(f|X).x0-r,(f|X).x0+r.[ by A110,A105,
XXREAL_2:def 12;
then (f|X).x in N3 by A101,A130;
hence (f|X).x in N1 by A98;
end;
suppose
A131: (f|X).x0 = p;
then consider r such that
A132: r>0 and
A133: N1 = ].p-r,p+r.[ by RCOMP_1:def 6;
reconsider r as Real;
set R=min(r,g-p)/2;
g-p>0 by A4,XREAL_1:50;
then
A134: min(r,g-p)>0 by A132,XXREAL_0:15;
then
A135: R<min(r,g-p) by XREAL_1:216;
min(r,g-p) <= r by XXREAL_0:17;
then
A136: R<r by A135,XXREAL_0:2;
then
A137: p+R<p+r by XREAL_1:6;
A138: p-R<p by A134,XREAL_1:44,215;
-r<-R by A136,XREAL_1:24;
then
A139: p+-r<p+-R by XREAL_1:6;
p<p+r by A132,XREAL_1:29;
then p-R<p+r by A138,XXREAL_0:2;
then p-R in {s : p-r<s & s<p+r} by A139;
then
A140: p-R in ].p-r,p+r.[ by RCOMP_1:def 2;
A141: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
A142: p<p+R by A134,XREAL_1:29,215;
min(r,g-p) <= g-p by XXREAL_0:17;
then R<g-p by A135,XXREAL_0:2;
then p+R<g by XREAL_1:20;
then p+R in {s : p<s & s<g} by A142;
then p+R in ].p,g.[ by RCOMP_1:def 2;
then consider x1 being Element of REAL such that
A143: x1 in dom (f|X) & x1 in X and
A144: p+R=(f|X).x1 by A3,A92,A141,PARTFUN2:59;
A145: x1 in X /\ dom(f|X) by A143,XBOOLE_0:def 4;
now
assume
A146: x1>x0;
x0 in X /\ dom(f|X) & x1 in X /\ dom(f|X) by A93,A143,
XBOOLE_0:def 4;
hence contradiction by A90,A131,A142,A144,A146,RFUNCT_2:23;
end;
then x0>x1 by A131,A142,A144,XXREAL_0:1;
then reconsider
N=].x0-(x0-x1),x0+(x0-x1).[ as Neighbourhood of
x0 by RCOMP_1:def 6,XREAL_1:50;
take N;
let x be Real such that
A147: x in dom(f|X) and
A148: x in N;
x in {s : x0-(x0-x1)<s & s<x0+(x0-x1)}
by A148,RCOMP_1:def 2;
then
A149: ex s st s=x & x0-(x0-x1)<s & s<x0+(x0-x1);
(f|X).x in [.p,g.] by A3,A92,A147,FUNCT_1:def 6;
then (f|X).x in {s : p<=s & s<=g} by
RCOMP_1:def 1;
then ex s st s=(f|X).x & p<=s & s<=g;
then
A150: p-R<=(f|X).x by A138,XXREAL_0:2;
x in X /\ dom(f|X) by A147,XBOOLE_0:def 4;
then (f|X).x<=p+ R by A90,A144,A145,A149,RFUNCT_2:23;
then (f|X).x in {s : p-R<=s & s<=p+R} by A150;
then
A151: (f|X).x in [.p-R,p+R.] by RCOMP_1:def 1;
p-r<p by A132,XREAL_1:44;
then p-r<p+R by A142,XXREAL_0:2;
then p+R in {s : p-r<s & s<p+r} by A137;
then p+R in ].p-r,p+r.[ by RCOMP_1:def 2;
then [.p-R,p+R.] c= N1 by A133,A140,XXREAL_2:def 12;
hence (f|X).x in N1 by A151;
end;
suppose
A152: (f|X).x0 = g;
A153: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
consider r such that
A154: r>0 and
A155: N1 = ].g-r,g+r.[ by A152,RCOMP_1:def 6;
reconsider r as Real;
set R=min(r,g-p)/2;
g-p>0 by A4,XREAL_1:50;
then
A156: min(r,g-p)>0 by A154,XXREAL_0:15;
then
A157: R<min(r,g-p) by XREAL_1:216;
A158: g-R<g by A156,XREAL_1:44,215;
min(r,g-p) <= g-p by XXREAL_0:17;
then R<g-p by A157,XXREAL_0:2;
then R+p<g by XREAL_1:20;
then g-R>p by XREAL_1:20;
then g-R in {s : p<s & s<g} by A158;
then g-R in ].p,g.[ by RCOMP_1:def 2;
then consider x1 being Element of REAL such that
A159: x1 in dom (f|X) & x1 in X and
A160: g-R=(f|X).x1 by A3,A92,A153,PARTFUN2:59;
A161: now
assume
A162: x0>x1;
x0 in X /\ dom(f|X) & x1 in X /\ dom(f|X) by A93,A159,
XBOOLE_0:def 4;
hence contradiction by A90,A152,A158,A160,A162,RFUNCT_2:23;
end;
min(r,g-p) <= r by XXREAL_0:17;
then
A163: R<r by A157,XXREAL_0:2;
then
A164: g+R<g+r by XREAL_1:6;
-r<-R by A163,XREAL_1:24;
then
A165: g+-r<g+-R by XREAL_1:6;
g<g+r by A154,XREAL_1:29;
then g-R<g+r by A158,XXREAL_0:2;
then g-R in {s : g-r<s & s<g+r} by A165;
then
A166: g-R in ].g-r,g+r.[ by RCOMP_1:def 2;
A167: x1 in X /\ dom(f|X) by A159,XBOOLE_0:def 4;
A168: g<g+R by A156,XREAL_1:29,215;
x1<>x0 by A152,A156,A160,XREAL_1:44,215;
then x1>x0 by A161,XXREAL_0:1;
then reconsider
N=].x0-(x1-x0),x0+(x1-x0).[ as Neighbourhood of
x0 by RCOMP_1:def 6,XREAL_1:50;
take N;
let x be Real such that
A169: x in dom(f|X) and
A170: x in N;
x in {s : x0-(x1-x0)<s & s<x0+(x1-x0)}
by A170,RCOMP_1:def 2;
then
A171: ex s st s=x & x0-(x1-x0)<s & s<x0+(x1-x0);
(f|X).x in [.p,g.] by A3,A92,A169,FUNCT_1:def 6;
then (f|X).x in {s : p<=s & s<=g} by
RCOMP_1:def 1;
then ex s st s=(f|X).x & p<=s & s<=g;
then
A172: (f|X).x<=g+R by A168,XXREAL_0:2;
x in X /\ dom(f|X) by A169,XBOOLE_0:def 4;
then g-R<=(f|X). x by A90,A160,A167,A171,RFUNCT_2:23;
then (f|X).x in {s : g-R<=s & s<=g+R} by A172;
then
A173: (f|X).x in [.g-R,g+R.] by RCOMP_1:def 1;
g-r<g by A154,XREAL_1:44;
then g-r<g+R by A168,XXREAL_0:2;
then g+R in {s : g-r<s & s<g+r} by A164;
then g+R in ].g-r,g+r.[ by RCOMP_1:def 2;
then [.g-R,g+R.] c= N1 by A155,A166,XXREAL_2:def 12;
hence (f|X).x in N1 by A173;
end;
end;
then consider N being Neighbourhood of x0 such that
A174: for x1 being Real st x1 in dom(f|X) & x1 in N
holds (f|X) .x1 in N1;
take N;
thus for x1 st x1 in dom(f|X) & x1 in N holds (f|X).x1 in N1 by
A174;
end;
hence thesis by Th4;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for f being one-to-one PartFunc of REAL,REAL st p<=g & [.p,g.] c= dom
f & (f|[.p,g.] is increasing or f|[.p,g.] is decreasing) holds (f|[.p,g.])"|(f
.:[.p,g.]) is continuous
proof
let f be one-to-one PartFunc of REAL,REAL;
assume that
A1: p<=g and
A2: [.p,g.] c= dom f and
A3: f|[.p,g.] is increasing or f|[.p,g.] is decreasing;
reconsider p, g as Real;
now
per cases by A3;
suppose
A4: f|[.p,g.] is increasing;
A5: ((f|[.p,g.])").:(f.:[.p,g.]) = ((f|[.p,g.])").: (rng (f|[.p,g.])) by
RELAT_1:115
.= ((f|[.p,g.])").:(dom ((f|[.p,g.])")) by FUNCT_1:33
.= rng ((f|[.p,g.])") by RELAT_1:113
.= dom (f|[.p,g.]) by FUNCT_1:33
.= dom f /\ [.p,g.] by RELAT_1:61
.= [.p,g.] by A2,XBOOLE_1:28;
(f|[.p,g.])"|(f.:[.p,g.]) is increasing by A4,RFUNCT_2:51;
hence thesis by A1,A5,Th46;
end;
suppose
A6: f|[.p,g.] is decreasing;
A7: ((f|[.p,g.])").:(f.:[.p,g.]) = ((f|[.p,g.])").: (rng (f|[.p,g.]))
by RELAT_1:115
.= ((f|[.p,g.])").:(dom ((f|[.p,g.])")) by FUNCT_1:33
.= rng ((f|[.p,g.])") by RELAT_1:113
.= dom (f|[.p,g.]) by FUNCT_1:33
.= dom f /\ [.p,g.] by RELAT_1:61
.= [.p,g.] by A2,XBOOLE_1:28;
(f|[.p,g.])"|(f.:[.p,g.]) is decreasing by A6,RFUNCT_2:52;
hence thesis by A1,A7,Th46;
end;
end;
hence thesis;
end;
:: from
definition
let a,b be Real;
func AffineMap(a,b) -> Function of REAL, REAL means
:Def4:
for x being Real holds it.x = a*x + b;
existence
proof
reconsider a9 = a, b9 = b as Element of REAL by XREAL_0:def 1;
deffunc F(Real)=In(a9*$1+b9,REAL);
consider f being Function of REAL, REAL such that
A1: for x being Element of REAL holds f.x =F(x) from FUNCT_2:sch 4;
take f;
let x be Real;
reconsider x9 = x as Element of REAL by XREAL_0:def 1;
f.x9 = F(x) by A1;
hence thesis;
end;
uniqueness
proof
let f,f9 be Function of REAL, REAL such that
A2: for x being Real holds f.x = a*x + b and
A3: for x being Real holds f9.x = a*x + b;
now
let x be Element of REAL;
thus f.x = a*x + b by A2
.= f9.x by A3;
end;
hence f = f9 by FUNCT_2:63;
end;
end;
registration
let a,b be Real;
cluster AffineMap(a,b) -> continuous;
coherence
proof
set f = AffineMap(a,b);
for x0 being Real st x0 in REAL holds f.x0 = a*x0+b by Def4;
then REAL = dom f & AffineMap(a,b)|REAL is continuous by Th41,FUNCT_2:def 1
;
hence thesis;
end;
end;
registration
cluster continuous for Function of REAL, REAL;
existence
proof
take AffineMap(1,1);
thus thesis;
end;
end;
theorem Th48:
for a,b being Real holds AffineMap(a,b).0 = b
proof
let a,b be Real;
thus AffineMap(a,b).0 = a*0 + b by Def4
.= b;
end;
theorem Th49:
for a,b being Real holds AffineMap(a,b).1 = a+b
proof
let a,b be Real;
thus AffineMap(a,b).1 = a*1 + b by Def4
.= a + b;
end;
theorem Th50:
for a,b being Real st a<> 0 holds AffineMap(a,b) is one-to-one
proof
let a,b be Real such that
A1: a<> 0;
let x1,x2 be object;
set f = AffineMap(a,b);
assume x1 in dom f;
then reconsider r1 = x1 as Real;
assume x2 in dom f;
then reconsider r2 = x2 as Real;
assume f.x1 = f.x2;
then a*r1+b = f.x2 by Def4
.= a*r2 +b by Def4;
hence thesis by A1,XCMPLX_1:5;
end;
theorem
for a,b,x,y being Real st a > 0 & x < y holds AffineMap(a,b).x
< AffineMap(a,b).y
proof
let a,b,x,y be Real;
assume a > 0 & x < y;
then
A1: a*x < a*y by XREAL_1:68;
AffineMap(a,b).x = a*x + b & AffineMap(a,b).y = a*y + b by Def4;
hence thesis by A1,XREAL_1:8;
end;
theorem
for a,b,x,y being Real st a < 0 & x < y holds AffineMap(a,b).x
> AffineMap(a,b).y
proof
let a,b,x,y be Real;
assume a < 0 & x < y;
then
A1: a*x > a*y by XREAL_1:69;
AffineMap(a,b).x = a*x + b & AffineMap(a,b).y = a*y + b by Def4;
hence thesis by A1,XREAL_1:8;
end;
theorem Th53:
for a,b,x,y being Real st a >= 0 & x <= y holds AffineMap
(a,b).x <= AffineMap(a,b).y
proof
let a,b,x,y be Real;
assume a >= 0 & x <= y;
then
A1: a*x <= a*y by XREAL_1:64;
AffineMap(a,b).x = a*x + b & AffineMap(a,b).y = a*y + b by Def4;
hence thesis by A1,XREAL_1:7;
end;
theorem
for a,b,x,y being Real st a <= 0 & x <= y holds AffineMap(a,b).
x >= AffineMap(a,b).y
proof
let a,b,x,y be Real;
assume a <= 0 & x <= y;
then
A1: a*x >= a*y by XREAL_1:65;
AffineMap(a,b).x = a*x + b & AffineMap(a,b).y = a*y + b by Def4;
hence thesis by A1,XREAL_1:7;
end;
theorem Th55:
for a,b being Real st a <> 0 holds rng AffineMap(a,b) = REAL
proof
let a,b be Real such that
A1: a <> 0;
thus rng AffineMap(a,b) c= REAL;
let e be object;
assume e in REAL;
then reconsider r = e as Element of REAL;
reconsider s = (r - b)/a as Element of REAL by XREAL_0:def 1;
AffineMap(a,b).s = a*s + b by Def4
.= r - b + b by A1,XCMPLX_1:87
.= r;
then r in rng AffineMap(a,b) by FUNCT_2:4;
hence thesis;
end;
theorem
for a,b being Real st a <> 0 holds (AffineMap(a,b) qua
Function)" = AffineMap(a",-b/a)
proof
let a,b be Real such that
A1: a <> 0;
for x being Element of REAL holds (AffineMap(a",-b/a)*AffineMap(a,b)).x
= (id REAL).x
proof
let x being Element of REAL;
thus (AffineMap(a",-b/a)*AffineMap(a,b)).x = AffineMap(a",-b/a).(AffineMap
(a,b).x) by FUNCT_2:15
.= AffineMap(a",-b/a).(a*x+b) by Def4
.= a"*(a*x+b)+-b/a by Def4
.= a"*a*x+a"*b +-b/a
.= 1 *x+a"*b +-b/a by A1,XCMPLX_0:def 7
.= x+a"*b -b/a
.= x+ b/a -b/a by XCMPLX_0:def 9
.= (id REAL).x;
end;
then
A2: AffineMap(a",-b/a)*AffineMap(a,b) = id REAL by FUNCT_2:63;
rng AffineMap(a,b) = REAL by A1,Th55;
hence thesis by A1,A2,Th50,FUNCT_2:30;
end;
theorem
for a,b being Real st a > 0 holds AffineMap(a,b).:[.0,1.] = [.b,a+b.]
proof
let a,b be Real such that
A1: a > 0;
thus AffineMap(a,b).:[.0,1.] c= [.b,a+b.]
proof
A2: AffineMap(a,b).1 = a+b by Th49;
let u be object;
assume u in AffineMap(a,b).:[.0,1.];
then consider r being Element of REAL such that
A3: r in [.0,1.] and
A4: u = AffineMap(a,b).r by FUNCT_2:65;
reconsider s = u as Real by A4;
r <= 1 by A3,XXREAL_1:1;
then
A5: s <= a+b by A1,A4,A2,Th53;
A6: AffineMap(a,b).0 = b by Th48;
0 <= r by A3,XXREAL_1:1;
then b <= s by A1,A4,A6,Th53;
hence thesis by A5,XXREAL_1:1;
end;
let u be object;
assume
A7: u in [.b,a+b.];
then reconsider r = u as Element of REAL;
set s = (r - b)/a;
A8: AffineMap(a,b).s = a*s + b by Def4
.= r - b + b by A1,XCMPLX_1:87
.= r;
r <= a+b by A7,XXREAL_1:1;
then r-b <= a by XREAL_1:20;
then s <= a/a by A1,XREAL_1:72;
then
A9: s <= 1 by A1,XCMPLX_1:60;
b <= r by A7,XXREAL_1:1;
then 0 <= r - b by XREAL_1:48;
then s in [.0,1.] by A1,A9,XXREAL_1:1;
hence thesis by A8,FUNCT_2:35;
end;