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

registration
let n be Nat;
cluster non empty convex Element of bool the carrier of (TOP-REAL n);
existence
ex b1 being Subset of (TOP-REAL n) st
( not b1 is empty & b1 is convex )
proof end;
end;

definition
let n be Nat;
let T be SubSpace of TOP-REAL n;
attr T is convex means :Def1: :: TOPALG_2:def 1
 [#] T is convex Subset of (TOP-REAL n);
end;

:: deftheorem Def1 defines convex TOPALG_2:def 1 :
for n being Nat
for T being SubSpace of TOP-REAL n holds
( T is convex iff [#] T is convex Subset of (TOP-REAL n) );

registration
let n be Nat;
cluster non empty convex -> non empty arcwise_connected SubSpace of TOP-REAL n;
coherence
for b1 being non empty SubSpace of TOP-REAL n st b1 is convex holds
b1 is arcwise_connected
proof end;
end;

registration
let n be Nat;
cluster non empty strict arcwise_connected convex SubSpace of TOP-REAL n;
existence
ex b1 being SubSpace of TOP-REAL n st
( b1 is strict & not b1 is empty & b1 is convex )
proof end;
end;

theorem Th1: :: TOPALG_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for Y being non empty SubSpace of X
for x1, x2 being Point of X
for y1, y2 being Point of Y
for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds
f is Path of x1,x2
proof end;

set I = the carrier of I[01] ;

Lm1: the carrier of [:I[01] ,I[01] :] = [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:def 5;

Lm2: the carrier of [:(TOP-REAL 1),I[01] :] = [:the carrier of (TOP-REAL 1),the carrier of I[01] :]
by BORSUK_1:def 5;

Lm3: the carrier of [:R^1 ,I[01] :] = [:the carrier of R^1 ,the carrier of I[01] :]
by BORSUK_1:def 5;

Lm4: dom (id I[01] ) = the carrier of I[01]
by FUNCT_2:def 1;

definition
let n be Nat;
let T be non empty convex SubSpace of TOP-REAL n;
let a, b be Point of T;
let P, Q be Path of a,b;
func ConvexHomotopy P,Q -> Function of [:I[01] ,I[01] :],T means :Def2: :: TOPALG_2:def 2
for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
it . s,t = ((1 - t) * a1) + (t * b1);
existence
ex b1 being Function of [:I[01] ,I[01] :],T st
for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b1 . s,t = ((1 - t) * a1) + (t * b1)
proof end;
uniqueness
for b1, b2 being Function of [:I[01] ,I[01] :],T st ( for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b1 . s,t = ((1 - t) * a1) + (t * b1) ) & ( for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b2 . s,t = ((1 - t) * a1) + (t * b1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ConvexHomotopy TOPALG_2:def 2 :
for n being Nat
for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b
for b7 being Function of [:I[01] ,I[01] :],T holds
( b7 = ConvexHomotopy P,Q iff for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
b7 . s,t = ((1 - t) * a1) + (t * b1) );

Lm5: for n being Nat
for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b holds ConvexHomotopy P,Q is continuous
proof end;

Lm6: for n being Nat
for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (ConvexHomotopy P,Q) . s,0 = P . s & (ConvexHomotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy P,Q) . 0,t = a & (ConvexHomotopy P,Q) . 1,t = b ) ) )
proof end;

theorem Th2: :: TOPALG_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b holds P,Q are_homotopic
proof end;

definition
let n be Nat;
let T be non empty convex SubSpace of TOP-REAL n;
let a, b be Point of T;
let P, Q be Path of a,b;
:: original: ConvexHomotopy
redefine func ConvexHomotopy P,Q -> Homotopy of P,Q;
coherence
ConvexHomotopy P,Q is Homotopy of P,Q
proof end;
end;

registration
let n be Nat;
let T be non empty convex SubSpace of TOP-REAL n;
let a, b be Point of T;
let P, Q be Path of a,b;
cluster -> continuous Homotopy of P,Q;
coherence
for b1 being Homotopy of P,Q holds b1 is continuous
proof end;
end;

theorem Th3: :: TOPALG_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being non empty convex SubSpace of TOP-REAL n
for a being Point of T
for C being Loop of a holds the carrier of (pi_1 T,a) = {(Class (EqRel T,a),C)}
proof end;

registration
let n be Nat;
let T be non empty convex SubSpace of TOP-REAL n;
let a be Point of T;
cluster FundamentalGroup T,a -> trivial ;
coherence
pi_1 T,a is trivial
proof end;
end;

theorem Th4: :: TOPALG_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number holds Proj |[a]|,1 = a
proof end;

registration
cluster -> real-membered SubSpace of R^1 ;
coherence
for b1 being SubSpace of R^1 holds b1 is real-membered ;
end;

theorem :: TOPALG_2: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
[.a,b.] = { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) }
proof end;

theorem Th6: :: TOPALG_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Function of [:R^1 ,I[01] :],R^1 st ( for x being Point of R^1
for i being Point of I[01] holds F . x,i = (1 - i) * x ) holds
F is continuous
proof end;

theorem Th7: :: TOPALG_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Function of [:R^1 ,I[01] :],R^1 st ( for x being Point of R^1
for i being Point of I[01] holds F . x,i = i * x ) holds
F is continuous
proof end;

definition
let P be Subset of R^1 ;
attr P is convex means :Def3: :: TOPALG_2:def 3
for a, b being Point of R^1 st a in P & b in P holds
[.a,b.] c= P;
end;

:: deftheorem Def3 defines convex TOPALG_2:def 3 :
for P being Subset of R^1 holds
( P is convex iff for a, b being Point of R^1 st a in P & b in P holds
[.a,b.] c= P );

registration
cluster non empty convex Element of bool the carrier of R^1 ;
existence
ex b1 being Subset of R^1 st
( not b1 is empty & b1 is convex )
proof end;
cluster empty -> convex Element of bool the carrier of R^1 ;
coherence
for b1 being Subset of R^1 st b1 is empty holds
b1 is convex
proof end;
end;

theorem Th8: :: TOPALG_2:8  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 holds [.a,b.] is convex Subset of R^1
proof end;

theorem :: TOPALG_2:9  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 holds ].a,b.[ is convex Subset of R^1
proof end;

theorem :: TOPALG_2: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 holds [.a,b.[ is convex Subset of R^1
proof end;

theorem :: TOPALG_2: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 holds ].a,b.] is convex Subset of R^1
proof end;

definition
let T be SubSpace of R^1 ;
attr T is convex means :Def4: :: TOPALG_2:def 4
 [#] T is convex Subset of R^1 ;
end;

:: deftheorem Def4 defines convex TOPALG_2:def 4 :
for T being SubSpace of R^1 holds
( T is convex iff [#] T is convex Subset of R^1 );

Lm7: for T being SubSpace of R^1 st T = R^1 holds
T is convex
proof end;

registration
cluster non empty strict real-membered convex SubSpace of R^1 ;
existence
ex b1 being SubSpace of R^1 st
( b1 is strict & not b1 is empty & b1 is convex )
proof end;
end;

definition
:: original: R^1
redefine func R^1 -> strict convex SubSpace of R^1 ;
coherence
R^1 is strict convex SubSpace of R^1 by Lm7, TSEP_1:2;
end;

theorem Th12: :: TOPALG_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty convex SubSpace of R^1
for a, b being Point of T holds [.a,b.] c= the carrier of T
proof end;

registration
cluster non empty convex -> non empty arcwise_connected real-membered SubSpace of R^1 ;
coherence
for b1 being non empty SubSpace of R^1 st b1 is convex holds
b1 is arcwise_connected
proof end;
end;

theorem Th13: :: TOPALG_2:13  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 convex
proof end;

theorem Th14: :: TOPALG_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
I[01] is convex by Th13, TOPMETR:27;

theorem :: TOPALG_2: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
Closed-Interval-TSpace a,b is arcwise_connected
proof end;

definition
let T be non empty convex SubSpace of R^1 ;
let a, b be Point of T;
let P, Q be Path of a,b;
func R1Homotopy P,Q -> Function of [:I[01] ,I[01] :],T means :Def5: :: TOPALG_2:def 5
for s, t being Element of I[01] holds it . s,t = ((1 - t) * (P . s)) + (t * (Q . s));
existence
ex b1 being Function of [:I[01] ,I[01] :],T st
for s, t being Element of I[01] holds b1 . s,t = ((1 - t) * (P . s)) + (t * (Q . s))
proof end;
uniqueness
for b1, b2 being Function of [:I[01] ,I[01] :],T st ( for s, t being Element of I[01] holds b1 . s,t = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds b2 . s,t = ((1 - t) * (P . s)) + (t * (Q . s)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines R1Homotopy TOPALG_2:def 5 :
for T being non empty convex SubSpace of R^1
for a, b being Point of T
for P, Q being Path of a,b
for b6 being Function of [:I[01] ,I[01] :],T holds
( b6 = R1Homotopy P,Q iff for s, t being Element of I[01] holds b6 . s,t = ((1 - t) * (P . s)) + (t * (Q . s)) );

Lm8: for T being non empty convex SubSpace of R^1
for a, b being Point of T
for P, Q being Path of a,b holds R1Homotopy P,Q is continuous
proof end;

Lm9: for T being non empty convex SubSpace of R^1
for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (R1Homotopy P,Q) . s,0 = P . s & (R1Homotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (R1Homotopy P,Q) . 0,t = a & (R1Homotopy P,Q) . 1,t = b ) ) )
proof end;

theorem Th16: :: TOPALG_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty convex SubSpace of R^1
for a, b being Point of T
for P, Q being Path of a,b holds P,Q are_homotopic
proof end;

definition
let T be non empty convex SubSpace of R^1 ;
let a, b be Point of T;
let P, Q be Path of a,b;
:: original: R1Homotopy
redefine func R1Homotopy P,Q -> Homotopy of P,Q;
coherence
R1Homotopy P,Q is Homotopy of P,Q
proof end;
end;

registration
let T be non empty convex SubSpace of R^1 ;
let a, b be Point of T;
let P, Q be Path of a,b;
cluster -> continuous Homotopy of P,Q;
coherence
for b1 being Homotopy of P,Q holds b1 is continuous
proof end;
end;

theorem Th17: :: TOPALG_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty convex SubSpace of R^1
for a being Point of T
for C being Loop of a holds the carrier of (pi_1 T,a) = {(Class (EqRel T,a),C)}
proof end;

registration
let T be non empty convex SubSpace of R^1 ;
let a be Point of T;
cluster FundamentalGroup T,a -> trivial ;
coherence
pi_1 T,a is trivial
proof end;
end;

theorem :: TOPALG_2: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
for x, y being Point of (Closed-Interval-TSpace a,b)
for P, Q being Path of x,y holds P,Q are_homotopic
proof end;

theorem :: TOPALG_2: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
for x being Point of (Closed-Interval-TSpace a,b)
for C being Loop of x holds the carrier of (pi_1 (Closed-Interval-TSpace a,b),x) = {(Class (EqRel (Closed-Interval-TSpace a,b),x),C)}
proof end;

theorem :: TOPALG_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Point of I[01]
for P, Q being Path of x,y holds P,Q are_homotopic by Th14, Th16;

theorem Th21: :: TOPALG_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of I[01]
for C being Loop of x holds the carrier of (pi_1 I[01] ,x) = {(Class (EqRel I[01] ,x),C)} by Th14, Th17;

registration
let x be Point of I[01] ;
cluster FundamentalGroup I[01] ,x -> trivial ;
coherence
pi_1 I[01] ,x is trivial
proof end;
end;