begin
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;
reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def 17, BORSUK_1:def 18;
theorem
theorem
theorem
canceled;
theorem Th4:
theorem
theorem
theorem Th7:
theorem Th8:
theorem
theorem
theorem
theorem
theorem
begin
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem
theorem
theorem
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 )
theorem
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 )
begin
theorem
theorem Th23:
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
theorem
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
theorem Th30:
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)
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 pT =
pi_1 T,
(f . s);
set pS =
pi_1 S,
s;
func FundGrIso f,
s -> Function of
(pi_1 S,s),
(pi_1 T,(f . s)) means :
Def1:
for
x being
Element of
(pi_1 S,s) ex
ls being
Loop of
s st
(
x = Class (EqRel S,s),
ls &
it . x = Class (EqRel T,(f . s)),
(f * ls) );
existence
ex b1 being Function of (pi_1 S,s),(pi_1 T,(f . s)) st
for x being Element of (pi_1 S,s) ex ls being Loop of s st
( x = Class (EqRel S,s),ls & b1 . x = Class (EqRel T,(f . s)),(f * ls) )
uniqueness
for b1, b2 being Function of (pi_1 S,s),(pi_1 T,(f . s)) st ( for x being Element of (pi_1 S,s) ex ls being Loop of s st
( x = Class (EqRel S,s),ls & b1 . x = Class (EqRel T,(f . s)),(f * ls) ) ) & ( for x being Element of (pi_1 S,s) ex ls being Loop of s st
( x = Class (EqRel S,s),ls & b2 . x = Class (EqRel T,(f . s)),(f * ls) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines FundGrIso TOPALG_3:def 1 :
for
S,
T being non
empty TopSpace for
s being
Point of
S for
f being
Function of
S,
T st
f is
continuous holds
for
b5 being
Function of
(pi_1 S,s),
(pi_1 T,(f . s)) holds
(
b5 = FundGrIso f,
s iff for
x being
Element of
(pi_1 S,s) ex
ls being
Loop of
s st
(
x = Class (EqRel S,s),
ls &
b5 . x = Class (EqRel T,(f . s)),
(f * ls) ) );
theorem
canceled;
theorem
definition
let S,
T be non
empty TopSpace;
let s be
Point of
S;
let f be
continuous Function of
S,
T;
FundGrIsoredefine func FundGrIso f,
s -> Homomorphism of
(pi_1 S,s),
(pi_1 T,(f . s));
coherence
FundGrIso f,s is Homomorphism of (pi_1 S,s),(pi_1 T,(f . s))
end;
theorem Th33:
theorem
theorem