:: Real Function Continuity :: by Konrad Raczkowski and Pawe{\l} Sadowski :: :: Received June 18, 1990 :: Copyright (c) 1990-2021 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.|
x0;
defpred P[Nat,set,set] means for n,m st $2=n & $3=m holds n 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.| 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 &
00 by A9;
let x2 such that
x2 in REAL and
A11: |.x2-x1.|{} & (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 Lipschitzian for PartFunc of REAL,REAL;
coherence
proof
set X = dom f1, X1 = dom f2;
consider s such that
A9: 0 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: 00;
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 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(f|X).x0 by A15,XREAL_1:29,215;
A33: now
assume
A34: x2-(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-x0x0 by A67,A71,A75,XREAL_1:44,215;
then x1x1;
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-(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: R0 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: Rx1;
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 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;