let n be non empty Element of NAT ; :: thesis: for r being real positive number
for x being Point of (TOP-REAL n)
for f being Function of (Tunit_circle n),(Tcircle x,r) st ( for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + x ) holds
f is being_homeomorphism
let r be real positive number ; :: thesis: for x being Point of (TOP-REAL n)
for f being Function of (Tunit_circle n),(Tcircle x,r) st ( for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + x ) holds
f is being_homeomorphism
let x be Point of (TOP-REAL n); :: thesis: for f being Function of (Tunit_circle n),(Tcircle x,r) st ( for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + x ) holds
f is being_homeomorphism
let f be Function of (Tunit_circle n),(Tcircle x,r); :: thesis: ( ( for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + x ) implies f is being_homeomorphism )
assume A1: for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + x ; :: thesis: f is being_homeomorphism
set U = Tunit_circle n;
set C = Tcircle x,r;
defpred S1[ Point of (TOP-REAL n), set ] means $2 = (r * $1) + x;
A2: (1 / r) * r = 1 by XCMPLX_1:88;
A3: the carrier of (Tunit_circle n) = Sphere (0. (TOP-REAL n)),1 by Th9;
A4: the carrier of (Tcircle x,r) = Sphere x,r by Th9;
A5: dom f = the carrier of (Tunit_circle n) by FUNCT_2:def 1;
thus dom f = [#] (Tunit_circle n) by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng f = [#] (Tcircle x,r) & f is one-to-one & f is continuous & f /" is continuous )
thus A6: rng f = [#] (Tcircle x,r) :: thesis: ( f is one-to-one & f is continuous & f /" is continuous )
proof
thus rng f c= [#] (Tcircle x,r) ; :: according to XBOOLE_0:def 10 :: thesis: [#] (Tcircle x,r) c= rng f
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in [#] (Tcircle x,r) or b in rng f )
assume A7: b in [#] (Tcircle x,r) ; :: thesis: b in rng f
then reconsider c = b as Point of (TOP-REAL n) by PRE_TOPC:55;
set a = (1 / r) * (c - x);
|.(((1 / r) * (c - x)) - (0. (TOP-REAL n))).| = |.((1 / r) * (c - x)).| by RLVECT_1:26, RLVECT_1:27
.= (abs (1 / r)) * |.(c - x).| by TOPRNS_1:8
.= (1 / r) * |.(c - x).| by ABSVALUE:def 1
.= (1 / r) * r by A4, A7, TOPREAL9:9 ;
then A8: (1 / r) * (c - x) in Sphere (0. (TOP-REAL n)),1 by A2;
then f . ((1 / r) * (c - x)) = (r * ((1 / r) * (c - x))) + x by A1, A3
.= ((r * (1 / r)) * (c - x)) + x by EUCLID:34
.= (c - x) + x by A2, EUCLID:33
.= b by EUCLID:52 ;
hence b in rng f by A3, A5, A8, FUNCT_1:def 5; :: thesis: verum
end;
thus A9: f is one-to-one :: thesis: ( f is continuous & f /" is continuous )
proof
let a, b be set ; :: according to FUNCT_1:def 8 :: thesis: ( not a in K1(f) or not b in K1(f) or not f . a = f . b or a = b )
assume that
A10: a in dom f and
A11: b in dom f and
A12: f . a = f . b ; :: thesis: a = b
reconsider a1 = a, b1 = b as Point of (TOP-REAL n) by A3, A5, A10, A11;
A13: f . a1 = (r * a1) + x by A1, A10;
f . b1 = (r * b1) + x by A1, A11;
then r * a1 = ((r * b1) + x) - x by A12, A13, EUCLID:52;
hence a = b by EUCLID:38, EUCLID:52; :: thesis: verum
end;
A14: for u being Point of (TOP-REAL n) ex y being Point of (TOP-REAL n) st S1[u,y] ;
consider F being Function of (TOP-REAL n),(TOP-REAL n) such that
A15: for x being Point of (TOP-REAL n) holds S1[x,F . x] from FUNCT_2:sch 3(A14);
 set f1 = id (TOP-REAL n);
set f2 = (TOP-REAL n) --> x;
for p being Point of (TOP-REAL n) holds F . p = (r * ((id (TOP-REAL n)) . p)) + (1 * (((TOP-REAL n) --> x) . p))
proof
let p be Point of (TOP-REAL n); :: thesis: F . p = (r * ((id (TOP-REAL n)) . p)) + (1 * (((TOP-REAL n) --> x) . p))
thus (r * ((id (TOP-REAL n)) . p)) + (1 * (((TOP-REAL n) --> x) . p)) = (r * ((id (TOP-REAL n)) . p)) + (((TOP-REAL n) --> x) . p) by EUCLID:33
.= (r * p) + (((TOP-REAL n) --> x) . p) by FUNCT_1:35
.= (r * p) + x by FUNCOP_1:13
.= F . p by A15 ; :: thesis: verum
end;
then A16: F is continuous by TOPALG_1:17;
dom F = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
then A17: dom (F | (Sphere (0. (TOP-REAL n)),1)) = Sphere (0. (TOP-REAL n)),1 by RELAT_1:91;
for a being set st a in dom f holds
f . a = (F | (Sphere (0. (TOP-REAL n)),1)) . a
proof
let a be set ; :: thesis: ( a in dom f implies f . a = (F | (Sphere (0. (TOP-REAL n)),1)) . a )
assume A18: a in dom f ; :: thesis: f . a = (F | (Sphere (0. (TOP-REAL n)),1)) . a
reconsider y = a as Point of (TOP-REAL n) by A18, PRE_TOPC:55;
thus f . a = (r * y) + x by A1, A18
.= F . y by A15
.= (F | (Sphere (0. (TOP-REAL n)),1)) . a by A3, A18, FUNCT_1:72 ; :: thesis: verum
end;
hence f is continuous by A16, A3, A5, A17, BORSUK_4:69, FUNCT_1:9; :: thesis: f /" is continuous
defpred S2[ Point of (TOP-REAL n), set ] means $2 = (1 / r) * ($1 - x);
A19: for u being Point of (TOP-REAL n) ex y being Point of (TOP-REAL n) st S2[u,y] ;
consider G being Function of (TOP-REAL n),(TOP-REAL n) such that
A20: for a being Point of (TOP-REAL n) holds S2[a,G . a] from FUNCT_2:sch 3(A19);
 A21: dom (f " ) = the carrier of (Tcircle x,r) by FUNCT_2:def 1;
dom G = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
then A22: dom (G | (Sphere x,r)) = Sphere x,r by RELAT_1:91;
for p being Point of (TOP-REAL n) holds G . p = ((1 / r) * ((id (TOP-REAL n)) . p)) + ((- (1 / r)) * (((TOP-REAL n) --> x) . p))
proof
let p be Point of (TOP-REAL n); :: thesis: G . p = ((1 / r) * ((id (TOP-REAL n)) . p)) + ((- (1 / r)) * (((TOP-REAL n) --> x) . p))
thus ((1 / r) * ((id (TOP-REAL n)) . p)) + ((- (1 / r)) * (((TOP-REAL n) --> x) . p)) = ((1 / r) * p) + ((- (1 / r)) * (((TOP-REAL n) --> x) . p)) by FUNCT_1:35
.= ((1 / r) * p) + ((- (1 / r)) * x) by FUNCOP_1:13
.= ((1 / r) * p) - ((1 / r) * x) by EUCLID:44
.= (1 / r) * (p - x) by EUCLID:53
.= G . p by A20 ; :: thesis: verum
end;
then A23: G is continuous by TOPALG_1:17;
for a being set st a in dom (f " ) holds
(f " ) . a = (G | (Sphere x,r)) . a
proof
let a be set ; :: thesis: ( a in dom (f " ) implies (f " ) . a = (G | (Sphere x,r)) . a )
assume A24: a in dom (f " ) ; :: thesis: (f " ) . a = (G | (Sphere x,r)) . a
reconsider y = a as Point of (TOP-REAL n) by A24, PRE_TOPC:55;
reconsider ff = f as Function ;
set e = (1 / r) * (y - x);
|.(((1 / r) * (y - x)) - (0. (TOP-REAL n))).| = |.((1 / r) * (y - x)).| by RLVECT_1:26, RLVECT_1:27
.= (abs (1 / r)) * |.(y - x).| by TOPRNS_1:8
.= (1 / r) * |.(y - x).| by ABSVALUE:def 1
.= (1 / r) * r by A4, A24, TOPREAL9:9 ;
then A25: (1 / r) * (y - x) in Sphere (0. (TOP-REAL n)),1 by A2;
then f . ((1 / r) * (y - x)) = (r * ((1 / r) * (y - x))) + x by A1, A3
.= ((r * (1 / r)) * (y - x)) + x by EUCLID:34
.= (y - x) + x by A2, EUCLID:33
.= y by EUCLID:52 ;
then (ff " ) . a = (1 / r) * (y - x) by A3, A5, A9, A25, FUNCT_1:54;
hence (f " ) . a = (1 / r) * (y - x) by A6, A9, TOPS_2:def 4
.= G . y by A20
.= (G | (Sphere x,r)) . a by A4, A24, FUNCT_1:72 ;
:: thesis: verum
end;
hence f /" is continuous by A23, A4, A21, A22, BORSUK_4:69, FUNCT_1:9; :: thesis: verum