:: TREAL_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: TREAL_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c, d, b being real number st a <= c & d <= b holds
[.c,d.] c= [.a,b.]
proof end;

theorem Th2: :: TREAL_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c, b, d being real number st a <= c & b <= d & c <= b holds
[.a,b.] \/ [.c,d.] = [.a,d.]
proof end;

theorem Th3: :: TREAL_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c, b, d being real number st a <= c & b <= d & c <= b holds
[.a,b.] /\ [.c,d.] = [.c,b.]
proof end;

Lm1: for a, b being real number
for x being set st x in [.a,b.] holds
x is Real
;

Lm2: for a, b, v being real number
for x being set st x in [.a,b.] & a <= b & v = x holds
( a <= v & v <= b )
proof end;

Lm3: for a, b being real number
for x being Point of (Closed-Interval-TSpace a,b) st a <= b holds
x is Real
proof end;

theorem Th4: :: TREAL_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for A being Subset of R^1 st A = [.a,b.] holds
A is closed
proof end;

theorem Th5: :: TREAL_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <= b holds
Closed-Interval-TSpace a,b is closed SubSpace of R^1
proof end;

theorem :: TREAL_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c, d, b being real number st a <= c & d <= b & c <= d holds
Closed-Interval-TSpace c,d is closed SubSpace of Closed-Interval-TSpace a,b
proof end;

theorem :: TREAL_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c, b, d being real number st a <= c & b <= d & c <= b holds
( Closed-Interval-TSpace a,d = (Closed-Interval-TSpace a,b) union (Closed-Interval-TSpace c,d) & Closed-Interval-TSpace c,b = (Closed-Interval-TSpace a,b) meet (Closed-Interval-TSpace c,d) )
proof end;

definition
let a, b be real number ;
assume A1: a <= b ;
func (#) a,b -> Point of (Closed-Interval-TSpace a,b) equals :Def1: :: TREAL_1:def 1
a;
coherence
a is Point of (Closed-Interval-TSpace a,b)
proof end;
correctness
;
func a,b (#) -> Point of (Closed-Interval-TSpace a,b) equals :Def2: :: TREAL_1:def 2
b;
coherence
b is Point of (Closed-Interval-TSpace a,b)
proof end;
correctness
;
end;

:: 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 :: TREAL_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 0[01] = (#) 0,1 & 1[01] = 0,1 (#) ) by Def1, Def2, BORSUK_1:def 17, BORSUK_1:def 18;

theorem :: TREAL_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a <= b & b <= c holds
( (#) a,b = (#) a,c & b,c (#) = a,c (#) )
proof end;

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: :: TREAL_1:def 3
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)
proof end;
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
proof end;
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: :: TREAL_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace a,b)
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
(L[01] t1,t2) . s = ((r2 - r1) * r) + r1
proof end;

theorem Th11: :: TREAL_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace a,b) holds L[01] t1,t2 is continuous Function of (Closed-Interval-TSpace 0,1),(Closed-Interval-TSpace a,b)
proof end;

theorem :: TREAL_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace a,b) holds
( (L[01] t1,t2) . ((#) 0,1) = t1 & (L[01] t1,t2) . (0,1 (#) ) = t2 )
proof end;

theorem :: TREAL_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
L[01] ((#) 0,1),(0,1 (#) ) = id (Closed-Interval-TSpace 0,1)
proof end;

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: :: TREAL_1:def 4
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)
proof end;
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
proof end;
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: :: TREAL_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace 0,1)
for s being Point of (Closed-Interval-TSpace a,b)
for r, r1, r2 being Real st s = r & r1 = t1 & r2 = t2 holds
(P[01] a,b,t1,t2) . s = (((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a))
proof end;

theorem Th15: :: TREAL_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0,1)
proof end;

theorem :: TREAL_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: TREAL_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
P[01] 0,1,((#) 0,1),(0,1 (#) ) = id (Closed-Interval-TSpace 0,1)
proof end;

theorem Th18: :: TREAL_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 (#) )) )
proof end;

theorem Th19: :: TREAL_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)) )
proof end;

theorem Th20: :: TREAL_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a < b holds
( L[01] ((#) a,b),(a,b (#) ) is_homeomorphism & (L[01] ((#) a,b),(a,b (#) )) " = P[01] a,b,((#) 0,1),(0,1 (#) ) & P[01] a,b,((#) 0,1),(0,1 (#) ) is_homeomorphism & (P[01] a,b,((#) 0,1),(0,1 (#) )) " = L[01] ((#) a,b),(a,b (#) ) )
proof end;

theorem :: TREAL_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a < b holds
( L[01] (a,b (#) ),((#) a,b) is_homeomorphism & (L[01] (a,b (#) ),((#) a,b)) " = P[01] a,b,(0,1 (#) ),((#) 0,1) & P[01] a,b,(0,1 (#) ),((#) 0,1) is_homeomorphism & (P[01] a,b,(0,1 (#) ),((#) 0,1)) " = L[01] (a,b (#) ),((#) a,b) )
proof end;

theorem Th22: :: TREAL_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
I[01] is connected
proof end;

theorem :: TREAL_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <= b holds
Closed-Interval-TSpace a,b is connected
proof end;

theorem Th24: :: TREAL_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being continuous Function of I[01] ,I[01] ex x being Point of I[01] st f . x = x
proof end;

theorem Th25: :: TREAL_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a <= b holds
for f being continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace a,b) ex x being Point of (Closed-Interval-TSpace a,b) st f . x = x
proof end;

theorem Th26: :: TREAL_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty SubSpace of R^1
for f being continuous Function of X,Y st ex a, b being Real st
( a <= b & [.a,b.] c= the carrier of X & [.a,b.] c= the carrier of Y & f .: [.a,b.] c= [.a,b.] ) holds
ex x being Point of X st f . x = x
proof end;

theorem :: TREAL_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty SubSpace of R^1
for f being continuous Function of X,Y st ex a, b being Real st
( a <= b & [.a,b.] c= the carrier of X & f .: [.a,b.] c= [.a,b.] ) holds
ex x being Point of X st f . x = x
proof end;