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