begin
Lm1:
for a, b being real number
for x being set st x in [.a,b.] holds
x is Real
;
Lm2:
for a, b being real number
for x being Point of (Closed-Interval-TSpace a,b) st a <= b holds
x is Real
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem Th5:
theorem
theorem
:: deftheorem Def1 defines (#) TREAL_1:def 1 :
:: deftheorem Def2 defines (#) TREAL_1:def 2 :
theorem
theorem
begin
definition
let a,
b be
real number ;
assume A1:
a <= b
;
let t1,
t2 be
Point of
(Closed-Interval-TSpace a,b);
func L[01] t1,
t2 -> Function of
(Closed-Interval-TSpace 0 ,1),
(Closed-Interval-TSpace a,b) means :
Def3:
for
s being
Point of
(Closed-Interval-TSpace 0 ,1) for
r,
r1,
r2 being
real number st
s = r &
r1 = t1 &
r2 = t2 holds
it . s = ((1 - r) * r1) + (r * r2);
existence
ex b1 being Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace a,b) st
for s being Point of (Closed-Interval-TSpace 0 ,1)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
b1 . s = ((1 - r) * r1) + (r * r2)
uniqueness
for b1, b2 being Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace a,b) st ( for s being Point of (Closed-Interval-TSpace 0 ,1)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
b1 . s = ((1 - r) * r1) + (r * r2) ) & ( for s being Point of (Closed-Interval-TSpace 0 ,1)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
b2 . s = ((1 - r) * r1) + (r * r2) ) holds
b1 = b2
end;
:: deftheorem Def3 defines L[01] TREAL_1:def 3 :
for
a,
b being
real number st
a <= b holds
for
t1,
t2 being
Point of
(Closed-Interval-TSpace a,b) for
b5 being
Function of
(Closed-Interval-TSpace 0 ,1),
(Closed-Interval-TSpace a,b) holds
(
b5 = L[01] t1,
t2 iff for
s being
Point of
(Closed-Interval-TSpace 0 ,1) for
r,
r1,
r2 being
real number st
s = r &
r1 = t1 &
r2 = t2 holds
b5 . s = ((1 - r) * r1) + (r * r2) );
theorem Th10:
theorem Th11:
theorem
theorem
definition
let a,
b be
real number ;
assume A1:
a < b
;
let t1,
t2 be
Point of
(Closed-Interval-TSpace 0 ,1);
func P[01] a,
b,
t1,
t2 -> Function of
(Closed-Interval-TSpace a,b),
(Closed-Interval-TSpace 0 ,1) means :
Def4:
for
s being
Point of
(Closed-Interval-TSpace a,b) for
r,
r1,
r2 being
real number st
s = r &
r1 = t1 &
r2 = t2 holds
it . s = (((b - r) * r1) + ((r - a) * r2)) / (b - a);
existence
ex b1 being Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0 ,1) st
for s being Point of (Closed-Interval-TSpace a,b)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
b1 . s = (((b - r) * r1) + ((r - a) * r2)) / (b - a)
uniqueness
for b1, b2 being Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0 ,1) st ( for s being Point of (Closed-Interval-TSpace a,b)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
b1 . s = (((b - r) * r1) + ((r - a) * r2)) / (b - a) ) & ( for s being Point of (Closed-Interval-TSpace a,b)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
b2 . s = (((b - r) * r1) + ((r - a) * r2)) / (b - a) ) holds
b1 = b2
end;
:: deftheorem Def4 defines P[01] TREAL_1:def 4 :
for
a,
b being
real number st
a < b holds
for
t1,
t2 being
Point of
(Closed-Interval-TSpace 0 ,1) for
b5 being
Function of
(Closed-Interval-TSpace a,b),
(Closed-Interval-TSpace 0 ,1) holds
(
b5 = P[01] a,
b,
t1,
t2 iff for
s being
Point of
(Closed-Interval-TSpace a,b) for
r,
r1,
r2 being
real number st
s = r &
r1 = t1 &
r2 = t2 holds
b5 . s = (((b - r) * r1) + ((r - a) * r2)) / (b - a) );
theorem Th14:
theorem Th15:
theorem
for
a,
b being
real number st
a < b holds
for
t1,
t2 being
Point of
(Closed-Interval-TSpace 0 ,1) holds
(
(P[01] a,b,t1,t2) . ((#) a,b) = t1 &
(P[01] a,b,t1,t2) . (a,b (#) ) = t2 )
theorem
theorem Th18:
for
a,
b being
real number st
a < b holds
(
id (Closed-Interval-TSpace a,b) = (L[01] ((#) a,b),(a,b (#) )) * (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) &
id (Closed-Interval-TSpace 0 ,1) = (P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) * (L[01] ((#) a,b),(a,b (#) )) )
theorem Th19:
for
a,
b being
real number st
a < b holds
(
id (Closed-Interval-TSpace a,b) = (L[01] (a,b (#) ),((#) a,b)) * (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) &
id (Closed-Interval-TSpace 0 ,1) = (P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) * (L[01] (a,b (#) ),((#) a,b)) )
theorem Th20:
for
a,
b being
real number st
a < b holds
(
L[01] ((#) a,b),
(a,b (#) ) is
being_homeomorphism &
(L[01] ((#) a,b),(a,b (#) )) " = P[01] a,
b,
((#) 0 ,1),
(0 ,1 (#) ) &
P[01] a,
b,
((#) 0 ,1),
(0 ,1 (#) ) is
being_homeomorphism &
(P[01] a,b,((#) 0 ,1),(0 ,1 (#) )) " = L[01] ((#) a,b),
(a,b (#) ) )
theorem
for
a,
b being
real number st
a < b holds
(
L[01] (a,b (#) ),
((#) a,b) is
being_homeomorphism &
(L[01] (a,b (#) ),((#) a,b)) " = P[01] a,
b,
(0 ,1 (#) ),
((#) 0 ,1) &
P[01] a,
b,
(0 ,1 (#) ),
((#) 0 ,1) is
being_homeomorphism &
(P[01] a,b,(0 ,1 (#) ),((#) 0 ,1)) " = L[01] (a,b (#) ),
((#) a,b) )
begin
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem