:: by Artur Korni{\l}owicz , Yasunari Shidama and Adam Grabowski

::

:: Received March 18, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

theorem :: TOPALG_1:1

theorem Th7: :: TOPALG_1:7

for x being Real

for f, g being real-valued FinSequence holds x * (f - g) = (x * f) - (x * g) by RFUNCT_1:18;

for f, g being real-valued FinSequence holds x * (f - g) = (x * f) - (x * g) by RFUNCT_1:18;

theorem Th10: :: TOPALG_1:10

for x being Real

for n being Nat

for f being Element of REAL n st 0 <= x & x <= 1 holds

|.(x * f).| <= |.f.|

for n being Nat

for f being Element of REAL n st 0 <= x & x <= 1 holds

|.(x * f).| <= |.f.|

proof end;

theorem :: TOPALG_1:12

for x, y being Real

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

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

proof end;

theorem Th13: :: TOPALG_1:13

for x, y being Real

for n being Nat

for e1, e2, e5, e6 being Point of (Euclid n)

for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds

dist (e5,e6) < |.y.| * x

for n being Nat

for e1, e2, e5, e6 being Point of (Euclid n)

for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds

dist (e5,e6) < |.y.| * x

proof end;

theorem Th14: :: TOPALG_1:14

for p, q, x, y being Real

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) < (|.x.| * p) + (|.y.| * q)

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) < (|.x.| * p) + (|.y.| * q)

proof end;

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

proof end;

theorem Th15: :: TOPALG_1:15

for y being Real

for n being Nat

for X being non empty TopSpace

for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds

g is continuous

for n being Nat

for X being non empty TopSpace

for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds

g is continuous

proof end;

theorem :: TOPALG_1:16

for x, y being Real

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 = (x * (f1 . p)) + (y * (f2 . p)) ) holds

g is continuous

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 = (x * (f1 . p)) + (y * (f2 . p)) ) holds

g is continuous

proof end;

theorem Th17: :: TOPALG_1:17

for n being Nat

for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n)

for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds

F is continuous

for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n)

for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds

F is continuous

proof end;

theorem Th18: :: TOPALG_1:18

for n being Nat

for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n)

for i being Point of I[01] holds F . (x,i) = i * x ) holds

F is continuous

for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n)

for i being Point of I[01] holds F . (x,i) = i * x ) holds

F is continuous

proof end;

theorem Th19: :: TOPALG_1:19

for X being non empty TopSpace

for a, b, c being Point of X st a,b are_connected & b,c are_connected holds

for A1, A2 being Path of a,b

for B being Path of b,c st A1,A2 are_homotopic holds

A1,(A2 + B) + (- B) are_homotopic

for a, b, c being Point of X st a,b are_connected & b,c are_connected holds

for A1, A2 being Path of a,b

for B being Path of b,c st A1,A2 are_homotopic holds

A1,(A2 + B) + (- B) are_homotopic

proof end;

theorem :: TOPALG_1:20

for T being non empty pathwise_connected TopSpace

for a1, b1, c1 being Point of T

for A1, A2 being Path of a1,b1

for B being Path of b1,c1 st A1,A2 are_homotopic holds

A1,(A2 + B) + (- B) are_homotopic

for a1, b1, c1 being Point of T

for A1, A2 being Path of a1,b1

for B being Path of b1,c1 st A1,A2 are_homotopic holds

A1,(A2 + B) + (- B) are_homotopic

proof end;

theorem Th21: :: TOPALG_1:21

for X being non empty TopSpace

for a, b, c being Point of X st a,b are_connected & c,b are_connected holds

for A1, A2 being Path of a,b

for B being Path of c,b st A1,A2 are_homotopic holds

A1,(A2 + (- B)) + B are_homotopic

for a, b, c being Point of X st a,b are_connected & c,b are_connected holds

for A1, A2 being Path of a,b

for B being Path of c,b st A1,A2 are_homotopic holds

A1,(A2 + (- B)) + B are_homotopic

proof end;

theorem :: TOPALG_1:22

for T being non empty pathwise_connected TopSpace

for a1, b1, c1 being Point of T

for A1, A2 being Path of a1,b1

