let n be Nat; for A being non empty convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A
set T = TOP-REAL n;
set cB = cl_Ball ((0. (TOP-REAL n)),1);
set S = Sphere ((0. (TOP-REAL n)),1);
A1:
[#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) = cl_Ball ((0. (TOP-REAL n)),1)
by PRE_TOPC:def 5;
then reconsider s = Sphere ((0. (TOP-REAL n)),1) as Subset of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by TOPREAL9:17;
A2:
(TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) = ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) | s
by PRE_TOPC:7, TOPREAL9:17;
let A be non empty convex Subset of (TOP-REAL n); ( A is compact & not A is boundary implies for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A )
assume A3:
( A is compact & not A is boundary )
; for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A
A4:
( [#] ((TOP-REAL n) | A) = A & Fr A c= A )
by A3, PRE_TOPC:def 5, TOPS_1:35;
let FR be non empty SubSpace of (TOP-REAL n) | A; ( [#] FR = Fr A implies not FR is_a_retract_of (TOP-REAL n) | A )
assume A5:
[#] FR = Fr A
; not FR is_a_retract_of (TOP-REAL n) | A
n > 0
then reconsider Ts = ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) | s as non empty SubSpace of (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) ;
assume
FR is_a_retract_of (TOP-REAL n) | A
; contradiction
then consider F being continuous Function of ((TOP-REAL n) | A),FR such that
A7:
F is being_a_retraction
;
reconsider f = F as Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) by A5, A4, FUNCT_2:7;
A8:
f is continuous
by PRE_TOPC:26;
A9:
rng F c= Fr A
by A5;
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set TN = TOP-REAL N;
A10:
[#] ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) = Sphere ((0. (TOP-REAL n)),1)
by PRE_TOPC:def 5;
( (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) = Tdisk ((0. (TOP-REAL N)),1) & (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) = Tcircle ((0. (TOP-REAL N)),1) )
by TOPREALB:def 6;
then A11:
not Ts is_a_retract_of (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))
by A2, Lm6;
not cl_Ball ((0. (TOP-REAL n)),1) is boundary
by Lm5;
then consider h being Function of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))),((TOP-REAL n) | A) such that
A12:
h is being_homeomorphism
and
A13:
h .: (Fr (cl_Ball ((0. (TOP-REAL n)),1))) = Fr A
by A3, Th7;
A14:
dom h = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)))
by A12, TOPS_2:def 5;
rng ((h ") * f) = ((h ") * f) .: (dom ((h ") * f))
by RELAT_1:113;
then A15:
rng ((h ") * f) c= ((h ") * f) .: (dom f)
by RELAT_1:25, RELAT_1:123;
reconsider H = h as Function ;
A16:
Fr (cl_Ball ((0. (TOP-REAL n)),1)) = Sphere ((0. (TOP-REAL n)),1)
by Th5;
rng h = [#] ((TOP-REAL n) | A)
by A12, TOPS_2:def 5;
then A17: (h ") .: (Fr A) =
h " (Fr A)
by A12, A4, TOPS_2:55
.=
Fr (cl_Ball ((0. (TOP-REAL n)),1))
by A12, A13, A1, A14, FUNCT_1:94, TOPS_1:35
;
((h ") * f) .: (dom f) =
(h ") .: (f .: (dom f))
by RELAT_1:126
.=
(h ") .: (rng f)
by RELAT_1:113
;
then
((h ") * f) .: (dom f) c= Fr (cl_Ball ((0. (TOP-REAL n)),1))
by A17, A9, RELAT_1:123;
then
( rng (((h ") * f) * h) c= rng ((h ") * f) & rng ((h ") * f) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) )
by A15, RELAT_1:26;
then
rng (((h ") * f) * h) c= Fr (cl_Ball ((0. (TOP-REAL n)),1))
;
then reconsider hfh = ((h ") * f) * h as Function of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))),Ts by A2, A16, A10, FUNCT_2:6;
h " is continuous
by A12, TOPS_2:def 5;
then
hfh is continuous
by A12, A8, PRE_TOPC:27;
then
not hfh is being_a_retraction
by A11;
then consider x being Point of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) such that
A18:
x in Sphere ((0. (TOP-REAL n)),1)
and
A19:
hfh . x <> x
by A2, A10;
set hx = h . x;
A20:
dom hfh = the carrier of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)))
by FUNCT_2:def 1;
then A21:
hfh . x = ((h ") * f) . (h . x)
by FUNCT_1:12;
x in dom h
by A20, FUNCT_1:11;
then A22:
h . x in the carrier of FR
by A5, A13, A16, A18, FUNCT_1:def 6;
h . x in dom ((h ") * f)
by A20, FUNCT_1:11;
then A23:
((h ") * f) . (h . x) = (h ") . (f . (h . x))
by FUNCT_1:12;
A24:
H " = h "
by A12, TOPS_2:def 4;
(H ") . (h . x) = x
by A12, A14, FUNCT_1:34;
hence
contradiction
by A7, A24, A19, A21, A23, A22; verum