environ
vocabularies HIDDEN, STRUCT_0, BORSUK_1, ZFMISC_1, CARD_1, PRE_TOPC, FUNCT_1, FUNCT_4, FUNCOP_1, TARSKI, RELAT_1, XBOOLE_0, SUBSET_1, TEX_2, CONNSP_1, RELAT_2, COMPTS_1, ORDINAL2, FUNCT_2, RCOMP_1, T_0TOPSP, BORSUK_2, TOPS_2, EUCLID, TOPREAL2, TOPREAL1, SETFAM_1, TAXONOM2, RLVECT_3, ALGSTR_1, GRAPH_1, BORSUK_6, ARYTM_3, XXREAL_0, ARYTM_1, TOPALG_1, EQREL_1, WAYBEL20, GROUP_6, WELLORD1, TOPALG_3, MSSUBFAM;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, EQREL_1, ORDINAL1, NUMBERS, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, XCMPLX_0, FUNCOP_1, FUNCT_4, STRUCT_0, ALGSTR_0, PRE_TOPC, GROUP_6, BORSUK_1, TOPS_2, COMPTS_1, CONNSP_1, TOPREAL1, TEX_2, TOPREAL2, EUCLID, BORSUK_2, BORSUK_3, TAXONOM2, YELLOW_8, BORSUK_6, TOPALG_1, XXREAL_0;
definitions TARSKI, XBOOLE_0, FUNCT_1, FUNCT_2, GROUP_6, TOPS_2, T_0TOPSP, BORSUK_2, BORSUK_6, CONNSP_1;
theorems GROUP_6, PRE_TOPC, FUNCT_2, BORSUK_1, TOPALG_1, TOPS_2, BORSUK_3, FUNCT_1, TOPMETR, RELAT_1, FUNCOP_1, TOPREAL6, BORSUK_6, BORSUK_2, BINOP_1, TARSKI, PCOMPS_1, ZFMISC_1, FUNCT_4, TSEP_1, XBOOLE_1, TOPREAL1, TOPREAL2, XBOOLE_0, TAXONOM2, TEX_2, CONNSP_1, TDLAT_3, ENUMSET1, YELLOW12, TOPS_3, YELLOW13, YELLOW_8, SETFAM_1;
schemes FUNCT_2;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, XREAL_0, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, BORSUK_1, TEX_1, EUCLID, TOPREAL2, BORSUK_2, TOPALG_1, RELSET_1, TOPMETR, MEMBERED, RELAT_1, GROUP_6, GROUP_1;
constructors HIDDEN, REAL_1, CONNSP_1, TOPS_2, COMPTS_1, GRCAT_1, TDLAT_3, TEX_2, TOPREAL1, TOPREAL2, YELLOW_8, TAXONOM2, BORSUK_3, BORSUK_6, TOPALG_1, FUNCOP_1, GROUP_6, FUNCT_4;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities STRUCT_0, FUNCOP_1, TOPALG_1;
expansions XBOOLE_0, FUNCT_2, TOPS_2, BORSUK_2, CONNSP_1, STRUCT_0;
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 2;
reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def 14, BORSUK_1:def 15;
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 )
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 Th29:
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);
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)) ) );