for B being Path of c1,b1 st A1,A2 are_homotopic holds

A1,(A2 + (- B)) + B are_homotopic

for a1, b1, c1 being Point of T

for A1, A2 being Path of a1,b1

for B being Path of c1,b1 st A1,A2 are_homotopic holds

A1,(A2 + (- B)) + B are_homotopic

proof end;

theorem Th23: :: TOPALG_1:23

for X being non empty TopSpace

for a, b, c being Point of X st a,b are_connected & c,a are_connected holds

for A1, A2 being Path of a,b

for B being Path of c,a st A1,A2 are_homotopic holds

A1,((- B) + B) + A2 are_homotopic

for a, b, c being Point of X st a,b are_connected & c,a are_connected holds

for A1, A2 being Path of a,b

for B being Path of c,a st A1,A2 are_homotopic holds

A1,((- B) + B) + A2 are_homotopic

proof end;

theorem :: TOPALG_1:24

for T being non empty pathwise_connected TopSpace

for a1, b1, c1 being Point of T

for A1, A2 being Path of a1,b1

for B being Path of c1,a1 st A1,A2 are_homotopic holds

A1,((- B) + B) + A2 are_homotopic

for a1, b1, c1 being Point of T

for A1, A2 being Path of a1,b1

for B being Path of c1,a1 st A1,A2 are_homotopic holds

A1,((- B) + B) + A2 are_homotopic

proof end;

theorem Th25: :: TOPALG_1:25

for X being non empty TopSpace

for a, b, c being Point of X st a,b are_connected & a,c are_connected holds

for A1, A2 being Path of a,b

for B being Path of a,c st A1,A2 are_homotopic holds

A1,(B + (- B)) + A2 are_homotopic

for a, b, c being Point of X st a,b are_connected & a,c are_connected holds

for A1, A2 being Path of a,b

for B being Path of a,c st A1,A2 are_homotopic holds

A1,(B + (- B)) + A2 are_homotopic

proof end;

theorem :: TOPALG_1:26

for T being non empty pathwise_connected TopSpace

for a1, b1, c1 being Point of T

for A1, A2 being Path of a1,b1

for B being Path of a1,c1 st A1,A2 are_homotopic holds

A1,(B + (- B)) + A2 are_homotopic

for a1, b1, c1 being Point of T

for A1, A2 being Path of a1,b1

for B being Path of a1,c1 st A1,A2 are_homotopic holds

A1,(B + (- B)) + A2 are_homotopic

proof end;

theorem Th27: :: TOPALG_1:27

for X being non empty TopSpace

for a, b, c being Point of X st a,b are_connected & c,b are_connected holds

for A, B being Path of a,b

for C being Path of b,c st A + C,B + C are_homotopic holds

A,B are_homotopic

for a, b, c being Point of X st a,b are_connected & c,b are_connected holds

for A, B being Path of a,b

for C being Path of b,c st A + C,B + C are_homotopic holds

A,B are_homotopic

proof end;

theorem :: TOPALG_1:28

for T being non empty pathwise_connected TopSpace

for a1, b1, c1 being Point of T

for A, B being Path of a1,b1

for C being Path of b1,c1 st A + C,B + C are_homotopic holds

A,B are_homotopic

for a1, b1, c1 being Point of T

for A, B being Path of a1,b1

for C being Path of b1,c1 st A + C,B + C are_homotopic holds

A,B are_homotopic

proof end;

theorem Th29: :: TOPALG_1:29

for X being non empty TopSpace

for a, b, c being Point of X st a,b are_connected & a,c are_connected holds

for A, B being Path of a,b

for C being Path of c,a st C + A,C + B are_homotopic holds

A,B are_homotopic

for a, b, c being Point of X st a,b are_connected & a,c are_connected holds

for A, B being Path of a,b

for C being Path of c,a st C + A,C + B are_homotopic holds

A,B are_homotopic

proof end;

theorem :: TOPALG_1:30

for T being non empty pathwise_connected TopSpace

for a1, b1, c1 being Point of T

for A, B being Path of a1,b1

for C being Path of c1,a1 st C + A,C + B are_homotopic holds

A,B are_homotopic

for a1, b1, c1 being Point of T

for A, B being Path of a1,b1

for C being Path of c1,a1 st C + A,C + B are_homotopic holds

A,B are_homotopic

proof end;

theorem Th31: :: TOPALG_1:31

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

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

proof end;

theorem :: TOPALG_1:32

for T being non empty pathwise_connected TopSpace

for a1, b1, c1, d1, e1 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 holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic

for a1, b1, c1, d1, e1 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 holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic

proof end;

theorem Th33: :: TOPALG_1:33

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

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

proof end;

theorem :: TOPALG_1:34

for T being non empty pathwise_connected TopSpace

for a1, b1, c1, d1, e1 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 holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic

for a1, b1, c1, d1, e1 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 holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic

proof end;

theorem Th35: :: TOPALG_1:35

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

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

proof end;

theorem :: TOPALG_1:36

for T being non empty pathwise_connected TopSpace

for a1, b1, c1, d1, e1 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 holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic

for a1, b1, c1, d1, e1 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 holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic

proof end;

theorem Th37: :: TOPALG_1:37

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

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

proof end;

theorem :: TOPALG_1:38

for T being non empty pathwise_connected TopSpace

for a1, b1, c1, d1 being Point of T

for A being Path of a1,b1

for B being Path of d1,b1

for C being Path of b1,c1 holds ((A + (- B)) + B) + C,A + C are_homotopic

for a1, b1, c1, d1 being Point of T

for A being Path of a1,b1

for B being Path of d1,b1

for C being Path of b1,c1 holds ((A + (- B)) + B) + C,A + C are_homotopic

proof end;

theorem Th39: :: TOPALG_1:39

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

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

proof end;

theorem :: TOPALG_1:40

for T being non empty pathwise_connected TopSpace

for a1, b1, c1, d1 being Point of T

for A being Path of a1,b1

for B being Path of c1,d1

for C being Path of a1,c1 holds (((A + (- A)) + C) + B) + (- B),C are_homotopic

for a1, b1, c1, d1 being Point of T

for A being Path of a1,b1

for B being Path of c1,d1

for C being Path of a1,c1 holds (((A + (- A)) + C) + B) + (- B),C are_homotopic

proof end;

theorem Th41: :: TOPALG_1:41

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

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

proof end;

theorem :: TOPALG_1:42

for T being non empty pathwise_connected TopSpace

for a1, b1, c1, d1 being Point of T

for A being Path of a1,b1

for B being Path of c1,d1

for C being Path of a1,c1 holds (A + (((- A) + C) + B)) + (- B),C are_homotopic

for a1, b1, c1, d1 being Point of T

for A being Path of a1,b1

for B being Path of c1,d1

for C being Path of a1,c1 holds (A + (((- A) + C) + B)) + (- B),C are_homotopic

proof end;

theorem Th43: :: TOPALG_1:43

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

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

proof end;

theorem :: TOPALG_1:44

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

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

proof end;

definition

let T be non empty TopStruct ;

let t1, t2 be Point of T;

defpred S_{1}[ object ] means $1 is Path of t1,t2;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff x is Path of t1,t2 )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff x is Path of t1,t2 ) ) & ( for x being object holds

( x in b_{2} iff x is Path of t1,t2 ) ) holds

b_{1} = b_{2}

end;
let t1, t2 be Point of T;

defpred S

func Paths (t1,t2) -> set means :Def1: :: TOPALG_1:def 1

for x being object holds

( x in it iff x is Path of t1,t2 );

existence for x being object holds

( x in it iff x is Path of t1,t2 );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines Paths TOPALG_1:def 1 :

for T being non empty TopStruct

for t1, t2 being Point of T

for b_{4} being set holds

( b_{4} = Paths (t1,t2) iff for x being object holds

( x in b_{4} iff x is Path of t1,t2 ) );

for T being non empty TopStruct

for t1, t2 being Point of T

for b

( b

( x in b

registration

let T be non empty TopStruct ;

let t1, t2 be Point of T;

coherence

not Paths (t1,t2) is empty

end;
let t1, t2 be Point of T;

coherence

not Paths (t1,t2) is empty

proof end;

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

for T being non empty TopStruct

for t being Point of T holds Loops t = Paths (t,t);

registration
end;

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 object 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 ) ) )

