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

begin

registration

let n be Element of NAT ;
cluster non empty convex Element of bool the carrier of (TOP-REAL n);
existence
ex b₁ being Subset of (TOP-REAL n) st
( not b₁ is empty & b₁ 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 SubSpace of TOP-REAL n;
coherence
for b₁ being non empty SubSpace of TOP-REAL n st b₁ is convex holds
b₁ is pathwise_connected

proof end;

end;

registration

let n be Element of NAT ;
cluster non empty strict TopSpace-like convex SubSpace of TOP-REAL n;
existence
ex b₁ being SubSpace of TOP-REAL n st
( b₁ is strict & not b₁ is empty & b₁ 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 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 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 b₁ 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
b₁ . (s,t) = ((1 - t) * a1) + (t * b1)

proof end;

uniqueness
for b₁, b₂ 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
b₁ . (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
b₂ . (s,t) = ((1 - t) * a1) + (t * b1) ) holds
b₁ = b₂

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 b₅ being Function of [:I[01],I[01]:],T holds
( b₅ = 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
b₅ . (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 Homotopy of P,Q;
coherence
for b₁ being Homotopy of P,Q holds b₁ 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 V213() V214() V215() interval Element of bool the carrier of R^1;
existence
ex b₁ being Subset of R^1 st
( not b₁ is empty & b₁ is interval )

proof end;

end;

registration

let T be real-membered TopStruct ;
cluster V213() V214() V215() interval Element of bool the carrier of T;
existence
ex b₁ being Subset of T st b₁ is interval

proof end;

end;

definition

canceled;
let T be real-membered TopStruct ;
attr T is interval means :Def4: :: TOPALG_2:def 4
[#] T is interval ;

end;

:: deftheorem TOPALG_2:def 3 :
canceled;

:: deftheorem Def4 defines interval TOPALG_2:def 4 :
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 SubSpace of R^1 ;
existence
ex b₁ being SubSpace of R^1 st
( b₁ is strict & not b₁ is empty & b₁ 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 :: TOPALG_2:8

canceled;

theorem Th9: :: TOPALG_2:9

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 SubSpace of R^1 ;
coherence
for b₁ being non empty SubSpace of R^1 st b₁ is interval holds
b₁ is pathwise_connected

proof end;

end;

theorem Th10: :: TOPALG_2:10

for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is interval

proof end;

theorem Th11: :: TOPALG_2:11

I[01] is interval by Th10, TOPMETR:27;

theorem :: TOPALG_2:12

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 :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 b₁ being Function of [:I[01],I[01]:],T st
for s, t being Element of I[01] holds b₁ . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))

proof end;

uniqueness
for b₁, b₂ being Function of [:I[01],I[01]:],T st ( for s, t being Element of I[01] holds b₁ . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds b₂ . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines R1Homotopy TOPALG_2:def 5 :
for T being non empty interval SubSpace of R^1
for P, Q being Function of I[01],T
for b₄ being Function of [:I[01],I[01]:],T holds
( b₄ = R1Homotopy (P,Q) iff for s, t being Element of I[01] holds b₄ . (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 Th13: :: TOPALG_2:13

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 Homotopy of P,Q;
coherence
for b₁ being Homotopy of P,Q holds b₁ is continuous

proof end;

end;

theorem Th14: :: TOPALG_2:14

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:15

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:16

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:17

for x, y being Point of I[01]
for P, Q being Path of x,y holds P,Q are_homotopic by Th11, Th13;

theorem :: TOPALG_2:18

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 Th11, Th14;

registration

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

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:19

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:20

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;