:: The Fundamental Group of Convex Subspaces of TOP-REAL n
:: by Artur Korni{\l}owicz
::
:: Received April 20, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

registration
let n be Element of NAT ;
cluster non empty convex for 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 Element of 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 Element of 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 Element of NAT ;
cluster non empty convex -> non empty pathwise_connected for SubSpace of TOP-REAL n;
coherence
for b1 being non empty SubSpace of TOP-REAL n st b1 is convex holds
b1 is pathwise_connected
proof end;
end;

registration
let n be Element of NAT ;
cluster non empty strict TopSpace-like convex for 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 :: TOPALG_2:1
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 2;

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

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

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

definition
let n be Element of NAT ;
let T be non empty convex SubSpace of TOP-REAL n;
let P, Q be Function of I[01],T;
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 Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for P, Q being Function of I[01],T
for b5 being Function of [:I[01],I[01]:],T holds
( b5 = 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
b5 . (s,t) = ((1 - t) * a1) + (t * b1) );

Lm5: for n being Element of NAT
for T being non empty convex SubSpace of TOP-REAL n
for P, Q being continuous Function of I[01],T holds ConvexHomotopy (P,Q) is continuous
proof end;

Lm6: for n being Element of 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
for n being Element of 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;

registration
let n be Element of 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 for Homotopy of P,Q;
coherence
for b1 being Homotopy of P,Q holds b1 is continuous
proof end;
end;

theorem Th3: :: TOPALG_2:3
for n being Element of 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 Element of 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;

begin

theorem Th4: :: TOPALG_2:4
for a being real number holds |[a]| /. 1 = a
proof end;

theorem :: TOPALG_2:5
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
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
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;

registration
cluster non empty V166() V167() V168() interval for Element of bool the carrier of R^1;
existence
ex b1 being Subset of R^1 st
( not b1 is empty & b1 is interval )
proof end;
end;

registration
let T be real-membered TopStruct ;
cluster V166() V167() V168() interval for Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 is interval
proof end;
end;

definition
let T be real-membered TopStruct ;
attr T is interval means :Def3: :: TOPALG_2:def 3
 [#] T is interval ;
end;

:: deftheorem Def3 defines interval TOPALG_2:def 3 :
for T being real-membered TopStruct holds
( T is interval iff [#] T is interval );

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

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

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

theorem Th8: :: TOPALG_2:8
for T being non empty interval 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 interval -> non empty pathwise_connected for SubSpace of R^1 ;
coherence
for b1 being non empty SubSpace of R^1 st b1 is interval holds
b1 is pathwise_connected
proof end;
end;

theorem Th9: :: TOPALG_2:9
for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is interval
proof end;

theorem Th10: :: TOPALG_2:10
I[01] is interval by Th9, TOPMETR:20;

theorem :: TOPALG_2:11
for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is pathwise_connected
proof end;

definition
let T be non empty interval SubSpace of R^1 ;
let P, Q be Function of I[01],T;
func R1Homotopy (P,Q) -> Function of [:I[01],I[01]:],T means :Def4: :: TOPALG_2:def 4
 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 Def4 defines R1Homotopy TOPALG_2:def 4 :
for T being non empty interval SubSpace of R^1
for P, Q being Function of I[01],T
for b4 being Function of [:I[01],I[01]:],T holds
( b4 = R1Homotopy (P,Q) iff for s, t being Element of I[01] holds b4 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) );

Lm8: for T being non empty interval SubSpace of R^1
for P, Q being continuous Function of I[01],T holds R1Homotopy (P,Q) is continuous
proof end;

Lm9: for T being non empty interval 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 Th12: :: TOPALG_2:12
for T being non empty interval 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;

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

theorem Th13: :: TOPALG_2:13
for T being non empty interval 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 interval 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:14
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:15
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:16
for x, y being Point of I[01]
for P, Q being Path of x,y holds P,Q are_homotopic by Th10, Th12;

theorem :: TOPALG_2:17
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 Th10, Th13;

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

registration
let n be Element of NAT ;
let T be non empty convex SubSpace of TOP-REAL n;
let P, Q be continuous Function of I[01],T;
cluster ConvexHomotopy (P,Q) -> continuous ;
coherence
ConvexHomotopy (P,Q) is continuous by Lm5;
end;

theorem :: TOPALG_2:18
for n being Element of 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 Homotopy of P,Q
proof end;

registration
let T be non empty interval SubSpace of R^1 ;
let P, Q be continuous Function of I[01],T;
cluster R1Homotopy (P,Q) -> continuous ;
coherence
R1Homotopy (P,Q) is continuous by Lm8;
end;

theorem :: TOPALG_2:19
for T being non empty interval SubSpace of R^1
for a, b being Point of T
for P, Q being Path of a,b holds R1Homotopy (P,Q) is Homotopy of P,Q
proof end;