let n be Element of NAT ; for A being convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
set TRn = TOP-REAL n;
let A be convex Subset of (TOP-REAL n); ( A is compact & not A is boundary implies ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) )
assume A1:
( A is compact & not A is boundary )
; ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
Int A <> {}
by A1, TOPS_1:48;
then consider p being object such that
A2:
p in Int A
by XBOOLE_0:def 1;
set TRnA = (TOP-REAL n) | A;
reconsider p = p as Point of (TOP-REAL n) by A2;
A3:
Int A c= A
by TOPS_1:16;
A4:
not A is empty
by A2;
per cases
( n = 0 or n > 0 )
;
suppose A5:
n = 0
;
ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )set T =
Tdisk (
(0. (TOP-REAL n)),1);
A6:
{(0. (TOP-REAL n))} = the
carrier of
(TOP-REAL n)
by A5, EUCLID:22, EUCLID:77;
then A7:
A = {(0. (TOP-REAL n))}
by A4, ZFMISC_1:33;
then reconsider I =
id ((TOP-REAL n) | A) as
Function of
((TOP-REAL n) | A),
(Tdisk ((0. (TOP-REAL n)),1)) by A6, ZFMISC_1:33;
take
I
;
( I is being_homeomorphism & I .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )A8:
Fr A = A \ (Int A)
by A5, TOPS_1:43;
A9:
Sphere (
(0. (TOP-REAL n)),1)
= {}
Int A = A
by A2, A3, A7, ZFMISC_1:33;
then A10:
Fr A = {}
by A8, XBOOLE_1:37;
Tdisk (
(0. (TOP-REAL n)),1)
= (TOP-REAL n) | A
by A6, A7, ZFMISC_1:33;
hence
(
I is
being_homeomorphism &
I .: (Fr A) = Sphere (
(0. (TOP-REAL n)),1) )
by A10, A9;
verum end; suppose A11:
n > 0
;
ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )set T =
transl (
(- p),
(TOP-REAL n));
set TA =
(transl ((- p),(TOP-REAL n))) .: A;
A12:
(transl ((- p),(TOP-REAL n))) .: A = (- p) + A
by RLTOPSP1:33;
then A13:
(
0. (TOP-REAL n) = 0* n &
(transl ((- p),(TOP-REAL n))) .: A is
convex )
by CONVEX1:7, EUCLID:70;
reconsider TT =
(transl ((- p),(TOP-REAL n))) | A as
Function of
((TOP-REAL n) | A),
((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A)) by JORDAN24:12;
A14:
TT .: (Int A) = (transl ((- p),(TOP-REAL n))) .: (Int A)
by RELAT_1:129, TOPS_1:16;
0. (TOP-REAL n) = (- p) + p
by RLVECT_1:5;
then A15:
0. (TOP-REAL n) in { ((- p) + q) where q is Element of (TOP-REAL n) : q in Int A }
by A2;
Int ((transl ((- p),(TOP-REAL n))) .: A) = (- p) + (Int A)
by A12, RLTOPSP1:37;
then
0. (TOP-REAL n) in Int ((transl ((- p),(TOP-REAL n))) .: A)
by A15, RUSUB_4:def 8;
then consider h being
Function of
((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A)),
(Tdisk ((0. (TOP-REAL n)),1)) such that A16:
h is
being_homeomorphism
and A17:
h .: (Fr ((transl ((- p),(TOP-REAL n))) .: A)) = Sphere (
(0. (TOP-REAL n)),1)
by A1, A11, A12, A13, Lm4;
reconsider hTT =
h * TT as
Function of
((TOP-REAL n) | A),
(Tdisk ((0. (TOP-REAL n)),1)) by A4;
take
hTT
;
( hTT is being_homeomorphism & hTT .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )A18:
Int ((transl ((- p),(TOP-REAL n))) .: A) =
(- p) + (Int A)
by A12, RLTOPSP1:37
.=
(transl ((- p),(TOP-REAL n))) .: (Int A)
by RLTOPSP1:33
;
A19:
TT is
being_homeomorphism
by JORDAN24:14;
then
dom TT = [#] ((TOP-REAL n) | A)
by TOPS_2:def 5;
then A20:
dom TT = A
by PRE_TOPC:def 5;
thus
hTT is
being_homeomorphism
by A4, A16, A19, TOPS_2:57;
hTT .: (Fr A) = Sphere ((0. (TOP-REAL n)),1)
rng TT = [#] ((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A))
by A19, TOPS_2:def 5;
then A21:
rng TT = (transl ((- p),(TOP-REAL n))) .: A
by PRE_TOPC:def 5;
Fr A = A \ (Int A)
by A1, TOPS_1:43;
then A22:
TT .: (Fr A) = (TT .: A) \ (TT .: (Int A))
by A19, FUNCT_1:64;
Fr ((transl ((- p),(TOP-REAL n))) .: A) =
((transl ((- p),(TOP-REAL n))) .: A) \ (Int ((transl ((- p),(TOP-REAL n))) .: A))
by A1, A12, TOPS_1:43
.=
TT .: (Fr A)
by A18, A22, A20, A21, A14, RELAT_1:113
;
hence
hTT .: (Fr A) = Sphere (
(0. (TOP-REAL n)),1)
by A17, RELAT_1:126;
verum end;