let r be positive real number ; :: thesis: for o being Point of (TOP-REAL 2)
for Y being non empty SubSpace of Tdisk o,r st Y = Tcircle o,r holds
not Y is_a_retract_of Tdisk o,r
let o be Point of (TOP-REAL 2); :: thesis: for Y being non empty SubSpace of Tdisk o,r st Y = Tcircle o,r holds
not Y is_a_retract_of Tdisk o,r
let Y be non empty SubSpace of Tdisk o,r; :: thesis: ( Y = Tcircle o,r implies not Y is_a_retract_of Tdisk o,r )
assume A1:
Y = Tcircle o,r
; :: thesis: not Y is_a_retract_of Tdisk o,r
set X = Tdisk o,r;
given R being continuous Function of (Tdisk o,r),Y such that A2:
R is being_a_retraction
; :: according to BORSUK_1:def 20 :: thesis: contradiction
A3:
the carrier of (Tcircle o,r) = Sphere o,r
by TOPREALB:9;
A4:
Sphere o,r c= cl_Ball o,r
by TOPREAL9:17;
consider y0 being Point of Y;
y0 in the carrier of Y
;
then reconsider x0 = y0 as Point of (Tdisk o,r) by A1, A3, A4, Th3;
consider C being constant Loop of x0;
A5: C =
I[01] --> x0
by BORSUK_2:6
.=
the carrier of I[01] --> y0
;
then reconsider D = C as Function of I[01] ,Y ;
A6:
D = I[01] --> y0
by A5;
reconsider a0 = 0 , a1 = 1 as Point of I[01] by BORSUK_1:def 17, BORSUK_1:def 18;
A7:
y0,y0 are_connected
;
( D . a0 = y0 & D . a1 = y0 )
by A5, FUNCOP_1:13;
then reconsider D = D as constant Loop of y0 by A6, A7, BORSUK_2:def 2;
reconsider z0 = y0 as Point of (Tcircle o,r) by A1;
the carrier of (pi_1 Y,y0) = {(Class (EqRel Y,y0),D)}
proof
set E =
EqRel Y,
y0;
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: {(Class (EqRel Y,y0),D)} c= the carrier of (pi_1 Y,y0)
let x be
set ;
:: thesis: ( x in the carrier of (pi_1 Y,y0) implies x in {(Class (EqRel Y,y0),D)} )assume
x in the
carrier of
(pi_1 Y,y0)
;
:: thesis: x in {(Class (EqRel Y,y0),D)}then consider f0 being
Loop of
y0 such that A9:
x = Class (EqRel Y,y0),
f0
by TOPALG_1:48;
reconsider g0 =
f0 as
Loop of
x0 by TOPALG_2:1;
g0,
C are_homotopic
by TOPALG_2:2;
then consider f being
Function of
[:I[01] ,I[01] :],
(Tdisk o,r) such that A10:
f is
continuous
and A11:
for
s being
Point of
I[01] holds
(
f . s,
0 = g0 . s &
f . s,1
= C . s & ( for
t being
Point of
I[01] holds
(
f . 0 ,
t = x0 &
f . 1,
t = x0 ) ) )
by BORSUK_2:def 7;
f0,
D are_homotopic
proof
take F =
R * f;
:: according to BORSUK_2:def 7 :: thesis: ( F is continuous & ( for b1 being Element of the carrier of K704() holds
( F . b1,0 = f0 . b1 & F . b1,1 = D . b1 & F . 0 ,b1 = y0 & F . 1,b1 = y0 ) ) )
thus
F is
continuous
by A10;
:: thesis: for b1 being Element of the carrier of K704() holds
( F . b1,0 = f0 . b1 & F . b1,1 = D . b1 & F . 0 ,b1 = y0 & F . 1,b1 = y0 )
let s be
Point of
I[01] ;
:: thesis: ( F . s,0 = f0 . s & F . s,1 = D . s & F . 0 ,s = y0 & F . 1,s = y0 )
thus F . s,
0 =
F . [s,a0]
.=
R . (f . s,0 )
by FUNCT_2:21
.=
R . (g0 . s)
by A11
.=
f0 . s
by A2, BORSUK_1:def 19
;
:: thesis: ( F . s,1 = D . s & F . 0 ,s = y0 & F . 1,s = y0 )
thus F . s,1 =
F . [s,a1]
.=
R . (f . s,1)
by FUNCT_2:21
.=
R . (C . s)
by A11
.=
D . s
by A2, BORSUK_1:def 19
;
:: thesis: ( F . 0 ,s = y0 & F . 1,s = y0 )
thus F . 0 ,
s =
F . [a0,s]
.=
R . (f . 0 ,s)
by FUNCT_2:21
.=
R . x0
by A11
.=
y0
by A2, BORSUK_1:def 19
;
:: thesis: F . 1,s = y0
thus F . 1,
s =
F . [a1,s]
.=
R . (f . 1,s)
by FUNCT_2:21
.=
R . x0
by A11
.=
y0
by A2, BORSUK_1:def 19
;
:: thesis: verum
end; then
x = Class (EqRel Y,y0),
D
by A9, TOPALG_1:47;
hence
x in {(Class (EqRel Y,y0),D)}
by TARSKI:def 1;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {(Class (EqRel Y,y0),D)} or x in the carrier of (pi_1 Y,y0) )
assume
x in {(Class (EqRel Y,y0),D)}
;
:: thesis: x in the carrier of (pi_1 Y,y0)
then A12:
x = Class (EqRel Y,y0),
D
by TARSKI:def 1;
D in Loops y0
by TOPALG_1:def 1;
then
x in Class (EqRel Y,y0)
by A12, EQREL_1:def 5;
hence
x in the
carrier of
(pi_1 Y,y0)
by TOPALG_1:def 3;
:: thesis: verum
end;
hence
contradiction
by A1; :: thesis: verum