proof end;

definition

let X be non empty TopSpace;

let a, b be Point of X;

assume A1: a,b are_connected ;

ex b_{1} being Relation of (Paths (a,b)) st

for P, Q being Path of a,b holds

( [P,Q] in b_{1} iff P,Q are_homotopic )

for b_{1}, b_{2} being Relation of (Paths (a,b)) st ( for P, Q being Path of a,b holds

( [P,Q] in b_{1} iff P,Q are_homotopic ) ) & ( for P, Q being Path of a,b holds

( [P,Q] in b_{2} iff P,Q are_homotopic ) ) holds

b_{1} = b_{2}

end;
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: :: TOPALG_1:def 3

for P, Q being Path of a,b holds

( [P,Q] in it iff P,Q are_homotopic );

existence for P, Q being Path of a,b holds

( [P,Q] in it iff P,Q are_homotopic );

ex b

for P, Q being Path of a,b holds

( [P,Q] in b

proof end;

uniqueness for b

( [P,Q] in b

( [P,Q] in b

b

proof 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 b_{4} being Relation of (Paths (a,b)) holds

( b_{4} = EqRel (X,a,b) iff for P, Q being Path of a,b holds

( [P,Q] in b_{4} iff P,Q are_homotopic ) );

for X being non empty TopSpace

for a, b being Point of X st a,b are_connected holds

for b

( b

( [P,Q] in b

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 )

proof end;

theorem Th45: :: TOPALG_1:45

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

( Q in Class ((EqRel (X,a,b)),P) iff P,Q are_homotopic )

for a, b being Point of X st a,b are_connected holds

for P, Q being Path of a,b holds

( Q in Class ((EqRel (X,a,b)),P) iff P,Q are_homotopic )

proof end;

theorem Th46: :: TOPALG_1:46

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 )

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 )

proof end;

definition
end;

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

for X being non empty TopSpace

for a being Point of X holds EqRel (X,a) = EqRel (X,a,a);

registration

let X be non empty TopSpace;

let a be Point of X;

coherence

( not EqRel (X,a) is empty & EqRel (X,a) is total & EqRel (X,a) is symmetric & EqRel (X,a) is transitive ) by Lm3;

end;
let a be Point of X;

coherence

( not EqRel (X,a) is empty & EqRel (X,a) is total & EqRel (X,a) is symmetric & EqRel (X,a) is transitive ) by Lm3;

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;

ex b_{1} being strict multMagma st

( the carrier of b_{1} = Class (EqRel (X,a)) & ( for x, y being Element of b_{1} ex P, Q being Loop of a st

( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b_{1} . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) )

for b_{1}, b_{2} being strict multMagma st the carrier of b_{1} = Class (EqRel (X,a)) & ( for x, y being Element of b_{1} ex P, Q being Loop of a st

( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b_{1} . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) & the carrier of b_{2} = Class (EqRel (X,a)) & ( for x, y being Element of b_{2} ex P, Q being Loop of a st

( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b_{2} . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) holds

b_{1} = b_{2}

end;
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: :: TOPALG_1:def 5

( 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 ( 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)) ) ) );

ex b

( the carrier of b

( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b

proof end;

uniqueness for b

( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b

( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b

b

proof end;

:: deftheorem Def5 defines FundamentalGroup TOPALG_1:def 5 :

for X being non empty TopSpace

for a being Point of X

for b_{3} being strict multMagma holds

( b_{3} = FundamentalGroup (X,a) iff ( the carrier of b_{3} = Class (EqRel (X,a)) & ( for x, y being Element of b_{3} ex P, Q being Loop of a st

( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b_{3} . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) ) );

for X being non empty TopSpace

for a being Point of X

for b

( b

( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b

notation
end;

registration
end;

theorem Th47: :: TOPALG_1:47

for X being non empty TopSpace

for a being Point of X

for x being set holds

( x in the carrier of (pi_1 (X,a)) iff ex P being Loop of a st x = Class ((EqRel (X,a)),P) )

for a being Point of X

for x being set holds

( x in the carrier of (pi_1 (X,a)) iff ex P being Loop of a st x = Class ((EqRel (X,a)),P) )

proof end;

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

proof end;

registration

let X be non empty TopSpace;

let a be Point of X;

coherence

( pi_1 (X,a) is associative & pi_1 (X,a) is Group-like )

end;
let a be Point of X;

coherence

( pi_1 (X,a) is associative & pi_1 (X,a) is Group-like )

proof end;

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 ;

ex b_{1} being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) st

for Q being Loop of x1 holds b_{1} . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P)))

for b_{1}, b_{2} being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) st ( for Q being Loop of x1 holds b_{1} . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) & ( for Q being Loop of x1 holds b_{2} . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) holds

b_{1} = b_{2}

end;
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: :: TOPALG_1:def 6

for Q being Loop of x1 holds it . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P)));

existence for Q being Loop of x1 holds it . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P)));

