let n be Nat; for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st n > 0 & p in A & ( for r being Real st r > 0 holds
ex U being open Subset of ((TOP-REAL n) | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds
ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st
( h is continuous & h | (A \ U) = f ) ) ) ) holds
p in Fr A
let A be Subset of (TOP-REAL n); for p being Point of (TOP-REAL n) st n > 0 & p in A & ( for r being Real st r > 0 holds
ex U being open Subset of ((TOP-REAL n) | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds
ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st
( h is continuous & h | (A \ U) = f ) ) ) ) holds
p in Fr A
let p be Point of (TOP-REAL n); ( n > 0 & p in A & ( for r being Real st r > 0 holds
ex U being open Subset of ((TOP-REAL n) | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds
ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st
( h is continuous & h | (A \ U) = f ) ) ) ) implies p in Fr A )
set TRn = TOP-REAL n;
set cTRn = the carrier of (TOP-REAL n);
set CL = cl_Ball ((0. (TOP-REAL n)),1);
set S = Sphere ((0. (TOP-REAL n)),1);
set TS = Tunit_circle n;
assume A1:
n > 0
; ( not p in A or ex r being Real st
( r > 0 & ( for U being open Subset of ((TOP-REAL n) | A) holds
( not p in U or not U c= Ball (p,r) or ex f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st
( f is continuous & ( for h being Function of ((TOP-REAL n) | A),(Tunit_circle n) holds
( not h is continuous or not h | (A \ U) = f ) ) ) ) ) ) or p in Fr A )
the carrier of (TOP-REAL n) \ {(0. (TOP-REAL n))} = {(0. (TOP-REAL n))} `
by SUBSET_1:def 4;
then reconsider cTR0 = the carrier of (TOP-REAL n) \ {(0. (TOP-REAL n))} as non empty open Subset of (TOP-REAL n) by A1;
set nN = n NormF ;
set TRn0 = (TOP-REAL n) | cTR0;
A2:
Int A c= A
by TOPS_1:16;
set G = transl (p,(TOP-REAL n));
reconsider I = incl ((TOP-REAL n) | cTR0) as continuous Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TMAP_1:87;
A3:
[#] ((TOP-REAL n) | cTR0) = cTR0
by PRE_TOPC:def 5;
A4:
(n NormF) | ((TOP-REAL n) | cTR0) = (n NormF) | the carrier of ((TOP-REAL n) | cTR0)
by TMAP_1:def 4;
not 0 in rng ((n NormF) | ((TOP-REAL n) | cTR0))
then reconsider nN0 = (n NormF) | ((TOP-REAL n) | cTR0) as non-empty continuous Function of ((TOP-REAL n) | cTR0),R^1 by RELAT_1:def 9;
reconsider b = I </> nN0 as Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TOPREALC:46;
A7:
Int A in the topology of (TOP-REAL n)
by PRE_TOPC:def 2;
set En = Euclid n;
set TM = TopSpaceMetr (Euclid n);
assume that
A8:
p in A
and
A9:
for r being Real st r > 0 holds
ex U being open Subset of ((TOP-REAL n) | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds
ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st
( h is continuous & h | (A \ U) = f ) ) )
; p in Fr A
reconsider e = p as Point of (Euclid n) by EUCLID:67;
A10:
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider IA = Int A as Subset of (TopSpaceMetr (Euclid n)) ;
Tunit_circle n = Tcircle ((0. (TOP-REAL n)),1)
by TOPREALB:def 7;
then
Tunit_circle n = (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))
by TOPREALB:def 6;
then A11:
[#] (Tunit_circle n) = Sphere ((0. (TOP-REAL n)),1)
by PRE_TOPC:def 5;
assume
not p in Fr A
; contradiction
then
p in A \ (Fr A)
by A8, XBOOLE_0:def 5;
then
p in Int A
by TOPS_1:40;
then consider r being Real such that
A12:
r > 0
and
A13:
Ball (e,r) c= IA
by A7, A10, PRE_TOPC:def 2, TOPMETR:15;
set r2 = r / 2;
consider U being open Subset of ((TOP-REAL n) | A) such that
A14:
p in U
and
A15:
U c= Ball (p,(r / 2))
and
A16:
for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds
ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st
( h is continuous & h | (A \ U) = f )
by A12, A9;
reconsider Sph = Sphere (p,(r / 2)) as non empty Subset of (TOP-REAL n) by A1, A12;
consider au being object such that
A17:
au in Sph
by XBOOLE_0:def 1;
A18:
n in NAT
by ORDINAL1:def 12;
A19:
Ball (e,r) = Ball (p,r)
by TOPREAL9:13;
A20:
cl_Ball (p,(r / 2)) c= Ball (p,r)
by JORDAN:21, A18, A12, XREAL_1:216;
A21:
Sph = (cl_Ball (p,(r / 2))) \ (Ball (p,(r / 2)))
by JORDAN:19, A18;
then W:
au in cl_Ball (p,(r / 2))
by A17, XBOOLE_0:def 5;
A22:
au in IA
by W, A20, A19, A13;
reconsider r2 = r / 2 as non zero Real by A12;
reconsider CL2 = cl_Ball (p,r2) as non empty Subset of (TOP-REAL n) by A12;
A23:
Sph c= CL2
by A21, XBOOLE_1:36;
[#] ((TOP-REAL n) | CL2) = CL2
by PRE_TOPC:def 5;
then reconsider sph = Sph as non empty Subset of ((TOP-REAL n) | CL2) by A21, XBOOLE_1:36;
A24:
((TOP-REAL n) | CL2) | sph = (TOP-REAL n) | Sph
by PRE_TOPC:7, A21, XBOOLE_1:36;
not au in U
by A15, A21, A17, XBOOLE_0:def 5;
then reconsider AU = A \ U as non empty Subset of (TOP-REAL n) by A22, A2, XBOOLE_0:def 5;
set TAU = (TOP-REAL n) | AU;
set t = transl ((- p),(TOP-REAL n));
set T = (transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU);
A25:
[#] ((TOP-REAL n) | AU) = A \ U
by PRE_TOPC:def 5;
then A26:
dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) = A \ U
by FUNCT_2:def 1;
A27:
(transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU) = (transl ((- p),(TOP-REAL n))) | the carrier of ((TOP-REAL n) | AU)
by TMAP_1:def 4;
A28:
rng ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) c= cTR0
proof
let y be
object ;
TARSKI:def 3 ( not y in rng ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) or y in cTR0 )
assume
y in rng ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU))
;
y in cTR0
then consider x being
object such that A29:
x in dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU))
and A30:
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . x = y
by FUNCT_1:def 3;
reconsider x =
x as
Point of
(TOP-REAL n) by A29, A26;
A31:
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . x = (transl ((- p),(TOP-REAL n))) . x
by A29, A27, FUNCT_1:47;
A32:
(transl ((- p),(TOP-REAL n))) . x = x + (- p)
by RLTOPSP1:def 10;
assume
not
y in cTR0
;
contradiction
then
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . x in {(0. (TOP-REAL n))}
by A31, XBOOLE_0:def 5, A30;
then
x - p = 0. (TOP-REAL n)
by TARSKI:def 1, A32, A31;
then
x = p
by RLVECT_1:21;
hence
contradiction
by A29, A25, XBOOLE_0:def 5, A14;
verum
end;
then reconsider T0 = (transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU) as continuous Function of ((TOP-REAL n) | AU),((TOP-REAL n) | cTR0) by A26, FUNCT_2:2, A3, A25, PRE_TOPC:27;
A33:
[#] ((TOP-REAL n) | Sph) = Sph
by PRE_TOPC:def 5;
A34:
CL2 c= IA
by A20, A19, A13;
A35:
CL2 c= A
by A2, A20, A19, A13;
A36:
dom b = cTR0
by A3, FUNCT_2:def 1;
A37:
for p being Point of (TOP-REAL n) st p in cTR0 holds
( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 )
proof
let p be
Point of
(TOP-REAL n);
( p in cTR0 implies ( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 ) )
A38:
|.(1 / |.p.|).| = 1
/ |.p.|
by ABSVALUE:def 1;
assume A39:
p in cTR0
;
( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 )
then A40:
I . p = p
by A3, TMAP_1:84;
A41:
nN0 . p = (n NormF) . p
by A39, A3, A4, FUNCT_1:49;
thus b . p =
(I . p) (/) (nN0 . p)
by A36, A39, VALUED_2:72
.=
p (/) |.p.|
by A41, A40, JGRAPH_4:def 1
.=
(1 / |.p.|) * p
by VALUED_2:def 32
;
|.((1 / |.p.|) * p).| = 1
A42:
p <> 0. (TOP-REAL n)
by A39, ZFMISC_1:56;
thus |.((1 / |.p.|) * p).| =
|.(1 / |.p.|).| * |.p.|
by TOPRNS_1:7
.=
1
by A38, A42, TOPRNS_1:24, XCMPLX_1:87
;
verum
end;
rng b c= Sphere ((0. (TOP-REAL n)),1)
proof
let y be
object ;
TARSKI:def 3 ( not y in rng b or y in Sphere ((0. (TOP-REAL n)),1) )
assume
y in rng b
;
y in Sphere ((0. (TOP-REAL n)),1)
then consider x being
object such that A43:
x in dom b
and A44:
b . x = y
by FUNCT_1:def 3;
reconsider x =
x as
Point of
(TOP-REAL n) by A36, A43;
A45:
|.((1 / |.x.|) * x).| = 1
by A3, A37, A43;
A46:
((1 / |.x.|) * x) - (0. (TOP-REAL n)) = (1 / |.x.|) * x
by RLVECT_1:13;
y = (1 / |.x.|) * x
by A3, A37, A43, A44;
hence
y in Sphere (
(0. (TOP-REAL n)),1)
by A46, A45;
verum
end;
then reconsider B = b as Function of ((TOP-REAL n) | cTR0),(Tunit_circle n) by A3, A11, A36, FUNCT_2:2;
A47:
[#] (((TOP-REAL n) | CL2) | sph) = sph
by PRE_TOPC:def 5;
set m = mlt (r2,(TOP-REAL n));
set M = (mlt (r2,(TOP-REAL n))) | (Tunit_circle n);
reconsider M = (mlt (r2,(TOP-REAL n))) | (Tunit_circle n) as continuous Function of (Tunit_circle n),(TOP-REAL n) by A1;
A48:
M = (mlt (r2,(TOP-REAL n))) | the carrier of (Tunit_circle n)
by TMAP_1:def 4;
A49:
[#] ((TOP-REAL n) | A) = A
by PRE_TOPC:def 5;
then reconsider clB = CL2 as Subset of ((TOP-REAL n) | A) by A34, A2, XBOOLE_1:1;
A50:
((TOP-REAL n) | A) | clB = (TOP-REAL n) | CL2
by PRE_TOPC:7, A34, A2, XBOOLE_1:1;
B is continuous
by PRE_TOPC:27;
then
B * T0 is continuous
by TOPS_2:46;
then consider h being Function of ((TOP-REAL n) | A),(Tunit_circle n) such that
A51:
h is continuous
and
A52:
h | (A \ U) = B * T0
by A16;
M * h is continuous Function of ((TOP-REAL n) | A),(TOP-REAL n)
by A1, A51, TOPS_2:46;
then reconsider GHM = (transl (p,(TOP-REAL n))) * (M * h) as continuous Function of ((TOP-REAL n) | A),(TOP-REAL n) by TOPS_2:46;
A53:
dom h = the carrier of ((TOP-REAL n) | A)
by A1, FUNCT_2:def 1;
A54:
|.r2.| = r2
by A12, ABSVALUE:def 1;
A55:
rng GHM c= Sph
proof
let y be
object ;
TARSKI:def 3 ( not y in rng GHM or y in Sph )
assume
y in rng GHM
;
y in Sph
then consider q being
object such that A56:
q in dom GHM
and A57:
GHM . q = y
by FUNCT_1:def 3;
A58:
y = (transl (p,(TOP-REAL n))) . ((M * h) . q)
by A56, A57, FUNCT_1:12;
A59:
q in A
by A56, A49;
A60:
q in dom (M * h)
by A56, FUNCT_1:11;
then A61:
q in dom h
by FUNCT_1:11;
A62:
(M * h) . q = M . (h . q)
by A60, FUNCT_1:12;
A63:
h . q in dom M
by A60, FUNCT_1:11;
reconsider q =
q as
Point of
(TOP-REAL n) by A59;
h . q in Sphere (
(0. (TOP-REAL n)),1)
by A63, A11;
then reconsider hq =
h . q as
Point of
(TOP-REAL n) ;
A64:
(mlt (r2,(TOP-REAL n))) . (h . q) = r2 * hq
by RLTOPSP1:def 13;
M . (h . q) = (mlt (r2,(TOP-REAL n))) . (h . q)
by A63, A48, FUNCT_1:47;
then A65:
y = p + (r2 * hq)
by A58, A62, A64, RLTOPSP1:def 10;
A66:
(p + (r2 * hq)) - p =
(r2 * hq) + (p - p)
by RLVECT_1:28
.=
(r2 * hq) + (0. (TOP-REAL n))
by RLVECT_1:15
.=
r2 * hq
by RLVECT_1:def 4
;
A67:
h . q in rng h
by FUNCT_1:def 3, A61;
|.(r2 * hq).| =
|.r2.| * |.hq.|
by EUCLID:11
.=
|.r2.| * 1
by A67, A11, TOPREAL9:12
;
hence
y in Sph
by A66, A65, A54;
verum
end;
dom GHM = A
by A49, FUNCT_2:def 1;
then reconsider ghm = GHM as Function of ((TOP-REAL n) | A),((TOP-REAL n) | Sph) by A55, A49, A33, FUNCT_2:2;
ghm is continuous
by PRE_TOPC:27;
then reconsider ghM = ghm | (((TOP-REAL n) | A) | clB) as continuous Function of ((TOP-REAL n) | CL2),(((TOP-REAL n) | CL2) | sph) by A8, A50, A24;
A68:
dom ghM = the carrier of ((TOP-REAL n) | CL2)
by FUNCT_2:def 1;
A69:
ghM = ghm | the carrier of (((TOP-REAL n) | A) | clB)
by TMAP_1:def 4, A8;
for w being Point of ((TOP-REAL n) | CL2) st w in Sph holds
ghM . w = w
proof
let w be
Point of
((TOP-REAL n) | CL2);
( w in Sph implies ghM . w = w )
assume A70:
w in Sph
;
ghM . w = w
then reconsider q =
w as
Point of
(TOP-REAL n) ;
A71:
w in CL2
by A70, A23;
w in A
by A35, A70, A23;
then A72:
q in dom GHM
by A49, FUNCT_2:def 1;
then A73:
q in dom (M * h)
by FUNCT_1:11;
then A74:
(M * h) . q = M . (h . q)
by FUNCT_1:12;
not
q in U
by A70, A21, XBOOLE_0:def 5, A15;
then A75:
q in A \ U
by A71, A35, XBOOLE_0:def 5;
then
q in (A \ U) /\ (dom h)
by A71, A35, A53, A49, XBOOLE_0:def 4;
then A76:
q in dom (B * T0)
by A52, RELAT_1:61;
then A77:
(B * T0) . q = B . (T0 . q)
by FUNCT_1:12;
A78:
h . q in dom M
by A73, FUNCT_1:11;
then A79:
M . (h . q) = (mlt (r2,(TOP-REAL n))) . (h . q)
by A48, FUNCT_1:47;
(transl ((- p),(TOP-REAL n))) . q = q + (- p)
by RLTOPSP1:def 10;
then A80:
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . q = q - p
by A26, A27, A75, FUNCT_1:47;
q in dom T0
by A76, FUNCT_1:11;
then A81:
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU)) . q in rng ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | AU))
by FUNCT_1:def 3;
h . q in Sphere (
(0. (TOP-REAL n)),1)
by A78, A11;
then reconsider hq =
h . q as
Point of
(TOP-REAL n) ;
ghM . q = ghm . q
by A68, A69, FUNCT_1:47;
then A82:
ghM . q = (transl (p,(TOP-REAL n))) . ((M * h) . q)
by A72, FUNCT_1:12;
hq = (B * T0) . q
by A76, A52, FUNCT_1:47;
then A83:
hq = (1 / |.(q - p).|) * (q - p)
by A80, A77, A37, A81, A28;
(mlt (r2,(TOP-REAL n))) . (h . q) =
r2 * hq
by RLTOPSP1:def 13
.=
r2 * ((1 / r2) * (q - p))
by A83, A70, TOPREAL9:9
.=
(r2 * (1 / r2)) * (q - p)
by RLVECT_1:def 7
.=
1
* (q - p)
by XCMPLX_1:106
.=
q - p
by RLVECT_1:def 8
;
then ghM . w =
p + (q - p)
by A82, A74, A79, RLTOPSP1:def 10
.=
q + ((- p) + p)
by RLVECT_1:def 3
.=
q + (0. (TOP-REAL n))
by RLVECT_1:def 10
.=
q
by RLVECT_1:4
;
hence
ghM . w = w
;
verum
end;
then A84:
ghM is being_a_retraction
by BORSUK_1:def 16, A33, A24;
Ball (p,r2) c= Int CL2
by TOPREAL9:16, TOPS_1:24;
then A85:
not CL2 is boundary
by A12;
Fr CL2 = Sph
by A12, BROUWER2:5;
hence
contradiction
by A84, A85, A47, BROUWER2:9, BORSUK_1:def 17; verum