begin
theorem
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem
for
x,
y being
real number for
n being
Nat for
e1,
e2,
e3,
e4,
e5,
e6 being
Point of
(Euclid n) for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL n) st
e1 = p1 &
e2 = p2 &
e3 = p3 &
e4 = p4 &
e5 = p1 + p3 &
e6 = p2 + p4 &
dist e1,
e2 < x &
dist e3,
e4 < y holds
dist e5,
e6 < x + y
theorem Th13:
theorem Th14:
for
x,
y,
p,
q being
real number for
n being
Nat for
e1,
e2,
e3,
e4,
e5,
e6 being
Point of
(Euclid n) for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL n) st
e1 = p1 &
e2 = p2 &
e3 = p3 &
e4 = p4 &
e5 = (x * p1) + (y * p3) &
e6 = (x * p2) + (y * p4) &
dist e1,
e2 < p &
dist e3,
e4 < q &
x <> 0 &
y <> 0 holds
dist e5,
e6 < ((abs x) * p) + ((abs y) * q)
Lm1:
for n being Nat
for X being non empty TopSpace
for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (f1 . p) + (f2 . p) ) holds
g is continuous
theorem
canceled;
theorem Th16:
theorem
theorem Th18:
theorem Th19:
begin
theorem Th20:
theorem
theorem Th22:
theorem
theorem Th24:
theorem
theorem Th26:
theorem
theorem Th28:
theorem
theorem Th30:
theorem
theorem Th32:
for
X being non
empty TopSpace for
a,
b,
c,
d,
e being
Point of
X st
a,
b are_connected &
b,
c are_connected &
c,
d are_connected &
d,
e are_connected holds
for
A being
Path of
a,
b for
B being
Path of
b,
c for
C being
Path of
c,
d for
D being
Path of
d,
e holds
((A + B) + C) + D,
(A + (B + C)) + D are_homotopic
theorem
theorem Th34:
for
X being non
empty TopSpace for
a,
b,
c,
d,
e being
Point of
X st
a,
b are_connected &
b,
c are_connected &
c,
d are_connected &
d,
e are_connected holds
for
A being
Path of
a,
b for
B being
Path of
b,
c for
C being
Path of
c,
d for
D being
Path of
d,
e holds
((A + B) + C) + D,
A + ((B + C) + D) are_homotopic
theorem
theorem Th36:
for
X being non
empty TopSpace for
a,
b,
c,
d,
e being
Point of
X st
a,
b are_connected &
b,
c are_connected &
c,
d are_connected &
d,
e are_connected holds
for
A being
Path of
a,
b for
B being
Path of
b,
c for
C being
Path of
c,
d for
D being
Path of
d,
e holds
(A + (B + C)) + D,
(A + B) + (C + D) are_homotopic
theorem
theorem Th38:
for
X being non
empty TopSpace for
a,
b,
c,
d being
Point of
X st
a,
b are_connected &
b,
c are_connected &
b,
d are_connected holds
for
A being
Path of
a,
b for
B being
Path of
d,
b for
C being
Path of
b,
c holds
((A + (- B)) + B) + C,
A + C are_homotopic
theorem
theorem Th40:
for
X being non
empty TopSpace for
a,
b,
c,
d being
Point of
X st
a,
b are_connected &
a,
c are_connected &
c,
d are_connected holds
for
A being
Path of
a,
b for
B being
Path of
c,
d for
C being
Path of
a,
c holds
(((A + (- A)) + C) + B) + (- B),
C are_homotopic
theorem
theorem Th42:
for
X being non
empty TopSpace for
a,
b,
c,
d being
Point of
X st
a,
b are_connected &
a,
c are_connected &
d,
c are_connected holds
for
A being
Path of
a,
b for
B being
Path of
c,
d for
C being
Path of
a,
c holds
(A + (((- A) + C) + B)) + (- B),
C are_homotopic
theorem
theorem Th44:
for
X being non
empty TopSpace for
a,
b,
c,
d,
e,
f being
Point of
X st
a,
b are_connected &
b,
c are_connected &
c,
d are_connected &
d,
e are_connected &
a,
f are_connected holds
for
A being
Path of
a,
b for
B being
Path of
b,
c for
C being
Path of
c,
d for
D being
Path of
d,
e for
E being
Path of
f,
c holds
(A + (B + C)) + D,
((A + B) + (- E)) + ((E + C) + D) are_homotopic
theorem
for
T being non
empty pathwise_connected TopSpace for
a1,
b1,
c1,
d1,
e1,
f1 being
Point of
T for
A being
Path of
a1,
b1 for
B being
Path of
b1,
c1 for
C being
Path of
c1,
d1 for
D being
Path of
d1,
e1 for
E being
Path of
f1,
c1 holds
(A + (B + C)) + D,
((A + B) + (- E)) + ((E + C) + D) are_homotopic
begin
:: deftheorem Def1 defines Paths TOPALG_1:def 1 :
for T being non empty TopStruct
for t1, t2 being Point of T
for b4 being set holds
( b4 = Paths t1,t2 iff for x being set holds
( x in b4 iff x is Path of t1,t2 ) );
:: deftheorem defines Loops TOPALG_1:def 2 :
for T being non empty TopStruct
for t being Point of T holds Loops t = Paths t,t;
Lm2:
for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
ex E being Equivalence_Relation of (Paths a,b) st
for x, y being set holds
( [x,y] in E iff ( x in Paths a,b & y in Paths a,b & ex P, Q being Path of a,b st
( P = x & Q = y & P,Q are_homotopic ) ) )
definition
let X be non
empty TopSpace;
let a,
b be
Point of
X;
assume A1:
a,
b are_connected
;
func EqRel X,
a,
b -> Relation of
(Paths a,b) means :
Def3:
for
P,
Q being
Path of
a,
b holds
(
[P,Q] in it iff
P,
Q are_homotopic );
existence
ex b1 being Relation of (Paths a,b) st
for P, Q being Path of a,b holds
( [P,Q] in b1 iff P,Q are_homotopic )
uniqueness
for b1, b2 being Relation of (Paths a,b) st ( for P, Q being Path of a,b holds
( [P,Q] in b1 iff P,Q are_homotopic ) ) & ( for P, Q being Path of a,b holds
( [P,Q] in b2 iff P,Q are_homotopic ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines EqRel TOPALG_1:def 3 :
for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
for b4 being Relation of (Paths a,b) holds
( b4 = EqRel X,a,b iff for P, Q being Path of a,b holds
( [P,Q] in b4 iff P,Q are_homotopic ) );
Lm3:
for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
( not EqRel X,a,b is empty & EqRel X,a,b is total & EqRel X,a,b is symmetric & EqRel X,a,b is transitive )
theorem Th46:
theorem Th47:
for
X being non
empty TopSpace for
a,
b being
Point of
X st
a,
b are_connected holds
for
P,
Q being
Path of
a,
b holds
(
Class (EqRel X,a,b),
P = Class (EqRel X,a,b),
Q iff
P,
Q are_homotopic )
:: deftheorem defines EqRel TOPALG_1:def 4 :
for X being non empty TopSpace
for a being Point of X holds EqRel X,a = EqRel X,a,a;
definition
let X be non
empty TopSpace;
let a be
Point of
X;
set E =
EqRel X,
a;
set A =
Class (EqRel X,a);
set W =
Loops a;
func FundamentalGroup X,
a -> strict multMagma means :
Def5:
( the
carrier of
it = Class (EqRel X,a) & ( for
x,
y being
Element of
it ex
P,
Q being
Loop of
a st
(
x = Class (EqRel X,a),
P &
y = Class (EqRel X,a),
Q & the
multF of
it . x,
y = Class (EqRel X,a),
(P + Q) ) ) );
existence
ex b1 being strict multMagma st
( the carrier of b1 = Class (EqRel X,a) & ( for x, y being Element of b1 ex P, Q being Loop of a st
( x = Class (EqRel X,a),P & y = Class (EqRel X,a),Q & the multF of b1 . x,y = Class (EqRel X,a),(P + Q) ) ) )
uniqueness
for b1, b2 being strict multMagma st the carrier of b1 = Class (EqRel X,a) & ( for x, y being Element of b1 ex P, Q being Loop of a st
( x = Class (EqRel X,a),P & y = Class (EqRel X,a),Q & the multF of b1 . x,y = Class (EqRel X,a),(P + Q) ) ) & the carrier of b2 = Class (EqRel X,a) & ( for x, y being Element of b2 ex P, Q being Loop of a st
( x = Class (EqRel X,a),P & y = Class (EqRel X,a),Q & the multF of b2 . x,y = Class (EqRel X,a),(P + Q) ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines FundamentalGroup TOPALG_1:def 5 :
for X being non empty TopSpace
for a being Point of X
for b3 being strict multMagma holds
( b3 = FundamentalGroup X,a iff ( the carrier of b3 = Class (EqRel X,a) & ( for x, y being Element of b3 ex P, Q being Loop of a st
( x = Class (EqRel X,a),P & y = Class (EqRel X,a),Q & the multF of b3 . x,y = Class (EqRel X,a),(P + Q) ) ) ) );
theorem Th48:
Lm4:
for S being non empty TopSpace
for s being Point of S
for x, y being Element of (pi_1 S,s)
for P, Q being Loop of s st x = Class (EqRel S,s),P & y = Class (EqRel S,s),Q holds
x * y = Class (EqRel S,s),(P + Q)
definition
let T be non
empty TopSpace;
let x0,
x1 be
Point of
T;
let P be
Path of
x0,
x1;
assume A1:
x0,
x1 are_connected
;
func pi_1-iso P -> Function of
(pi_1 T,x1),
(pi_1 T,x0) means :
Def6:
for
Q being
Loop of
x1 holds
it . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),
((P + Q) + (- P));
existence
ex b1 being Function of (pi_1 T,x1),(pi_1 T,x0) st
for Q being Loop of x1 holds b1 . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + Q) + (- P))
uniqueness
for b1, b2 being Function of (pi_1 T,x1),(pi_1 T,x0) st ( for Q being Loop of x1 holds b1 . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + Q) + (- P)) ) & ( for Q being Loop of x1 holds b2 . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + Q) + (- P)) ) holds
b1 = b2
end;
:: deftheorem Def6 defines pi_1-iso TOPALG_1:def 6 :
for T being non empty TopSpace
for x0, x1 being Point of T
for P being Path of x0,x1 st x0,x1 are_connected holds
for b5 being Function of (pi_1 T,x1),(pi_1 T,x0) holds
( b5 = pi_1-iso P iff for Q being Loop of x1 holds b5 . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + Q) + (- P)) );
theorem Th49:
theorem
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem
theorem Th56:
theorem
theorem
theorem
begin
definition
let n be
Nat;
let P,
Q be
Function of
I[01] ,
(TOP-REAL n);
func RealHomotopy P,
Q -> Function of
[:I[01] ,I[01] :],
(TOP-REAL n) means :
Def7:
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] :],(TOP-REAL n) st
for s, t being Element of I[01] holds b1 . s,t = ((1 - t) * (P . s)) + (t * (Q . s))
uniqueness
for b1, b2 being Function of [:I[01] ,I[01] :],(TOP-REAL n) 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
end;
:: deftheorem Def7 defines RealHomotopy TOPALG_1:def 7 :
for n being Nat
for P, Q being Function of I[01] ,(TOP-REAL n)
for b4 being Function of [:I[01] ,I[01] :],(TOP-REAL n) holds
( b4 = RealHomotopy P,Q iff for s, t being Element of I[01] holds b4 . s,t = ((1 - t) * (P . s)) + (t * (Q . s)) );
Lm5:
for n being Nat
for P, Q being continuous Function of I[01] ,(TOP-REAL n) holds RealHomotopy P,Q is continuous
Lm6:
for n being Nat
for a, b being Point of (TOP-REAL n)
for P, Q being Path of a,b
for s being Point of I[01] holds
( (RealHomotopy P,Q) . s,0 = P . s & (RealHomotopy P,Q) . s,1 = Q . s & ( for t being Point of I[01] holds
( (RealHomotopy P,Q) . 0 ,t = a & (RealHomotopy P,Q) . 1,t = b ) ) )
theorem Th60:
theorem Th61:
theorem
theorem Th63:
theorem
theorem
theorem
for
X being non
empty TopSpace for
a,
b being
Point of
X st
a,
b are_connected holds
( not
EqRel X,
a,
b is
empty &
EqRel X,
a,
b is
total &
EqRel X,
a,
b is
symmetric &
EqRel X,
a,
b is
transitive )
by Lm3;