ex b

for Q being Loop of x1 holds b

proof end;

uniqueness for b

b

proof 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 b_{5} being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) holds

( b_{5} = pi_1-iso P iff for Q being Loop of x1 holds b_{5} . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) );

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 b

( b

theorem Th48: :: TOPALG_1:48

for X being non empty TopSpace

for x0, x1 being Point of X

for P, Q being Path of x0,x1 st x0,x1 are_connected & P,Q are_homotopic holds

pi_1-iso P = pi_1-iso Q

for x0, x1 being Point of X

for P, Q being Path of x0,x1 st x0,x1 are_connected & P,Q are_homotopic holds

pi_1-iso P = pi_1-iso Q

proof end;

theorem :: TOPALG_1:49

for T being non empty pathwise_connected TopSpace

for y0, y1 being Point of T

for R, V being Path of y0,y1 st R,V are_homotopic holds

pi_1-iso R = pi_1-iso V by Th48, BORSUK_2:def 3;

for y0, y1 being Point of T

for R, V being Path of y0,y1 st R,V are_homotopic holds

pi_1-iso R = pi_1-iso V by Th48, BORSUK_2:def 3;

theorem Th50: :: TOPALG_1:50

for X being non empty TopSpace

for x0, x1 being Point of X

for P being Path of x0,x1 st x0,x1 are_connected holds

pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0))

for x0, x1 being Point of X

for P being Path of x0,x1 st x0,x1 are_connected holds

pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0))

proof end;

registration

let T be non empty pathwise_connected TopSpace;

let x0, x1 be Point of T;

let P be Path of x0,x1;

coherence

pi_1-iso P is multiplicative by Th50, BORSUK_2:def 3;

end;
let x0, x1 be Point of T;

let P be Path of x0,x1;

coherence

pi_1-iso P is multiplicative by Th50, BORSUK_2:def 3;

theorem Th51: :: TOPALG_1:51

for X being non empty TopSpace

for x0, x1 being Point of X

for P being Path of x0,x1 st x0,x1 are_connected holds

pi_1-iso P is one-to-one

for x0, x1 being Point of X

for P being Path of x0,x1 st x0,x1 are_connected holds

pi_1-iso P is one-to-one

proof end;

theorem Th52: :: TOPALG_1:52

for X being non empty TopSpace

for x0, x1 being Point of X

for P being Path of x0,x1 st x0,x1 are_connected holds

pi_1-iso P is onto

for x0, x1 being Point of X

for P being Path of x0,x1 st x0,x1 are_connected holds

pi_1-iso P is onto

proof end;

registration

let T be non empty pathwise_connected TopSpace;

let x0, x1 be Point of T;

let P be Path of x0,x1;

coherence

( pi_1-iso P is one-to-one & pi_1-iso P is onto ) by Th51, Th52, BORSUK_2:def 3;

end;
let x0, x1 be Point of T;

let P be Path of x0,x1;

coherence

( pi_1-iso P is one-to-one & pi_1-iso P is onto ) by Th51, Th52, BORSUK_2:def 3;

theorem Th53: :: TOPALG_1:53

for X being non empty TopSpace

for x0, x1 being Point of X

for P being Path of x0,x1 st x0,x1 are_connected holds

(pi_1-iso P) " = pi_1-iso (- P)

