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
begin
definition
let a,
b be
real number ;
assume B1:
a <= b
;
let t1,
t2 be
Point of
(Closed-Interval-TSpace (a,b));
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)) holds b1 . s = ((1 - s) * t1) + (s * t2)
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)) holds b1 . s = ((1 - s) * t1) + (s * t2) ) & ( for s being Point of (Closed-Interval-TSpace (0,1)) holds b2 . s = ((1 - s) * t1) + (s * t2) ) holds
b1 = b2
end;
definition
let a,
b be
real number ;
assume B1:
a < b
;
let t1,
t2 be
Point of
(Closed-Interval-TSpace (0,1));
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)) holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (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)) holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) & ( for s being Point of (Closed-Interval-TSpace (a,b)) holds b2 . s = (((b - s) * t1) + ((s - a) * t2)) / (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)) holds b5 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) );
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 Th15:
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 Th16:
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 Th17:
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