let r be positive Real; 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)
set y0 = the Point of Y;
set X = Tdisk (o,r);
A2:
the Point of Y 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 = the Point of Y as Point of (Tdisk (o,r)) by A1, A2, Th3;
reconsider a0 = 0 , a1 = 1 as Point of I[01] by BORSUK_1:def 14, BORSUK_1:def 15;
set C = the constant Loop of x0;
A3: the constant Loop of x0 =
I[01] --> x0
by BORSUK_2:5
.=
the carrier of I[01] --> the Point of Y
;
then reconsider D = the constant Loop of x0 as Function of I[01],Y ;
A4:
( D = I[01] --> the Point of Y & D . a0 = the Point of Y )
by A3, FUNCOP_1:7;
( the Point of Y, the Point of Y are_connected & D . a1 = the Point of Y )
by A3, FUNCOP_1:7;
then reconsider D = D as constant Loop of the Point of Y 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 17 contradiction
the carrier of (pi_1 (Y, the Point of Y)) = {(Class ((EqRel (Y, the Point of Y)),D))}
proof
set E =
EqRel (
Y, the
Point of
Y);
hereby TARSKI:def 3,
XBOOLE_0:def 10 {(Class ((EqRel (Y, the Point of Y)),D))} c= the carrier of (pi_1 (Y, the Point of Y))
let x be
object ;
( x in the carrier of (pi_1 (Y, the Point of Y)) implies x in {(Class ((EqRel (Y, the Point of Y)),D))} )assume
x in the
carrier of
(pi_1 (Y, the Point of Y))
;
x in {(Class ((EqRel (Y, the Point of Y)),D))}then consider f0 being
Loop of the
Point of
Y such that A6:
x = Class (
(EqRel (Y, the Point of Y)),
f0)
by TOPALG_1:47;
reconsider g0 =
f0 as
Loop of
x0 by TOPALG_2:1;
g0, the
constant Loop of
x0 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)
= the
constant Loop of
x0 . s & ( for
t being
Point of
I[01] holds
(
f . (
0,
t)
= x0 &
f . (1,
t)
= x0 ) ) )
;
f0,
D are_homotopic
proof
take F =
R * f;
BORSUK_2:def 7 ( F is continuous & ( for b1 being Element of the carrier of K543() holds
( F . (b1,0) = f0 . b1 & F . (b1,1) = D . b1 & F . (0,b1) = the Point of Y & F . (1,b1) = the Point of Y ) ) )
thus
F is
continuous
by A7;
for b1 being Element of the carrier of K543() holds
( F . (b1,0) = f0 . b1 & F . (b1,1) = D . b1 & F . (0,b1) = the Point of Y & F . (1,b1) = the Point of Y )
let s be
Point of
I[01];
( F . (s,0) = f0 . s & F . (s,1) = D . s & F . (0,s) = the Point of Y & F . (1,s) = the Point of Y )
thus F . (
s,
0) =
F . [s,a0]
.=
R . (f . (s,0))
by FUNCT_2:15
.=
R . (g0 . s)
by A8
.=
f0 . s
by A5
;
( F . (s,1) = D . s & F . (0,s) = the Point of Y & F . (1,s) = the Point of Y )
thus F . (
s,1) =
F . [s,a1]
.=
R . (f . (s,1))
by FUNCT_2:15
.=
R . ( the constant Loop of x0 . s)
by A8
.=
D . s
by A5
;
( F . (0,s) = the Point of Y & F . (1,s) = the Point of Y )
thus F . (
0,
s) =
F . [a0,s]
.=
R . (f . (0,s))
by FUNCT_2:15
.=
R . x0
by A8
.=
the
Point of
Y
by A5
;
F . (1,s) = the Point of Y
thus F . (1,
s) =
F . [a1,s]
.=
R . (f . (1,s))
by FUNCT_2:15
.=
R . x0
by A8
.=
the
Point of
Y
by A5
;
verum
end; then
x = Class (
(EqRel (Y, the Point of Y)),
D)
by A6, TOPALG_1:46;
hence
x in {(Class ((EqRel (Y, the Point of Y)),D))}
by TARSKI:def 1;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in {(Class ((EqRel (Y, the Point of Y)),D))} or x in the carrier of (pi_1 (Y, the Point of Y)) )
assume
x in {(Class ((EqRel (Y, the Point of Y)),D))}
;
x in the carrier of (pi_1 (Y, the Point of Y))
then A9:
x = Class (
(EqRel (Y, the Point of Y)),
D)
by TARSKI:def 1;
D in Loops the
Point of
Y
by TOPALG_1:def 1;
then
x in Class (EqRel (Y, the Point of Y))
by A9, EQREL_1:def 3;
hence
x in the
carrier of
(pi_1 (Y, the Point of Y))
by TOPALG_1:def 5;
verum
end;
hence
contradiction
by A1; verum