for x0, x1 being Point of X

for P being Path of x0,x1 st x0,x1 are_connected holds

(pi_1-iso P) " = pi_1-iso (- P)

proof end;

theorem :: TOPALG_1:54

theorem :: TOPALG_1:56

theorem :: TOPALG_1:57

for X being non empty TopSpace

for x0, x1 being Point of X st x0,x1 are_connected holds

pi_1 (X,x0), pi_1 (X,x1) are_isomorphic

for x0, x1 being Point of X st x0,x1 are_connected holds

pi_1 (X,x0), pi_1 (X,x1) are_isomorphic

proof end;

theorem :: TOPALG_1:58

for T being non empty pathwise_connected TopSpace

for y0, y1 being Point of T holds pi_1 (T,y0), pi_1 (T,y1) are_isomorphic

for y0, y1 being Point of T holds pi_1 (T,y0), pi_1 (T,y1) are_isomorphic

proof end;

definition

let n be Nat;

let P, Q be Function of I[01],(TOP-REAL n);

ex b_{1} being Function of [:I[01],I[01]:],(TOP-REAL n) st

for s, t being Element of I[01] holds b_{1} . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))

for b_{1}, b_{2} being Function of [:I[01],I[01]:],(TOP-REAL n) st ( for s, t being Element of I[01] holds b_{1} . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds b_{2} . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) holds

b_{1} = b_{2}

end;
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: :: TOPALG_1:def 7

for s, t being Element of I[01] holds it . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s));

existence for s, t being Element of I[01] holds it . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s));

ex b

for s, t being Element of I[01] holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being Function of [:I[01],I[01]:],(TOP-REAL n) holds

( b_{4} = RealHomotopy (P,Q) iff for s, t being Element of I[01] holds b_{4} . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) );

for n being Nat

for P, Q being Function of I[01],(TOP-REAL n)

for b

( b

Lm5: for n being Nat

for P, Q being continuous Function of I[01],(TOP-REAL n) holds RealHomotopy (P,Q) is continuous

proof end;

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

proof end;

theorem Th59: :: TOPALG_1:59

for n being Nat

for a, b being Point of (TOP-REAL n)

for P, Q being Path of a,b holds P,Q are_homotopic

for a, b being Point of (TOP-REAL n)

for P, Q being Path of a,b holds P,Q are_homotopic

proof end;

registration

let n be Nat;

let a, b be Point of (TOP-REAL n);

let P, Q be Path of a,b;

coherence

for b_{1} being Homotopy of P,Q holds b_{1} is continuous

end;
let a, b be Point of (TOP-REAL n);

let P, Q be Path of a,b;

coherence

for b

proof end;

theorem Th60: :: TOPALG_1:60

for n being Nat

for a being Point of (TOP-REAL n)

for C being Loop of a holds the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))}

for a being Point of (TOP-REAL n)

for C being Loop of a holds the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))}

proof end;

registration
end;

theorem :: TOPALG_1:61

:: Added, AK 5.02.2007

theorem Th62: :: TOPALG_1:62

for X being non empty TopSpace

for a being Point of X

for C being constant Loop of a holds 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C)

for a being Point of X

for C being constant Loop of a holds 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C)

proof end;

theorem :: TOPALG_1:63

for X being non empty TopSpace

for a being Point of X

for x, y being Element of (pi_1 (X,a))

for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds

x " = y

for a being Point of X

for x, y being Element of (pi_1 (X,a))

for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds

x " = y

proof end;

registration

let n be Nat;

let P, Q be continuous Function of I[01],(TOP-REAL n);

coherence

RealHomotopy (P,Q) is continuous by Lm5;

end;
let P, Q be continuous Function of I[01],(TOP-REAL n);

coherence

RealHomotopy (P,Q) is continuous by Lm5;

theorem :: TOPALG_1:64

for n being Nat

for a, b being Point of (TOP-REAL n)

for P, Q being Path of a,b holds RealHomotopy (P,Q) is Homotopy of P,Q

for a, b being Point of (TOP-REAL n)

for P, Q being Path of a,b holds RealHomotopy (P,Q) is Homotopy of P,Q

proof end;

theorem :: TOPALG_1:65