let a, b, d, e be Real; ( a <= b & e < 0 implies ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) st
( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds
f . r = (e * r) + d ) ) )
assume that
A1:
a <= b
and
A2:
e < 0
; ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) st
( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds
f . r = (e * r) + d ) )
set S = Closed-Interval-TSpace (a,b);
defpred S1[ object , object ] means for r being Real st $1 = r holds
$2 = (e * r) + d;
set X = the carrier of (Closed-Interval-TSpace (a,b));
A3:
the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.]
by A1, TOPMETR:18;
then reconsider B = the carrier of (Closed-Interval-TSpace (a,b)) as Subset of R^1 by TOPMETR:17;
A4:
R^1 | B = Closed-Interval-TSpace (a,b)
by A1, A3, TOPMETR:19;
set T = Closed-Interval-TSpace (((e * b) + d),((e * a) + d));
set Y = the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d)));
A5:
e * a >= e * b
by A1, A2, XREAL_1:65;
then A6:
the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) = [.((e * b) + d),((e * a) + d).]
by TOPMETR:18, XREAL_1:7;
then reconsider C = the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) as Subset of R^1 by TOPMETR:17;
defpred S2[ object , object ] means for r being Real st r = $1 holds
$2 = (e * r) + d;
Closed-Interval-TSpace (((e * b) + d),((e * a) + d)) = TopSpaceMetr (Closed-Interval-MSpace (((e * b) + d),((e * a) + d)))
by TOPMETR:def 7;
then A7:
Closed-Interval-TSpace (((e * b) + d),((e * a) + d)) is T_2
by PCOMPS_1:34;
A8:
for x being object st x in the carrier of (Closed-Interval-TSpace (a,b)) holds
ex y being object st
( y in the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) & S1[x,y] )
proof
let x be
object ;
( x in the carrier of (Closed-Interval-TSpace (a,b)) implies ex y being object st
( y in the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) & S1[x,y] ) )
assume A9:
x in the
carrier of
(Closed-Interval-TSpace (a,b))
;
ex y being object st
( y in the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) & S1[x,y] )
then reconsider r1 =
x as
Real ;
set y1 =
(e * r1) + d;
r1 <= b
by A3, A9, XXREAL_1:1;
then
e * r1 >= e * b
by A2, XREAL_1:65;
then A10:
(e * r1) + d >= (e * b) + d
by XREAL_1:7;
a <= r1
by A3, A9, XXREAL_1:1;
then
e * a >= e * r1
by A2, XREAL_1:65;
then
(e * a) + d >= (e * r1) + d
by XREAL_1:7;
then
( ( for
r being
Real st
x = r holds
(e * r1) + d = (e * r) + d ) &
(e * r1) + d in the
carrier of
(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) )
by A6, A10, XXREAL_1:1;
hence
ex
y being
object st
(
y in the
carrier of
(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) &
S1[
x,
y] )
;
verum
end;
ex f being Function of the carrier of (Closed-Interval-TSpace (a,b)), the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) st
for x being object st x in the carrier of (Closed-Interval-TSpace (a,b)) holds
S1[x,f . x]
from FUNCT_2:sch 1(A8);
then consider f1 being Function of the carrier of (Closed-Interval-TSpace (a,b)), the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) such that
A11:
for x being object st x in the carrier of (Closed-Interval-TSpace (a,b)) holds
S1[x,f1 . x]
;
reconsider f2 = f1 as Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) ;
A12:
for r being Real st r in [.a,b.] holds
f2 . r = (e * r) + d
by A3, A11;
A13:
dom f2 = the carrier of (Closed-Interval-TSpace (a,b))
by FUNCT_2:def 1;
[#] (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) c= rng f2
proof
let y be
object ;
TARSKI:def 3 ( not y in [#] (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) or y in rng f2 )
assume A14:
y in [#] (Closed-Interval-TSpace (((e * b) + d),((e * a) + d)))
;
y in rng f2
then reconsider ry =
y as
Real ;
ry <= (e * a) + d
by A6, A14, XXREAL_1:1;
then
((e * a) + d) - d >= ry - d
by XREAL_1:9;
then
(a * e) / e <= (ry - d) / e
by A2, XREAL_1:73;
then A15:
a <= (ry - d) / e
by A2, XCMPLX_1:89;
(e * b) + d <= ry
by A6, A14, XXREAL_1:1;
then
((e * b) + d) - d <= ry - d
by XREAL_1:9;
then
(b * e) / e >= (ry - d) / e
by A2, XREAL_1:73;
then
b >= (ry - d) / e
by A2, XCMPLX_1:89;
then A16:
(ry - d) / e in [.a,b.]
by A15, XXREAL_1:1;
then f2 . ((ry - d) / e) =
(e * ((ry - d) / e)) + d
by A3, A11
.=
(ry - d) + d
by A2, XCMPLX_1:87
.=
ry
;
hence
y in rng f2
by A3, A13, A16, FUNCT_1:3;
verum
end;
then A17:
rng f2 = [#] (Closed-Interval-TSpace (((e * b) + d),((e * a) + d)))
by XBOOLE_0:def 10;
then reconsider f3 = f1 as Function of (Closed-Interval-TSpace (a,b)),R^1 by A6, A13, FUNCT_2:2, TOPMETR:17;
for x1, x2 being object st x1 in dom f2 & x2 in dom f2 & f2 . x1 = f2 . x2 holds
x1 = x2
then A21:
( dom f2 = [#] (Closed-Interval-TSpace (a,b)) & f2 is one-to-one )
by FUNCT_1:def 4, FUNCT_2:def 1;
A22:
for x being object st x in the carrier of R^1 holds
ex y being object st
( y in the carrier of R^1 & S2[x,y] )
ex f4 being Function of the carrier of R^1, the carrier of R^1 st
for x being object st x in the carrier of R^1 holds
S2[x,f4 . x]
from FUNCT_2:sch 1(A22);
then consider f4 being Function of the carrier of R^1, the carrier of R^1 such that
A23:
for x being object st x in the carrier of R^1 holds
S2[x,f4 . x]
;
reconsider f5 = f4 as Function of R^1,R^1 ;
A24:
for x being Real holds f5 . x = (e * x) + d
by XREAL_0:def 1, TOPMETR:17, A23;
A25: (dom f5) /\ B =
REAL /\ B
by FUNCT_2:def 1, TOPMETR:17
.=
B
by TOPMETR:17, XBOOLE_1:28
;
A26:
for x being object st x in dom f3 holds
f3 . x = f5 . x
dom f3 = B
by FUNCT_2:def 1;
then
f3 = f5 | B
by A25, A26, FUNCT_1:46;
then A28:
f3 is continuous
by A24, A4, TOPMETR:7, TOPMETR:21;
A29:
Closed-Interval-TSpace (a,b) is compact
by A1, HEINE:4;
R^1 | C = Closed-Interval-TSpace (((e * b) + d),((e * a) + d))
by A5, A6, TOPMETR:19, XREAL_1:7;
then
f2 is being_homeomorphism
by A21, A17, A28, A29, A7, COMPTS_1:17, TOPMETR:6;
hence
ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) st
( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds
f . r = (e * r) + d ) )
by A12; verum