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

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 arcwise_connected SubSpace of TOP-REAL n;
coherence
for b₁ being non empty SubSpace of TOP-REAL n st b₁ is convex holds
b₁ is arcwise_connected

proof end;

end;

registration

let n be Element of NAT ;
cluster non empty strict 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;

theorem Th4: :: TOPALG_2:4

for a being real number holds Proj |[a]|,1 = a

proof end;

registration

cluster -> real-membered SubSpace of R^1 ;
coherence
for b₁ being SubSpace of R^1 holds b₁ is real-membered ;

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;

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 b₁ being Subset of R^1 st
( not b₁ is empty & b₁ is convex )

proof end;

cluster empty -> convex Element of bool the carrier of R^1 ;
coherence
for b₁ being Subset of R^1 st b₁ is empty holds
b₁ is convex

proof end;

end;

theorem Th8: :: TOPALG_2:8

for a, b being real number holds [.a,b.] is convex Subset of R^1

proof end;

theorem :: TOPALG_2:9

for a, b being real number holds ].a,b.[ is convex Subset of R^1

proof end;

theorem :: TOPALG_2:10

for a, b being real number holds [.a,b.[ is convex Subset of R^1

proof end;

theorem :: TOPALG_2:11

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 b₁ being SubSpace of R^1 st
( b₁ is strict & not b₁ is empty & b₁ 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

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

proof end;

end;

theorem Th13: :: TOPALG_2:13

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

proof end;

theorem Th14: :: TOPALG_2:14

I[01] is convex by Th13, TOPMETR:27;

theorem :: TOPALG_2:15

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 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 convex 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 convex 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 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

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;

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

proof end;

end;

theorem Th17: :: TOPALG_2:17

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

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

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

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 :: TOPALG_2:21

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 by Th14;

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

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 convex 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:23

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 Homotopy of P,Q

proof end;