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 :
for a, b being real number st a <= b holds
(#) (a,b) = a;
:: deftheorem Def2 defines (#) TREAL_1:def 2 :
for a, b being real number st a <= b holds
(a,b) (#) = b;
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)) holds
it . s = ((1 - s) * t1) + (s * t2);
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;
:: 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)) holds b5 . s = ((1 - s) * t1) + (s * t2) );
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)) holds
it . s = (((b - s) * t1) + ((s - a) * t2)) / (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)) 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 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