let n be Element of NAT ; :: thesis: ( n > 0 implies for A being convex Subset of (TOP-REAL n) st A is compact & 0* n in Int A 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;
set En = Euclid n;
set cTRn = the carrier of (TOP-REAL n);
assume A1: n > 0 ; :: thesis: for A being convex Subset of (TOP-REAL n) st A is compact & 0* n in Int A 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) )
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 CL = cl_Ball ((0. (TOP-REAL n)),1);
set S = Sphere ((0. (TOP-REAL n)),1);
set TRn0 = (TOP-REAL n) | cTR0;
set nN = n NormF ;
set En = Euclid n;
set I0 = (0. (TOP-REAL n)) .--> (0. (TOP-REAL n));
let A be convex Subset of (TOP-REAL n); :: thesis: ( A is compact & 0* n in Int A 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 that
A2: A is compact and
A3: 0* n in Int A ; :: thesis: 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) )
A4: not A is empty by A3;
reconsider 0TRn = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
A5: 0* n = 0. (TOP-REAL n) by EUCLID:70;
then consider e being Real such that
A6: e > 0 and
A7: Ball (0TRn,e) c= A by A3, GOBOARD6:5;
Fr A misses Int A by TOPS_1:39;
then A8: not 0* n in Fr A by A3, XBOOLE_0:3;
then A9: (Fr A) \ {(0. (TOP-REAL n))} = Fr A by A5, ZFMISC_1:57;
set TM = TopSpaceMetr (Euclid n);
A10: [#] ((TOP-REAL n) | cTR0) = cTR0 by PRE_TOPC:def 5;
A11: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider a = A as Subset of (TopSpaceMetr (Euclid n)) ;
reconsider aa = a as Subset of (Euclid n) by EUCLID:67;
(TOP-REAL n) | A is compact by A2;
then (TopSpaceMetr (Euclid n)) | a is compact by A11, PRE_TOPC:36;
then A12: a is compact by A4, COMPTS_1:3;
A13: for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x} not Fr A is empty then reconsider FrA = Fr A as non empty Subset of ((TOP-REAL n) | cTR0) by A10, A9, XBOOLE_1:33;
A17: Fr A c= A by A2, TOPS_1:35;
set TS = (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1));
reconsider I = incl ((TOP-REAL n) | cTR0) as continuous Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TMAP_1:87;
A18: [#] ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) = Sphere ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;
A19: (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;
A22: dom b = cTR0 by A10, FUNCT_2:def 1;
A23: for p being Point of (TOP-REAL n) st p in cTR0 holds
( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 ) A27: rng b c= Sphere ((0. (TOP-REAL n)),1) then reconsider B = b as Function of ((TOP-REAL n) | cTR0),((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) by A10, A18, A22, FUNCT_2:2;
A31: (0. (TOP-REAL n)) .--> (0. (TOP-REAL n)) = {(0. (TOP-REAL n))} --> (0. (TOP-REAL n)) by FUNCOP_1:def 9;
then A32: dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) = {(0. (TOP-REAL n))} ;
set FRA = ((TOP-REAL n) | cTR0) | FrA;
set H = b | (((TOP-REAL n) | cTR0) | FrA);
A33: dom (b | (((TOP-REAL n) | cTR0) | FrA)) = the carrier of (((TOP-REAL n) | cTR0) | FrA) by FUNCT_2:def 1;
A34: b | (((TOP-REAL n) | cTR0) | FrA) = b | the carrier of (((TOP-REAL n) | cTR0) | FrA) by TMAP_1:def 4;
then A35: rng (b | (((TOP-REAL n) | cTR0) | FrA)) c= rng b by RELAT_1:70;
then A36: rng (b | (((TOP-REAL n) | cTR0) | FrA)) c= Sphere ((0. (TOP-REAL n)),1) by A27;
reconsider H = b | (((TOP-REAL n) | cTR0) | FrA) as Function of (((TOP-REAL n) | cTR0) | FrA),((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) by A18, A27, A33, A35, FUNCT_2:2, XBOOLE_1:1;
A37: [#] (((TOP-REAL n) | cTR0) | FrA) = FrA by PRE_TOPC:def 5;
A38: (Fr A) \ {(0. (TOP-REAL n))} c= cTR0 by XBOOLE_1:33;
Sphere ((0. (TOP-REAL n)),1) c= rng H then A47: Sphere ((0. (TOP-REAL n)),1) = rng H by A36, XBOOLE_0:def 10;
(Fr A) \ {(0. (TOP-REAL n))} c= cTR0 by XBOOLE_1:33;
then A48: ( dom H = [#] (((TOP-REAL n) | cTR0) | FrA) & (TOP-REAL n) | (Fr A) = ((TOP-REAL n) | cTR0) | FrA ) by A9, FUNCT_2:def 1, PRE_TOPC:7;
for x1, x2 being object st x1 in dom H & x2 in dom H & H . x1 = H . x2 holds
x1 = x2 then A62: H is one-to-one by FUNCT_1:def 4;
then H is being_homeomorphism by A2, A18, A47, A48, COMPTS_1:17, PRE_TOPC:27;
then reconsider H1 = H " as continuous Function of ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))),(((TOP-REAL n) | cTR0) | FrA) by TOPS_2:def 5;
reconsider HH = H as Function ;
set nN0F = nN0 | (((TOP-REAL n) | cTR0) | FrA);
reconsider H1B = H1 * B as Function of ((TOP-REAL n) | cTR0),(((TOP-REAL n) | cTR0) | FrA) by A47;
reconsider NH1B = (nN0 | (((TOP-REAL n) | cTR0) | FrA)) * H1B as Function of ((TOP-REAL n) | cTR0),R^1 ;
A63: nN0 | (((TOP-REAL n) | cTR0) | FrA) = nN0 | the carrier of (((TOP-REAL n) | cTR0) | FrA) by TMAP_1:def 4;
then ( rng NH1B c= rng (nN0 | (((TOP-REAL n) | cTR0) | FrA)) & rng (nN0 | (((TOP-REAL n) | cTR0) | FrA)) c= rng nN0 ) by RELAT_1:26, RELAT_1:70;
then rng NH1B c= rng nN0 ;
then A64: not 0 in rng NH1B ;
( B is continuous & not Sphere ((0. (TOP-REAL n)),1) is empty ) by A27, PRE_TOPC:27;
then reconsider NH1B = NH1B as non-empty continuous Function of ((TOP-REAL n) | cTR0),R^1 by A64, RELAT_1:def 9;
reconsider G = I </> NH1B as Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TOPREALC:46;
A65: dom G = cTR0 by A10, FUNCT_2:def 1;
A66: dom (nN0 | (((TOP-REAL n) | cTR0) | FrA)) = FrA by A37, FUNCT_2:def 1;
A67: for p being Point of (TOP-REAL n) st p in cTR0 holds
ex Hp being Point of (TOP-REAL n) st
( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) A74: not 0. (TOP-REAL n) in rng G A78: for x1, x2 being set st x1 in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) & x2 in (dom G) \ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) holds
((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2 H is onto by A18, A47, FUNCT_2:def 3;
then A82: H " = HH " by A62, TOPS_2:def 4;
A83: for p being Point of (TOP-REAL n) st p in cTR0 holds
(Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)} for x1, x2 being object st x1 in dom G & x2 in dom G & G . x1 = G . x2 holds
x1 = x2 then A104: G is one-to-one by FUNCT_1:def 4;
set G0 = G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)));
A105: dom (G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) = (dom G) \/ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) by FUNCT_4:def 1
.= cTR0 \/ {(0. (TOP-REAL n))} by A31, A65
.= the carrier of (TOP-REAL n) by ZFMISC_1:116 ;
A106: for p, Hp being Point of (TOP-REAL n) st p in cTR0 & Hp = H1B . p holds
( p = G . (|.Hp.| * p) & |.Hp.| * p in dom G ) A116: Sphere ((0. (TOP-REAL n)),1) c= G .: FrA A125: 0. (TOP-REAL n) in {(0. (TOP-REAL n))} by TARSKI:def 1;
then A126: ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . (0. (TOP-REAL n)) = 0. (TOP-REAL n) by A31, FUNCOP_1:7;
rng ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) = {(0. (TOP-REAL n))} by A31, FUNCOP_1:8;
then rng (G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) = (rng G) \/ {(0. (TOP-REAL n))} by A32, A65, NECKLACE:6, XBOOLE_1:79;
then reconsider G1 = G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) as one-to-one Function of (TOP-REAL n),(TOP-REAL n) by A105, A78, A104, FUNCT_2:2, TOPMETR2:1;
A127: G1 . (0. (TOP-REAL n)) = ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . (0. (TOP-REAL n)) by A32, A125, FUNCT_4:13;
A128: G .: FrA c= Sphere ((0. (TOP-REAL n)),1) set TRnCL = (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1));
set TRnA = (TOP-REAL n) | A;
A137: Int A c= A by TOPS_1:16;
set GA = G1 | ((TOP-REAL n) | A);
A138: G1 | ((TOP-REAL n) | A) = G1 | the carrier of ((TOP-REAL n) | A) by TMAP_1:def 4;
A139: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;
then A140: dom (G1 | ((TOP-REAL n) | A)) = A by FUNCT_2:def 1;
A141: dom (G1 | ((TOP-REAL n) | A)) = the carrier of ((TOP-REAL n) | A) by FUNCT_2:def 1;
A142: cl_Ball ((0. (TOP-REAL n)),1) c= rng (G1 | ((TOP-REAL n) | A)) rng (G1 | ((TOP-REAL n) | A)) c= cl_Ball ((0. (TOP-REAL n)),1) then A171: rng (G1 | ((TOP-REAL n) | A)) = cl_Ball ((0. (TOP-REAL n)),1) by A142, XBOOLE_0:def 10;
A172: [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;
then reconsider GA = G1 | ((TOP-REAL n) | A) as Function of ((TOP-REAL n) | A),((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A139, A140, A171, FUNCT_2:1;
set e2 = e / 2;
A173: GA is one-to-one by A138, FUNCT_1:52;
A174: e / 2 < e by A6, XREAL_1:216;
A175: G1 is continuous GA .: FrA = G1 .: FrA by A2, A138, A139, RELAT_1:129, TOPS_1:35;
then GA .: FrA = G .: FrA by A5, A8, A31, BOOLMARK:3, ZFMISC_1:50;
then A204: GA .: FrA = Sphere ((0. (TOP-REAL n)),1) by A116, A128, XBOOLE_0:def 10;
( dom GA = [#] ((TOP-REAL n) | A) & rng GA = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) ) by A142, A172, FUNCT_2:def 1, XBOOLE_0:def 10;
then GA is being_homeomorphism by A2, A3, A137, A173, A175, COMPTS_1:17, PRE_TOPC:27;
hence 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) ) by A204; :: thesis: verum