environ
vocabularies HIDDEN, NUMBERS, EUCLID, CARD_1, STRUCT_0, BORSUK_1, TOPMETR, TARSKI, ZFMISC_1, PRE_TOPC, SUBSET_1, RELAT_1, ARYTM_1, XXREAL_0, ARYTM_3, GR_CY_1, FINSET_1, ORDINAL1, METRIC_1, XXREAL_1, XBOOLE_0, REAL_1, RLVECT_3, PBOOLE, FUNCT_1, CARD_3, RELAT_2, PCOMPS_1, FRECHET, CONNSP_1, CONNSP_3, RCOMP_1, CONNSP_2, TOPS_1, TOPS_2, ORDINAL2, T_0TOPSP, CANTOR_1, SETFAM_1, GRAPH_1, BORSUK_6, TOPREALB, SUPINF_2, SIN_COS, COMPLEX1, SQUARE_1, MCART_1, INT_1, ALGSTR_1, TAXONOM2, TEX_2, RCOMP_3, FINSEQ_1, FUNCT_4, COMPTS_1, FUNCOP_1, BORSUK_2, TOPALG_1, EQREL_1, WAYBEL20, TOPALG_2, GROUP_6, ALGSTR_0, JGRAPH_2, FUNCT_2, WELLORD1, TOPREAL2, TOPALG_5, MSSUBFAM, MEASURE5, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, RELAT_1, EQREL_1, FUNCT_1, PBOOLE, CARD_3, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, INT_1, NAT_1, SEQM_3, FINSEQ_1, FUNCT_4, RCOMP_1, DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC, TOPS_1, GR_CY_1, GROUP_6, METRIC_1, CANTOR_1, YELLOW_8, BORSUK_1, TOPS_2, COMPTS_1, CONNSP_1, CONNSP_2, CONNSP_3, TEX_2, TSEP_1, TOPMETR, EUCLID, PCOMPS_1, FRECHET, BORSUK_2, SIN_COS, BORSUK_3, FCONT_1, TAXONOM2, BORSUK_6, TOPALG_1, TOPREAL9, TOPALG_2, TOPREALB, RCOMP_3, XXREAL_0;
definitions FUNCT_1, FUNCT_2, GROUP_6, TOPS_2, TSEP_1, BORSUK_2, TARSKI, XBOOLE_0, CONNSP_1, T_0TOPSP, CONNSP_2, RCOMP_3, SETFAM_1;
theorems GROUP_6, PRE_TOPC, XREAL_0, FUNCT_2, BORSUK_1, INT_1, SIN_COS, EUCLID, JGRAPH_1, SQUARE_1, TOPREAL9, TOPALG_1, TOPS_2, BORSUK_3, FUNCT_1, TOPMETR, JGRAPH_2, BORSUK_4, RELAT_1, FUNCOP_1, FCONT_1, BORSUK_6, BORSUK_2, TOPALG_2, BINOP_1, TARSKI, ZFMISC_1, FUNCT_4, TSEP_1, XBOOLE_1, COMPLEX2, SETFAM_1, XBOOLE_0, TAXONOM2, FINSEQ_3, NAT_1, SEQM_3, FINSEQ_5, TEX_2, DOMAIN_1, TOPS_1, GOBOARD9, CONNSP_1, TOPALG_3, TOPREALA, TOPREALB, FINSET_1, TOPS_3, CONNSP_3, CONNSP_2, TOPGRP_1, XREAL_1, CANTOR_1, FRECHET, TOPGEN_2, CARD_3, RCOMP_3, XXREAL_0, CARD_1, XXREAL_1, RLVECT_1, JORDAN16, XTUPLE_0;
schemes FUNCT_2, NAT_1, PBOOLE, BINOP_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, METRIC_1, BORSUK_1, TSEP_1, GR_CY_1, MONOID_0, EUCLID, TOPMETR, BORSUK_2, YELLOW13, TOPALG_1, TOPALG_2, TOPALG_3, TOPREALB, RCOMP_3, VALUED_0, XXREAL_2, FRECHET, CONNSP_1, GROUP_6, SQUARE_1, SIN_COS, ORDINAL1;
constructors HIDDEN, SQUARE_1, BINARITH, SIN_COS, TOPS_1, CONNSP_1, FUNCOP_1, COMPTS_1, GRCAT_1, TSEP_1, TEX_2, CANTOR_1, MONOID_0, CONNSP_3, YELLOW_8, TAXONOM2, BORSUK_3, FCONT_1, TOPALG_1, TOPREAL9, TOPREALB, RCOMP_3, BORSUK_6, SEQ_4, FRECHET, GROUP_6, FUNCT_4, REAL_1, BINOP_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities COMPTS_1, BINOP_1, GR_CY_1, STRUCT_0, BORSUK_1, ALGSTR_0, TOPALG_1;
expansions FUNCT_1, FUNCT_2, GROUP_6, TOPS_2, TSEP_1, BORSUK_2, COMPTS_1, TARSKI, XBOOLE_0, CONNSP_1, CONNSP_2;
set o = |[0,0]|;
set I = the carrier of I[01];
set R = the carrier of R^1;
Lm1:
0 in INT
by INT_1:def 1;
Lm2:
0 in the carrier of I[01]
by BORSUK_1:43;
then Lm3:
{0} c= the carrier of I[01]
by ZFMISC_1:31;
Lm4:
0 in {0}
by TARSKI:def 1;
Lm5:
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;
Lm6:
[#] I[01] = the carrier of I[01]
;
Lm7:
I[01] | ([#] I[01]) = I[01]
by TSEP_1:3;
Lm8:
1 - 0 <= 1
;
Lm9:
(3 / 2) - (1 / 2) <= 1
;
theorem Th1:
for
a,
r,
s being
Real st
r <= s holds
for
p being
Point of
(Closed-Interval-MSpace (r,s)) holds
(
Ball (
p,
a)
= [.r,s.] or
Ball (
p,
a)
= [.r,(p + a).[ or
Ball (
p,
a)
= ].(p - a),s.] or
Ball (
p,
a)
= ].(p - a),(p + a).[ )
Lm10:
for T being non empty TopSpace
for S being non empty open SubSpace of T st T is locally_connected holds
TopStruct(# the carrier of S, the topology of S #) is locally_connected
definition
let S,
T,
Y be non
empty TopSpace;
let H be
Function of
[:S,T:],
Y;
let t be
Point of
T;
existence
ex b1 being Function of S,Y st
for s being Point of S holds b1 . s = H . (s,t)
uniqueness
for b1, b2 being Function of S,Y st ( for s being Point of S holds b1 . s = H . (s,t) ) & ( for s being Point of S holds b2 . s = H . (s,t) ) holds
b1 = b2
end;
definition
let S,
T,
Y be non
empty TopSpace;
let H be
Function of
[:S,T:],
Y;
let s be
Point of
S;
existence
ex b1 being Function of T,Y st
for t being Point of T holds b1 . t = H . (s,t)
uniqueness
for b1, b2 being Function of T,Y st ( for t being Point of T holds b1 . t = H . (s,t) ) & ( for t being Point of T holds b2 . t = H . (s,t) ) holds
b1 = b2
end;
set TUC = Tunit_circle 2;
set cS1 = the carrier of (Tunit_circle 2);
Lm12:
dom CircleMap = REAL
by FUNCT_2:def 1, TOPMETR:17;
Lm13:
ex F being Subset-Family of (Tunit_circle 2) st
( F is Cover of (Tunit_circle 2) & F is open & ( for U being Subset of (Tunit_circle 2) st U in F holds
ex D being mutually-disjoint open Subset-Family of R^1 st
( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) )
Lm14:
[#] (Sspace 0[01]) = {0}
by TEX_2:def 2;
Lm15:
for r, s being Real
for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds
not G is empty
theorem Th22:
for
Y being non
empty TopSpace for
F being
Function of
[:Y,I[01]:],
(Tunit_circle 2) for
Ft being
Function of
[:Y,(Sspace 0[01]):],
R^1 st
F is
continuous &
Ft is
continuous &
F | [: the carrier of Y,{0}:] = CircleMap * Ft holds
ex
G being
Function of
[:Y,I[01]:],
R^1 st
(
G is
continuous &
F = CircleMap * G &
G | [: the carrier of Y,{0}:] = Ft & ( for
H being
Function of
[:Y,I[01]:],
R^1 st
H is
continuous &
F = CircleMap * H &
H | [: the carrier of Y,{0}:] = Ft holds
G = H ) )
theorem Th24:
for
x0,
y0 being
Point of
(Tunit_circle 2) for
P,
Q being
Path of
x0,
y0 for
F being
Homotopy of
P,
Q for
xt being
Point of
R^1 st
P,
Q are_homotopic &
xt in CircleMap " {x0} holds
ex
yt being
Point of
R^1 ex
Pt,
Qt being
Path of
xt,
yt ex
Ft being
Homotopy of
Pt,
Qt st
(
Pt,
Qt are_homotopic &
F = CircleMap * Ft &
yt in CircleMap " {y0} & ( for
F1 being
Homotopy of
Pt,
Qt st
F = CircleMap * F1 holds
Ft = F1 ) )
definition
existence
ex b1 being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) st
for n being Integer holds b1 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n))
uniqueness
for b1, b2 being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) st ( for n being Integer holds b1 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) & ( for n being Integer holds b2 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) holds
b1 = b2
end;
Lm16:
for r being positive Real
for o being Point of (TOP-REAL 2)
for x being Point of (Tcircle (o,r)) holds INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic