:: TOPALG_3 semantic presentation

set I = the carrier of I[01] ;

set R = the carrier of R^1 ;

Lm1: the carrier of [:I[01] ,I[01] :] = [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:def 5;

reconsider j0 = 0, j1 = 1 as Point of I[01] by BORSUK_1:def 17, BORSUK_1:def 18;

theorem :: TOPALG_3:1

for A, B, a, b being set
for f being Function of A,B st a in A & b in B holds
f +* (a .--> b) is Function of A,B

proof end;

theorem :: TOPALG_3:2

for f being Function
for X, x being set st f | X is one-to-one & x in rng (f | X) holds
(f * ((f | X) " )) . x = x

proof end;

theorem Th3: :: TOPALG_3:3

for x, y, X, Y, Z being set
for f being Function of [:X,Y:],Z
for g being Function st Z <> {} & x in X & y in Y holds
(g * f) . x,y = g . (f . x,y)

proof end;

theorem Th4: :: TOPALG_3:4

for X, a, b being set
for f being Function of X,{a,b} holds X = (f " {a}) \/ (f " {b})

proof end;

theorem Th5: :: TOPALG_3:5

for S, T being non empty 1-sorted
for s being Point of S
for t being Point of T holds (S --> t) . s = t

proof end;

theorem :: TOPALG_3:6

for T being non empty TopStruct
for t being Point of T
for A being Subset of T st A = {t} holds
Sspace t = T | A

proof end;

theorem Th7: :: TOPALG_3:7

for T being TopSpace
for A, B being Subset of T
for C, D being Subset of TopStruct(# the carrier of T,the topology of T #) st A = C & B = D holds
( A,B are_separated iff C,D are_separated )

proof end;

theorem Th8: :: TOPALG_3:8

for T being non empty TopSpace holds
( T is connected iff for f being Function of T,(1TopSp {0,1}) holds
( not f is continuous or not f is onto ) )

proof end;

registration

cluster empty -> connected TopStruct ;
coherence

proof end;

end;

theorem :: TOPALG_3:9

for T being TopSpace st TopStruct(# the carrier of T,the topology of T #) is connected holds
T is connected

proof end;

registration

let T be connected TopSpace;
cluster TopStruct(# the carrier of T,the topology of T #) -> connected ;
coherence

proof end;

end;

theorem :: TOPALG_3:10

for S, T being non empty TopSpace st S,T are_homeomorphic & S is arcwise_connected holds
T is arcwise_connected

proof end;

registration

cluster non empty trivial -> non empty arcwise_connected TopStruct ;
coherence

proof end;

end;

theorem :: TOPALG_3:11

for T being SubSpace of TOP-REAL 2 st the carrier of T is Simple_closed_curve holds
T is arcwise_connected

proof end;

theorem :: TOPALG_3:12

for T being TopSpace ex F being Subset-Family of T st
( F = {the carrier of T} & F is_a_cover_of T & F is open )

proof end;

registration

let T be TopSpace;
cluster non empty open closed mutually-disjoint Element of bool (bool the carrier of T);
existence

proof end;

end;

theorem :: TOPALG_3:13

for T being TopSpace
for D being open mutually-disjoint Subset-Family of T
for A being Subset of T
for X being set st A is connected & X in D & X meets A & D is_a_cover_of A holds
A c= X

proof end;

theorem Th14: :: TOPALG_3:14

for S, T being TopSpace holds TopStruct(# the carrier of [:S,T:],the topology of [:S,T:] #) = [:TopStruct(# the carrier of S,the topology of S #),TopStruct(# the carrier of T,the topology of T #):]

proof end;

theorem Th15: :: TOPALG_3:15

for S, T being TopSpace
for A being Subset of S
for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]

proof end;

theorem Th16: :: TOPALG_3:16

for S, T being TopSpace
for A being closed Subset of S
for B being closed Subset of T holds [:A,B:] is closed

proof end;

registration

let A, B be connected TopSpace;
cluster [:A,B:] -> connected ;
coherence

proof end;

end;

theorem :: TOPALG_3:17

for S, T being TopSpace
for A being Subset of S
for B being Subset of T st A is connected & B is connected holds
[:A,B:] is connected

proof end;

theorem :: TOPALG_3:18

for S, T being TopSpace
for Y being non empty TopSpace
for A being Subset of S
for f being Function of [:S,T:],Y
for g being Function of [:(S | A),T:],Y st g = f | [:A,the carrier of T:] & f is continuous holds
g is continuous

proof end;

theorem :: TOPALG_3:19

for S, T being TopSpace
for Y being non empty TopSpace
for A being Subset of T
for f being Function of [:S,T:],Y
for g being Function of [:S,(T | A):],Y st g = f | [:the carrier of S,A:] & f is continuous holds
g is continuous

proof end;

theorem :: TOPALG_3:20

for S, T, T1, T2, Y being non empty TopSpace
for f being Function of [:Y,T1:],S
for g being Function of [:Y,T2:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ) holds
ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous )

proof end;

theorem :: TOPALG_3:21

for S, T, T1, T2, Y being non empty TopSpace
for f being Function of [:T1,Y:],S
for g being Function of [:T2,Y:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds
f . p = g . p ) holds
ex h being Function of [:T,Y:],S st
( h = f +* g & h is continuous )

proof end;

registration

let T be non empty TopSpace;
let t be Point of T;
cluster -> continuous Path of t,t;
coherence

proof end;

end;

theorem :: TOPALG_3:22

for T being non empty TopSpace
for t being Point of T
for x being Point of I[01]
for P being constant Loop of t holds P . x = t

proof end;

theorem Th23: :: TOPALG_3:23

for T being non empty TopSpace
for t being Point of T
for P being Loop of t holds
( P . 0 = t & P . 1 = t )

proof end;

theorem Th24: :: TOPALG_3:24

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S st a,b are_connected holds
f . a,f . b are_connected

proof end;

theorem :: TOPALG_3:25

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P being Path of a,b st a,b are_connected holds
f * P is Path of f . a,f . b

proof end;

theorem :: TOPALG_3:26

for S being non empty arcwise_connected TopSpace
for T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P being Path of a,b holds f * P is Path of f . a,f . b

proof end;

theorem Th27: :: TOPALG_3:27

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a being Point of S
for P being Loop of a holds f * P is Loop of f . a

proof end;

theorem Th28: :: TOPALG_3:28

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
P1,Q1 are_homotopic

proof end;

theorem :: TOPALG_3:29

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b
for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1

proof end;

theorem Th30: :: TOPALG_3:30

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b, c being Point of S
for P being Path of a,b
for Q being Path of b,c
for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)

proof end;

theorem Th31: :: TOPALG_3:31

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;

definition

let S, T be non empty TopSpace;
let s be Point of S;
let f be Function of S,T;
assume A1: f is continuous ;
set pS = pi_1 S,s;
set pT = pi_1 T,(f . s);
func FundGrIso f,s -> Function of (pi_1 S,s),(pi_1 T,(f . s)) means :Def1: :: TOPALG_3:def 1
for x being Element of (pi_1 S,s) ex ls being Loop of s ex lt being Loop of f . s st
( x = Class (EqRel S,s),ls & lt = f * ls & it . x = Class (EqRel T,(f . s)),lt );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines FundGrIso TOPALG_3:def 1 :

theorem :: TOPALG_3:32

for S, T being non empty TopSpace
for s being Point of S
for f being continuous Function of S,T
for x being Element of (pi_1 S,s)
for ls being Loop of s
for lt being Loop of f . s st x = Class (EqRel S,s),ls & lt = f * ls holds
(FundGrIso f,s) . x = Class (EqRel T,(f . s)),lt

proof end;

definition

let S, T be non empty TopSpace;
let s be Point of S;
let f be continuous Function of S,T;
:: original: FundGrIso
redefine func FundGrIso f,s -> Homomorphism of (pi_1 S,s),(pi_1 T,(f . s));
coherence

proof end;

end;

theorem Th33: :: TOPALG_3:33

for S, T being non empty TopSpace
for s being Point of S
for f being continuous Function of S,T st f is_homeomorphism holds
FundGrIso f,s is_isomorphism

proof end;

theorem :: TOPALG_3:34

for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for f being continuous Function of S,T
for P being Path of t,f . s
for h being Homomorphism of (pi_1 S,s),(pi_1 T,t) st f is_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso f,s) holds
h is_isomorphism

proof end;

theorem :: TOPALG_3:35

for S being non empty TopSpace
for T being non empty arcwise_connected TopSpace
for s being Point of S
for t being Point of T st S,T are_homeomorphic holds
pi_1 S,s, pi_1 T,t are_isomorphic

proof end;