:: Brouwer Invariance of Domain Theorem
:: by Karol P\kak
::
:: Received February 11, 2014
:: Copyright (c) 2014-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_1, ARYTM_3, BROUWER, CARD_1, COMPLEX1, CONVEX1, EUCLID,
FUNCOP_1, FUNCT_1, FUNCT_4, JGRAPH_4, MEMBERED, METRIC_1, NAT_1, NUMBERS,
ORDINAL2, PCOMPS_1, PRE_TOPC, RCOMP_1, REAL_1, RELAT_1, STRUCT_0,
SUBSET_1, SUPINF_2, TARSKI, TOPMETR, TOPS_1, TOPS_2, VALUED_1, XBOOLE_0,
XXREAL_0, FUNCT_2, EUCLID_9, TOPREALC, FINSEQ_1, FINSEQ_2, CARD_3,
PARTFUN3, SQUARE_1, XCMPLX_0, PARTFUN1, FINSET_1, VALUED_0, ORDINAL4,
PRE_POLY, PSCOMP_1, RVSUM_1, VALUED_2, T_0TOPSP, WAYBEL23, TOPDIM_1,
MATRTOP3, TOPREALB, RLTOPSP1, FUNCT_3, RLAFFIN1, RLVECT_5, MEASURE5,
BORSUK_1, UNIALG_1, MSSUBFAM, MATRLIN, MESFUNC1, VECTSP_1;
notations TARSKI, XBOOLE_0, FINSET_1, VALUED_0, SUBSET_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, COMPLEX1, ORDINAL1, NUMBERS, XXREAL_0,
XREAL_0, RVSUM_1, VALUED_1, VALUED_2, XXREAL_3, XCMPLX_0, NAT_1, CARD_1,
MEMBERED, FUNCOP_1, FINSEQ_1, FINSEQ_2, STRUCT_0, PRE_TOPC, TOPS_1,
PSCOMP_1, METRIC_1, PCOMPS_1, TOPMETR, FUNCT_7, RLVECT_1, RLTOPSP1,
EUCLID, TOPREAL9, PARTFUN3, TOPS_2, COMPTS_1, TBSP_1, JGRAPH_4, TMAP_1,
BROUWER, EUCLID_9, CARD_3, SQUARE_1, PRE_POLY, JORDAN2B, WAYBEL23,
T_0TOPSP, METRIZTS, RLAFFIN1, TOPREALB, FUNCT_4, DOMAIN_1, CONVEX1,
TIETZE_2, RLVECT_5, BORSUK_1, VECTSP_1, TOPREALC, MATRTOP3, MATRIX_1,
TOPDIM_1;
constructors TBSP_1, MONOID_0, CONVEX1, TOPS_1, COMPTS_1, FUNCSDOM, PARTFUN3,
JGRAPH_4, TMAP_1, TOPREALC, BROUWER, EUCLID_9, SQUARE_1, JORDAN2B,
PSCOMP_1, WAYBEL23, TOPDIM_1, METRIZTS, SIMPLEX0, RLAFFIN1, BORSUK_3,
RLVECT_5, MATRTOP3, TIETZE_2, LAPLACE;
registrations BORSUK_1, BROUWER, EUCLID, EUCLID_9, FUNCOP_1, FINSEQ_1,
FUNCT_1, FUNCT_2, JGRAPH_4, MEMBERED, NAT_1, PCOMPS_1, PRE_TOPC, RELAT_1,
PARTFUN3, RVSUM_1, SIMPLEX2, STRUCT_0, SUBSET_1, TMAP_1, TOPGRP_1,
TOPMETR, TOPS_1, VALUED_0, VALUED_2, XBOOLE_0, XREAL_0, XXREAL_0,
RELSET_1, FINSET_1, MONOID_0, SQUARE_1, FUNCT_7, NUMBERS, JORDAN2B,
FINSEQ_2, TOPREALC, PARTFUN4, COMPTS_1, TOPREALB, CARD_1, INT_1,
TOPREAL1, TOPREAL9, METRIZTS, RLTOPSP1, RLAFFIN1, RLAFFIN3, XXREAL_3,
TOPDIM_1, TOPDIM_2, REVROT_1, WAYBEL_2, XCMPLX_0, ZFMISC_1, VECTSP_1,
PRE_POLY, VALUED_1, MATRTOP3;
requirements ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
definitions TARSKI, XBOOLE_0;
equalities FUNCOP_1, STRUCT_0, SQUARE_1, XCMPLX_0, ALGSTR_0, TOPREAL9,
BROUWER, FINSEQ_1, ORDINAL1, EUCLID, FINSEQ_2;
expansions TARSKI, FUNCT_1, XBOOLE_0, FINSEQ_1;
theorems ABSVALUE, BORSUK_1, BROUWER, COMPLEX1, EUCLID, FUNCOP_1, FUNCT_1,
FUNCT_2, FUNCT_4, GOBOARD6, JGRAPH_4, JORDAN24, NECKLACE, ORDINAL1,
PRE_TOPC, RELAT_1, RLAFFIN1, RLAFFIN3, RLTOPSP1, RLVECT_1, SIMPLEX2,
SUBSET_1, TARSKI, TBSP_1, TMAP_1, TOPMETR, TOPREAL9, TOPREALB, TOPREALC,
TOPRNS_1, TOPS_1, TOPS_2, VALUED_2, XBOOLE_0, XBOOLE_1, XCMPLX_1,
XREAL_0, XREAL_1, XXREAL_0, ZFMISC_1, EUCLID_9, FINSEQ_2, CARD_1,
FINSEQ_1, PARTFUN3, YELLOW_8, FINSEQ_3, RVSUM_1, VALUED_1, PARTFUN1,
FUNCT_7, TOPREAL7, TSEP_1, BROUWER2, NAT_1, REAL_NS1, SQUARE_1, TOPGRP_1,
PRE_POLY, JORDAN2B, FINSEQ_4, JORDAN5A, VECTSP_1, JORDAN, ENUMSET1,
TOPDIM_1, TOPDIM_2, MATRTOP3, TOPGEN_5, METRIZTS, T_0TOPSP, TIETZE_2;
schemes FINSEQ_1, FUNCT_2, FUNCT_1, NAT_1;
begin :: Preliminaries
reserve x,X for set,
n, m, i for Nat,
p, q for Point of TOP-REAL n,
A, B for Subset of TOP-REAL n,
r, s for Real;
Lm1: for V being Subset of TopSpaceMetr Euclid n holds V is open implies for e
being Point of Euclid n st e in V ex r be Real st r>0 & OpenHypercube(e,r) c= V
proof
let V be Subset of TopSpaceMetr Euclid n;
assume
A1: V is open;
let e be Point of Euclid n;
assume e in V;
then consider r being Real such that
A2: r > 0
and
A3: Ball(e,r) c= V by A1,TOPMETR:15;
per cases;
suppose
A4: n<>0;
OpenHypercube(e,r/sqrt(n)) c= Ball(e,r) by A4,EUCLID_9:17;
hence thesis by A3,XBOOLE_1:1, A4,A2;
end;
suppose
A6: n=0;
set TR=TOP-REAL 0,Z=0.TR;
A9: Ball(e,r) = {} or Ball(e,r) = {Z} by EUCLID:77,ZFMISC_1:33,A6;
the carrier of TopSpaceMetr Euclid 0= the carrier of Euclid 0
by TOPMETR:12;
then OpenHypercube(e,1) = {Z} by EUCLID:77,ZFMISC_1:33,A6;
hence thesis by A9,A2,A3;
end;
end;
Lm2: r>0 implies cl_Ball(p,r) is non boundary compact
proof
assume
A1: r>0;
Ball(p,r) c= Int cl_Ball(p,r) by TOPREAL9:16,TOPS_1:24;
hence thesis by A1;
end;
registration
let X;
let n;
cluster -> FinSequence-yielding for Function of X,TOP-REAL n;
coherence
proof
let F be Function of X,TOP-REAL n;
now let x be object;
assume x in dom F;
then F.x in rng F by FUNCT_1:def 3;
hence F.x is FinSequence;
end;
hence thesis by PRE_POLY:def 3;
end;
end;
definition
let X,n,m;
let f be Function of X,TOP-REAL n;
let g be Function of X,TOP-REAL m;
redefine func f^^g -> Function of X,TOP-REAL (n+m); :: redefines ^^ (PRE_POLY, definition)
coherence
proof
set fg=f^^g;
A1:dom g = X by FUNCT_2:def 1;
A2:dom f = X by FUNCT_2:def 1;
then
A3: dom fg=X/\X by A1,PRE_POLY:def 4;
rng fg c= the carrier of TOP-REAL (n+m)
proof
let y be object;
assume y in rng fg;
then consider x be object such that
A4: x in dom fg
and
A5: fg.x=y by FUNCT_1:def 3;
g.x in rng g by A1,A4, A3,FUNCT_1:def 3;
then reconsider gx=g.x as Point of TOP-REAL m;
f.x in rng f by A2,A4, A3,FUNCT_1:def 3;
then reconsider fx=f.x as Point of TOP-REAL n;
rng (fx^gx) c= REAL;
then
A7: fx^gx is FinSequence of REAL by FINSEQ_1:def 4;
Z: len (fx^gx)=n+m by CARD_1:def 7;
fg.x = fx^gx by PRE_POLY:def 4,A4;
hence thesis by A5,Z,A7,TOPREAL7:17;
end;
hence thesis by A3,FUNCT_2:2;
end;
end;
registration
let T be TopSpace;
let n,m;
let f be continuous Function of T,TOP-REAL n;
let g be continuous Function of T,TOP-REAL m;
cluster f^^g -> continuous for Function of T,TOP-REAL (n+m);
coherence
proof
set fg=f^^g;
set Tn=TOP-REAL n,Tm=TOP-REAL m,Tnm=TOP-REAL (n+m);
A1: [#]TOP-REAL n =the carrier of TOP-REAL n;
A2: the TopStruct of TOP-REAL (n+m) = TopSpaceMetr Euclid (n+m)
by EUCLID:def 8;
A3: the TopStruct of TOP-REAL m = TopSpaceMetr Euclid m by EUCLID:def 8;
A4: [#]TOP-REAL m =the carrier of TOP-REAL m;
A5: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
A6:now
let P be Subset of TOP-REAL (n+m);
assume P is open;
then P in the topology of TopSpaceMetr Euclid (n+m) by A2,PRE_TOPC:def 2;
then reconsider p=P as open Subset of TopSpaceMetr Euclid (n+m)
by PRE_TOPC:def 2;
for x holds x in fg"P iff ex Q be Subset of T st Q is open &
Q c= fg"P & x in Q
proof
let y be set;
hereby
assume
A7: y in fg"P;
then
A8: y in dom fg by FUNCT_1:def 7;
fg.y in p by A7,FUNCT_1:def 7;
then reconsider e=fg.y as Point of Euclid (n+m) by EUCLID: 67;
A10: dom fg = dom f/\dom g by PRE_POLY:def 4;
then
A11: y in dom f by A8,XBOOLE_0:def 4;
then f.y in rng f by FUNCT_1:def 3;
then reconsider fy=f.y as Point of TOP-REAL n;
A12: y in dom g by A10,A8,XBOOLE_0:def 4;
then g.y in rng g by FUNCT_1:def 3;
then reconsider gy=g.y as Point of TOP-REAL m;
len e = n+m by CARD_1:def 7;
then consider e1,e2 be FinSequence of REAL such that
A13: len e1 = n
and
A14: len e2 = m
and
A15: e=e1^e2 by FINSEQ_2:23;
reconsider e2 as Point of Euclid m by TOPREAL7:16,A14;
reconsider e1 as Point of Euclid n by TOPREAL7:16,A13;
A16: fy^gy = e1^e2 by PRE_POLY:def 4,A8,A15;
fg.y in p by A7,FUNCT_1:def 7;
then consider r be Real such that
A17: r>0
and
A18: OpenHypercube(e,r) c= p by Lm1;
OpenHypercube(e2,r) in the topology of TOP-REAL m
by A3,PRE_TOPC:def 2;
then reconsider O2=OpenHypercube(e2,r) as open Subset of TOP-REAL m
by PRE_TOPC:def 2;
A19: g"O2 is open by A4,TOPS_2:43;
OpenHypercube(e1,r) in the topology of TOP-REAL n
by A5,PRE_TOPC:def 2;
then reconsider O1=OpenHypercube(e1,r) as open Subset of TOP-REAL n
by PRE_TOPC:def 2;
take Q=(f"O1)/\(g"O2);
A20: O2 = product Intervals(e2,r) by EUCLID_9:def 4;
f"O1 is open by A1,TOPS_2:43;
hence Q is open by A19;
A21: OpenHypercube(e,r) = product Intervals(e,r) by EUCLID_9:def 4;
len fy = n by CARD_1:def 7;
then dom fy = dom e1 by A13,FINSEQ_3:29;
then
A22: fy = (e1^e2) | (dom e1) by FINSEQ_1:21,A16
.= e1 by FINSEQ_1:21;
then gy = e2 by A16,FINSEQ_1:33;
then gy in O2 by EUCLID_9:11,A17;
then
A23: y in g"O2 by A12,FUNCT_1:def 7;
A24: O1 = product Intervals(e1,r) by EUCLID_9:def 4;
thus Q c= fg"P
proof
let x be object;
assume
A25: x in Q;
then
A26: x in f"O1 by XBOOLE_0:def 4;
then
A27: f.x in O1 by FUNCT_1:def 7;
then reconsider fx=f.x as Point of TOP-REAL n;
A28: x in g"O2 by A25,XBOOLE_0:def 4;
then
A29: x in dom g by FUNCT_1:def 7;
A30: g.x in O2 by A28,FUNCT_1:def 7;
then reconsider gx=g.x as Point of TOP-REAL m;
A31: fx^gx in product (Intervals(e1,r)^Intervals(e2,r))
by A24,A20,A27,A30,RLAFFIN3:2;
x in dom f by A26,FUNCT_1:def 7;
then
A32: x in dom fg by A29,A10,XBOOLE_0:def 4;
then fg.x = fx^gx by PRE_POLY:def 4;
then fg.x in OpenHypercube(e,r) by A31,A15,RLAFFIN3:1,A21;
hence thesis by A18,A32,FUNCT_1:def 7;
end;
fy in O1 by A22,EUCLID_9:11,A17;
then y in f"O1 by A11,FUNCT_1:def 7;
hence y in Q by A23,XBOOLE_0:def 4;
end;
thus thesis;
end;
hence fg"P is open by TOPS_1:25;
end;
[#]TOP-REAL (n+m) =the carrier of TOP-REAL (n+m);
hence thesis by A6,TOPS_2:43;
end;
end;
definition
let f be real-valued Function;
func |[ f ]| -> Function means :Def1:
dom it = dom f & for x be object st x in dom it holds it.x = |[ f.x ]|;
existence
proof
deffunc F(object) = |[ f.$1 ]|;
ex F being Function st dom F = dom f & for x be object st x in dom f
holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Function such that
A1: dom F1 = dom f
and
A2: for x be object st x in dom F1 holds F1.x = |[ f.x ]|
and
A3: dom F2 = dom f
and
A4: for x be object st x in dom F2 holds F2.x = |[ f.x ]|;
now
let x;
assume
A5: x in dom F1;
hence F1.x = |[ f.x ]| by A2
.= F2.x by A1,A3,A4,A5;
end;
hence thesis by A1,A3;
end;
end;
registration
let f be real-valued Function;
cluster |[ f ]| -> (the carrier of TOP-REAL 1)-valued;
coherence
proof
set F=|[ f ]|;
rng F c= the carrier of TOP-REAL 1
proof
let y be object;
assume y in rng F;
then consider x be object such that
A1: x in dom F
and
A2: F.x = y by FUNCT_1:def 3;
F.x=|[ f.x ]| by A1,Def1;
hence thesis by A2;
end;
hence thesis by RELAT_1:def 19;
end;
end;
definition
let X;
let Y be non empty real-membered set;
let f be Function of X,Y;
redefine func |[ f ]| -> Function of X,TOP-REAL 1; :: redefines |[ (BROUWER3, definition)
coherence
proof
dom f = X by FUNCT_2:def 1;
then
A1:dom |[ f ]| = X by Def1;
rng |[f]| c= the carrier of TOP-REAL 1;
hence thesis by A1,FUNCT_2:2;
end;
end;
registration
let T be non empty TopSpace;
let f be continuous Function of T,R^1;
cluster |[ f ]| -> continuous for Function of T,TOP-REAL 1;
coherence
proof
defpred P[Element of TOP-REAL 1,object] means $2=$1/.1;
A1: for x be Element of TOP-REAL 1 ex y be Element of R^1 st P[x,y]
by TOPMETR:17;
consider P being Function of TOP-REAL 1,R^1 such that
A2: for x being Element of TOP-REAL 1 holds P[x,P.x]
from FUNCT_2:sch 3(A1);
A3: P is being_homeomorphism by A2,JORDAN2B:28;
then reconsider PP=P" as continuous Function of R^1,TOP-REAL 1
by TOPS_2:def 5;
A4: dom PP = the carrier of R^1 by FUNCT_2:def 1;
A5: dom |[ f ]| = dom f by Def1;
reconsider PPf=PP*f as Function of T,TOP-REAL 1;
A6: dom f = the carrier of T by FUNCT_2:def 1;
A7: now
A8: PP = (P qua Function)" by A3,TOPS_2:def 4;
let x be object;
A9: rng P =[#]R^1 by A3,TOPS_2:def 5;
assume
A10: x in dom PPf;
then
A11: PPf.x=PP.(f.x) by FUNCT_1:12;
PPf.x in rng PPf by A10, FUNCT_1:def 3;
then reconsider PPfx=PPf.x as Point of TOP-REAL 1;
f.x in dom PP by A10,FUNCT_1:11;
then P.(PPf.x) = f.x by A11,A8, A3,A9,FUNCT_1:35;
then
A12: PPfx/.1 = f.x by A2;
consider R be Real such that
B: <*R*> = PPfx by JORDAN2B:20;
R is Element of REAL by XREAL_0:def 1;
then R=f.x by A12,B,FINSEQ_4:16;
hence PPf.x=|[ f ]|.x by B,A10,A6,A5,Def1;
end;
rng f c= the carrier of R^1 by RELAT_1:def 19;
hence thesis by A4,A7,RELAT_1:27,A5,FUNCT_1:2;
end;
end;
registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
cluster |[ f ]| -> continuous for Function of T,TOP-REAL 1;
coherence
proof
reconsider F=f as Function of T,R^1 by TOPMETR:17;
F is continuous by JORDAN5A:27;
hence thesis;
end;
end;
begin :: A Distribution of Sphere
reserve N for non zero Nat,
u,t for Point of TOP-REAL(N+1);
theorem Th1:
for F be Element of N-tuples_on
Funcs(the carrier of TOP-REAL(N+1),the carrier of R^1)
st for i st i in dom F holds F.i = PROJ(N+1,i)
holds
(for t holds <:F:>.t = t|N) &
for Sp,Sn be Subset of TOP-REAL(N+1) st
Sp = {u: u.(N+1)>=0 & |.u.|=1} &
Sn = {t: t.(N+1)<=0 & |.t.|=1}
holds
<:F:>.:Sp = cl_Ball(0.TOP-REAL N,1) &
<:F:>.:Sn = cl_Ball(0.TOP-REAL N,1) &
<:F:>.:(Sp/\Sn) = Sphere(0.TOP-REAL N,1) &
(for H be Function of (TOP-REAL(N+1)) |Sp,Tdisk(0.TOP-REAL N,1) st
H= <:F:>|Sp holds H is being_homeomorphism) &
for H be Function of (TOP-REAL(N+1)) |Sn,Tdisk(0.TOP-REAL N,1) st
H= <:F:>|Sn holds H is being_homeomorphism
proof
set N1=N+1,Tn1=TOP-REAL N1,Tn=TOP-REAL N;
N:N in NAT by ORDINAL1:def 12;
set N0=(0*N1)+*(N1,-1);
A1: len N0 = N1 by CARD_1:def 7;
rng N0 c= REAL;
then N0 is FinSequence of REAL by FINSEQ_1:def 4;
then reconsider N0 as Point of Tn1 by A1,TOPREAL7:17;
set NF=N NormF,NNF=NF(#)NF;
reconsider ONE=1 as Element of NAT;
set TD=Tdisk(0.TOP-REAL N,1);
A2: [#]TD = cl_Ball(0.Tn,1) by PRE_TOPC:def 5;
reconsider NNF as Function of Tn,R^1 by TOPMETR:17;
reconsider mNNF=-NNF as Function of Tn,R^1 by TOPMETR:17;
reconsider m1=1+mNNF as Function of Tn,R^1 by TOPMETR:17;
1<= N1 by NAT_1:11;
then
A3: N1 in Seg N1;
dom (0*N1)=Seg N1;
then
A4: N0.N1 = -1 by A3,FUNCT_7:31;
let F be Element of N-tuples_on Funcs(the carrier of Tn1,the carrier of R^1);
set FF=<:F:>;
A5:N < N1 by NAT_1:13;
len F = N by CARD_1:def 7;
then
A6: dom F=Seg N by FINSEQ_1:def 3;
assume
A7: for i st i in dom F holds F.i = PROJ(N1,i);
thus
A8: for t holds <:F:>.t = t|N
proof
let s be Point of Tn1;
reconsider Fs=FF.s as Point of Tn;
A9: len Fs=N by CARD_1:def 7;
A10:len s = N1 by CARD_1:def 7;
now let i;
assume that
A12: 1<= i
and
A13: i <= N;
A14: Fs.i = F.i.s by TIETZE_2:1;
i < N1 by A13, NAT_1:13;
then
A15: i in dom s by A10,A12,FINSEQ_3: 25;
F.i = PROJ(N1,i) by A12,A13,FINSEQ_1:1,A7,A6;
then
A16: Fs.i = s/.i by A14,TOPREALC:def 6;
(s|N).i=s.i by A12,A13,FINSEQ_1:1, FUNCT_1:49;
hence Fs.i = (s|N).i by A16, A15,PARTFUN1:def 6;
end;
hence thesis by A9,A10,FINSEQ_1:59,A5;
end;
let Sp,Sn be Subset of Tn1;
assume
A17: Sp = {u: u.N1>=0 & |.u.|=1};
A18: dom FF = the carrier of Tn1 by FUNCT_2:def 1;
A19:cl_Ball(0.Tn,1) c= FF.:Sp
proof
let x be object;
assume
A20: x in cl_Ball(0.Tn,1);
then reconsider s=x as Element of REAL N by EUCLID:22;
set sq = sqrt(1-|.s.|^2), s1=s^<*sq*>;
|.s.| <= 1 by TOPREAL9:11,A20;
then |.s.|* |.s.| <= 1 * 1 by XREAL_1:66;
then
A21: 1-|.s.|^2 >= |.s.|^2-|.s.|^2 by XREAL_1:13;
then
A22: sq^2 = 1-|.s.|^2 by SQUARE_1:def 2;
A23:len s1 = len s + 1 by FINSEQ_2:16;
A24:len s = N by CARD_1:def 7;
s1 is FinSequence of REAL by RVSUM_1:145;
then reconsider s1 as Element of REAL N1 by A23,A24,FINSEQ_2:92;
(s1|N)^<*s1.N1*> = s1 by FINSEQ_3:55,A23, CARD_1:def 7;
then
A25: s1|N=s by FINSEQ_2:17;
reconsider ss1=s1 as Point of Tn1 by EUCLID:22;
A26: s1.N1 = sq by A24,FINSEQ_1:42;
then |.s1.| ^2 = |.s.| ^2 + (sq)^2 by A25,REAL_NS1:10
.= 1 ^2 by A22;
then |.s1.| = 1 or |.s1.| = -1 by SQUARE_1:40;
then
A27: ss1 in Sp by A17,A26,A21;
FF.ss1 = s by A25, A8;
hence thesis by A27, A18,FUNCT_1:def 6;
end;
assume
A28: Sn= {t: t.N1<=0 & |.t.| =1};
A29:cl_Ball(0.Tn,1) c= FF.:Sn
proof
let x be object;
assume
A30: x in cl_Ball(0.Tn,1);
then reconsider s=x as Element of REAL N by EUCLID:22;
|.s.| <= 1 by TOPREAL9:11,A30;
then |.s.|* |.s.| <= 1 * 1 by XREAL_1:66;
then
A31: 1-|.s.|^2 >= |.s.|^2-|.s.|^2 by XREAL_1:13;
set sq = -sqrt(1-|.s.|^2), s1=s^<*sq*>;
A32:len s1 = len s + 1 by FINSEQ_2:16;
sq^2 = (-sq)^2;
then
A33: sq^2 = 1-|.s.|^2 by SQUARE_1:def 2,A31;
A34: len s = N by CARD_1:def 7;
s1 is FinSequence of REAL by RVSUM_1:145;
then reconsider s1 as Element of REAL N1 by A32,A34,FINSEQ_2:92;
(s1|N)^<*s1.N1*> = s1 by FINSEQ_3:55,A32, CARD_1:def 7;
then
A35: s1|N=s by FINSEQ_2:17;
reconsider ss1=s1 as Point of Tn1 by EUCLID:22;
A36:s1.N1 = sq by A34,FINSEQ_1:42;
then |.s1.| ^2 = |.s.| ^2 + (sq)^2 by A35,REAL_NS1:10
.= 1 ^2 by A33;
then |.s1.| = 1 or |.s1.| = -1 by SQUARE_1:40;
then
A37: ss1 in Sn by A28,A36,A31;
FF.ss1 = s by A35,A8;
hence thesis by A37, A18,FUNCT_1:def 6;
end;
A38:Sphere(0.Tn,1) c= FF.:(Sn/\Sp)
proof
reconsider Z=0 as Element of REAL by XREAL_0:def 1;
let x be object;
assume
A39: x in Sphere(0.Tn,1);
then reconsider s=x as Element of REAL N by EUCLID:22;
A40: |.s.| = 1 by TOPREAL9:12,A39;
set s1=s^<* Z *>;
A41:len s = N by CARD_1:def 7;
A42:len s1 = len s + 1 by FINSEQ_2:16;
then reconsider s1 as Element of REAL N1 by A41,FINSEQ_2:92;
A43:s1.N1 = 0 by A41,FINSEQ_1:42;
reconsider ss1=s1 as Point of Tn1 by EUCLID:22;
(s1|N)^<*s1.N1*> = s1 by FINSEQ_3:55,A42, CARD_1:def 7;
then
A44: s1|N=s by FINSEQ_2:17;
then |.s1.| ^2 = |.s.| ^2 + 0^2 by A43,REAL_NS1:10;
then
A45: |.s1.| = 1 or |.s1.| = -1 by A40,SQUARE_1:40;
then
A46: ss1 in Sn by A28,A43;
ss1 in Sp by A45,A17,A43;
then
A47: ss1 in Sp/\Sn by A46,XBOOLE_0:def 4;
FF.ss1 = s by A44,A8;
hence thesis by A47, A18,FUNCT_1:def 6;
end;
A48:FF.:Sp c= cl_Ball(0.Tn,1)
proof
let y be object;
assume y in FF.:Sp;
then consider x be object such that
x in dom FF
and
A49: x in Sp
and
A50: FF.x=y by FUNCT_1:def 6;
consider s be Point of Tn1 such that
A51: s=x
and
s.N1>=0
and
A52: |.s.|=1 by A49,A17;
reconsider ss=s as Element of REAL N1 by EUCLID:22;
len ss = N1 by CARD_1:def 7;
then len (ss|N)=N by A5,FINSEQ_1:59;
then reconsider sN=ss|N as Point of Tn by TOPREAL7:17;
|.ss.| ^2 = |.sN .| ^2 + (s.N1)^2 by REAL_NS1:10;
then |.ss.| ^2 >= |.sN .| ^2+0 by XREAL_1:6;
then
A53: 1 >= |. sN .| by SQUARE_1:16,A52;
sN -0.Tn = sN by RLVECT_1:13;
then sN in cl_Ball(0.Tn,1) by A53;
hence thesis by A8,A51,A50;
end;
hence FF.:Sp = cl_Ball(0.Tn,1) by A19;
A54:FF.:Sn c= cl_Ball(0.Tn,1)
proof
let y be object;
assume y in FF.:Sn;
then consider x be object such that
x in dom FF and
A55: x in Sn
and
A56: FF.x=y by FUNCT_1:def 6;
consider s be Point of Tn1 such that
A57: s=x
and
s.N1<=0
and
A58: |.s.|=1 by A55,A28;
reconsider ss=s as Element of REAL N1 by EUCLID:22;
len ss = N1 by CARD_1:def 7;
then len (ss|N)=N by A5,FINSEQ_1:59;
then reconsider sN=ss|N as Point of Tn by TOPREAL7:17;
|.ss.| ^2 = |.sN .| ^2 + (s.N1)^2 by REAL_NS1:10;
then |.ss.| ^2 >= |.sN .| ^2+0 by XREAL_1:6;
then
A59: 1 >= |. sN .| by SQUARE_1:16,A58;
sN -0.Tn = sN by RLVECT_1:13;
then sN in cl_Ball(0.Tn,1) by A59;
hence thesis by A8,A57,A56;
end;
hence FF.:Sn = cl_Ball(0.Tn,1) by A29;
FF.:(Sn/\Sp) c= Sphere(0.Tn,1)
proof
let y be object;
assume y in FF.:(Sn/\Sp);
then consider x be object such that
x in dom FF
and
A60: x in (Sn/\Sp)
and
A61: FF.x=y by FUNCT_1:def 6;
x in Sn by A60,XBOOLE_0:def 4;
then consider s be Point of Tn1 such that
A62: s=x
and
A63: s.N1 <= 0
and
A64: |.s.|=1 by A28;
reconsider ss=s as Element of REAL N1 by EUCLID:22;
len ss = N1 by CARD_1:def 7;
then len (ss|N)=N by A5,FINSEQ_1:59;
then reconsider sN=ss|N as Point of Tn by TOPREAL7:17;
A65: |.ss.| ^2 = |.sN .| ^2 + (s.N1)^2 by REAL_NS1:10;
x in Sp by A60,XBOOLE_0:def 4;
then ex s1 be Point of Tn1 st s1=x & s1.N1 >= 0 & |.s1.|=1 by A17;
then (s.N1)^2 =0 by A62,A63;
then
A66: |.ss.| = |.sN .| or |.ss.| = -|.sN .| by A65,SQUARE_1:40;
sN -0.Tn = sN by RLVECT_1:13;
then sN in Sphere(0.Tn,1) by A66, A64;
hence thesis by A8, A62,A61;
end;
hence FF.:(Sp/\Sn) = Sphere(0.Tn,1) by A38;
thus for H be Function of (TOP-REAL(N+1)) |Sp,Tdisk(0.TOP-REAL N,1) st
H=<:F:>|Sp holds H is being_homeomorphism
proof
set N0=(0*N1)+*(N1,1);
rng N0 c= REAL;
then
W: N0 is FinSequence of REAL by FINSEQ_1:def 4;
len N0 = N1 by CARD_1:def 7;
then reconsider N0 as Point of Tn1 by W,TOPREAL7:17;
reconsider ONE=1 as Element of NAT;
set NF=N NormF,NNF=NF(#)NF;
A67:[#]TD = cl_Ball(0.Tn,1) by PRE_TOPC:def 5;
reconsider NNF as Function of Tn,R^1 by TOPMETR:17;
reconsider mNNF=-NNF as Function of Tn,R^1 by TOPMETR:17;
reconsider m1=1+mNNF as Function of Tn,R^1 by TOPMETR:17;
1<= N1 by NAT_1:11;
then
A68: N1 in Seg N1;
then
A69: |.N0.| = |. 1 .| by TOPREALC:13
.= 1 by ABSVALUE:def 1;
let H be Function of Tn1 |Sp,TD such that
A70: H = FF|Sp;
A71:dom H = [#](Tn1 |Sp) by FUNCT_2:def 1;
A72:[#](Tn1 |Sp) = Sp by PRE_TOPC:def 5;
then
A73: rng H = (FF|Sp).:Sp by A71,A70,RELAT_1:113
.= cl_Ball(0.Tn,1) by A19,A48,RELAT_1:129;
then
A74: rng H = [#]TD by PRE_TOPC:def 5;
A75:for x1,x2 be object st x1 in dom H & x2 in dom H & H.x1 =H.x2 holds x1=x2
proof
let x1,x2 be object;
assume
A76: x1 in dom H;
then consider s1 be Point of Tn1 such that
A77: x1=s1
and
A78: s1.N1>=0
and
A79: |.s1.|=1 by A17,A71,A72;
assume
A80: x2 in dom H;
then consider s2 be Point of Tn1 such that
A81: x2=s2
and
A82: s2.N1>=0
and
A83: |.s2.|=1 by A17,A71,A72;
reconsider s1,s2 as Element of REAL N1 by EUCLID:22;
A84: 1 ^2 = |.s1|N .| ^2 + (s1.N1)^2 by REAL_NS1:10,A79;
A85: H.x2 = FF.x2 by A70,FUNCT_1:47,A80;
assume
A86: H.x1 = H.x2;
H.x1 = FF.x1 by A76,A70,FUNCT_1:47;
then
A87: s1|N = FF.s2 by A85,A86,A8,A77, A81
.= s2|N by A8;
then 1 ^2 = |.s1|N .| ^2 + (s2.N1)^2 by REAL_NS1:10,A83;
then
A88: s1.N1 = s2.N1 or s1.N1 = -s2.N1 by A84, SQUARE_1:40;
A89: s1.N1 >0 or s1.N1=0 by A78;
A90: len s2 = N1 by CARD_1:def 7;
len s1= N1 by CARD_1:def 7;
hence x1 = (s1|N)^<*s1.N1*> by FINSEQ_3:55, A77
.= x2 by FINSEQ_3:55, A88,A89,A82,A90,A87, A81;
end;
then
A91: H is one-to-one;
set TD=Tdisk(0.Tn,1);
set M=m1 | TD;
A92:dom M = the carrier of TD by FUNCT_2:def 1;
reconsider MM=M as continuous Function of TD,REAL
by TOPMETR:17,JORDAN5A:27;
A93:M= m1 | the carrier of TD by TMAP_1:def 4;
A94: for p be Point of Tn st p in the carrier of TD holds
MM.p = 1-(|.p.|*|.p.|)
proof
let x be Point of Tn;
NF.x = |.x.| by JGRAPH_4:def 1;
then NNF.x = |.x.| * |.x.| by VALUED_1:5;
then mNNF.x = -|.x.| * |.x.| by VALUED_1:8;
then m1.x = 1+-|.x.| * |.x.| by VALUED_1:2;
hence thesis by A93,FUNCT_1:49;
end;
A95: the carrier of TD = cl_Ball(0.Tn,1) by N,BROUWER:3;
A96: now
let r be Real;
assume
r in rng MM;
then consider x be object such that
A97: x in dom MM
and
A98: MM.x =r by FUNCT_1:def 3;
reconsider x as Point of Tn by A92,A95,A97;
|.x.| <= 1 by A97,A95,TOPREAL9:11;
then |.x.| * |.x.| <= 1 *1 by XREAL_1:66;
then 1-|.x.| * |.x.| >= 1-1*1 by XREAL_1:10;
hence r>=0 by A94,A97,A98;
end;
then MM is nonnegative-yielding by PARTFUN3:def 4;
then reconsider SQR = |[sqrt MM]| as continuous Function of TD,TOP-REAL 1;
A99:dom (sqrt MM)=dom MM by PARTFUN3:def 5;
A100: rng id TD = the carrier of TD;
dom id TD = the carrier of TD;
then reconsider ID=id TD as continuous Function of TD,Tn
by A100,FUNCT_2:2,A95,PRE_TOPC:26;
reconsider SQR as continuous Function of TD,TOP-REAL ONE;
reconsider II=ID^^SQR as continuous Function of TD,TOP-REAL (N+ONE);
reconsider II as continuous Function of TD,Tn1;
A101: dom II = the carrier of TD by FUNCT_2:def 1;
A102: dom SQR = (dom sqrt MM) by Def1;
for y,x be object holds y in rng H & x = II.y iff x in dom H & y = H.x
proof
let y,x be object;
hereby
assume that
A103: y in rng H
and
A104: x = II.y;
reconsider p=y as Point of Tn by A103, A73;
set p1 = 1-(|.p.|*|.p.|),sp =sqrt p1,ssp=|[ sp ]|;
A105: ID.p=p by A103,FUNCT_1:17;
A106: MM.p = 1-(|.p.|*|.p.|) by A103,A94;
then (sqrt MM).p = sp by A103,A92,PARTFUN3:def 5,A99;
then SQR.p = ssp by Def1,A99,A102, A103,A92;
then
A107: II.p = p^ssp by A103, A101,A105,PRE_POLY:def 4;
II.p in rng II by A103, A101,FUNCT_1:def 3;
then reconsider IIp=II.p as Point of Tn1;
MM.p in rng MM by A103,A92,FUNCT_1:def 3;
then
A109: MM.p >=0 by A96;
A110: sqr ssp = <*sp^2*> by RVSUM_1:55
.= <*MM.p*> by A109,SQUARE_1:def 2,A106;
sqr IIp = (sqr p) ^ (sqr ssp) by RVSUM_1:144,A107;
then Sum sqr IIp = Sum (sqr p) + MM.p by A110,RVSUM_1:74
.= |.p.|^2 + MM.p by TOPREAL9:5
.=1 by A106;
then
A111: |.IIp.| =1;
A112: len p = N by CARD_1:def 7;
then IIp.N1 = sp by A107, FINSEQ_1:42;
then
A113: IIp in Sp by A106,A109,A17,A111;
hence x in dom H by A104,A71, PRE_TOPC:def 5;
FF.IIp = H.IIp by A113,A71,A72,A70,FUNCT_1:47;
hence H.x = (p^ssp) |N by A8,A107,A104
.= (p^ssp) | (dom p) by A112,FINSEQ_1:def 3
.=y by FINSEQ_1:21;
end;
assume that
A114: x in dom H
and
A115: y = H.x;
consider p be Point of Tn1 such that
A116: x=p
and
A117: p.N1>=0
and
A118: |.p.|=1 by A114,A17,A71,A72;
A119: p|N is FinSequence of REAL by RVSUM_1:145;
len p = N1 by CARD_1:def 7;
then len (p|N) = N by NAT_1:11,FINSEQ_1:59;
then reconsider pN=p|N as Point of Tn by A119,TOPREAL7:17;
A121: p =pN ^<*p.N1*> by CARD_1:def 7,FINSEQ_3:55;
set p1 = 1-(|.pN.|*|.pN.|),sp =sqrt p1,ssp=|[ sp ]|;
A122: sqr <*p.N1*> = <*(p.N1)^2*> by RVSUM_1:55;
A123: pN-0.Tn = pN by VECTSP_1:18;
sqr p =sqr pN ^ sqr <*p.N1*> by A121,RVSUM_1:144;
then Sum sqr p = Sum sqr pN + (p.N1)^2 by RVSUM_1:74,A122
.= |.pN.|^2 + (p.N1)^2 by TOPREAL9:5;
then
A124: |.p.|^2 = |.pN.|^2 + (p.N1)^2 by TOPREAL9:5;
then |.p.|^2 >= |.pN.|^2 by XREAL_1:38;
then |.pN.| <= 1 by SQUARE_1:47,A118;
then
A125: pN in rng H by A123, A73;
then MM.pN = 1-(|.pN.|*|.pN.|) by A94;
then (sqrt MM).pN = sp by A125,A92,PARTFUN3:def 5,A99;
then
A126: SQR.pN = ssp by Def1,A99,A102, A125,A92;
A127: FF.p = p|N by A8;
hence y in rng H by A125,A115,A116, A114,A70,FUNCT_1:47;
ID.pN=pN by A125,FUNCT_1:17;
then II.pN = pN^ssp by A125, A101, A126,PRE_POLY:def 4;
then II.pN = p by A118,A124,A117,SQUARE_1:def 2,A121;
hence x = II.y by A115,A116, A127, A114,A70,FUNCT_1:47;
end;
then
A128: (H qua Function)"=II by A91, A101,A74,FUNCT_1:32;
dom (0*N1)=Seg N1;
then N0.N1 = 1 by A68,FUNCT_7:31;
then
A129: N0 in Sp by A69,A17;
for P being Subset of Tn1 |Sp holds P is open iff H.:P is open
proof
let P being Subset of Tn1 |Sp;
for i st i in dom F for h be Function of Tn1,R^1 st h = F.i holds
h is continuous
proof
let i such that
A130: i in dom F;
i <= N by A130,A6,FINSEQ_1:1;
then
A131: i <= N1 by NAT_1:13;
let h be Function of Tn1,R^1 such that
A132: h = F.i;
A133: h = PROJ(N1,i) by A130,A132,A7;
1 <= i by A130,A6,FINSEQ_1:1;
then i in Seg N1 by A131;
hence thesis by A133,TOPREALC:57;
end;
then
A134: FF is continuous by TIETZE_2:21;
FF| (Tn1|Sp) = FF|Sp by TMAP_1:def 4,A72;
then
A135: H is continuous by A134, A129,A70,PRE_TOPC:27;
hereby
rng II = dom H by A128,A91,FUNCT_1:33;
then reconsider ii=II as Function of TD,Tn1 |Sp by FUNCT_2:2,A101;
assume
A136: P is open;
A137: ii is continuous by PRE_TOPC:27;
dom H is non empty by A73,A71;
then ii"P is open by A137,A71,A136,TOPS_2:43;
hence H.:P is open by A75,FUNCT_1:def 4,FUNCT_1:84, A128;
end;
assume
A138: H.:P is open;
H"(H.:P)=P by A71, A75,FUNCT_1:def 4,FUNCT_1:94;
hence P is open by A138, TOPS_2:43,A135,A67;
end;
hence thesis by A71,A74,A91, A129,TOPGRP_1:25;
end;
let H be Function of Tn1 |Sn,TD such that
A139: H = FF|Sn;
A140: dom H = [#](Tn1 |Sn) by FUNCT_2:def 1;
A141: [#](Tn1 |Sn) = Sn by PRE_TOPC:def 5;
then
A142: rng H = (FF|Sn).:Sn by A140,A139,RELAT_1:113
.= cl_Ball(0.Tn,1) by A29,A54,RELAT_1:129;
then A143: rng H = [#]TD by PRE_TOPC:def 5;
A144: for x1,x2 be object st x1 in dom H & x2 in dom H & H.x1 =H.x2
holds x1=x2
proof
let x1,x2 be object;
assume
A145: x1 in dom H;
then consider s1 be Point of Tn1 such that
A146: x1=s1
and
A147: s1.N1<=0
and
A148: |.s1.|=1 by A28,A140,A141;
assume
A149: x2 in dom H;
then consider s2 be Point of Tn1 such that
A150: x2=s2
and
A151: s2.N1<=0
and
A152: |.s2.|=1 by A28,A140,A141;
reconsider s1,s2 as Element of REAL N1 by EUCLID:22;
A153: 1 ^2 = |.s1|N .| ^2 + (s1.N1)^2 by REAL_NS1:10,A148;
A154: H.x2 = FF.x2 by A139,FUNCT_1:47,A149;
assume
A155: H.x1 = H.x2;
H.x1 = FF.x1 by A145,A139,FUNCT_1:47;
then
A156: s1|N = FF.s2 by A154,A155,A8,A146, A150
.= s2|N by A8;
then 1 ^2 = |.s1|N .| ^2 + (s2.N1)^2 by REAL_NS1:10,A152;
then
A157: s1.N1 = s2.N1 or s1.N1 = -s2.N1 by A153, SQUARE_1:40;
A158: s1.N1 <0 or s1.N1=0 by A147;
A159: len s2 = N1 by CARD_1:def 7;
len s1= N1 by CARD_1:def 7;
hence x1 = (s1|N)^<*s1.N1*> by FINSEQ_3:55, A146
.= x2 by FINSEQ_3:55, A157,A158,A151,A159,A156, A150;
end;
then
A160: H is one-to-one;
set TD=Tdisk(0.Tn,1);
set M=m1 | TD;
A161: dom M = the carrier of TD by FUNCT_2:def 1;
reconsider MM=M as continuous Function of TD,REAL by TOPMETR:17,JORDAN5A:27;
reconsider Msqr=-sqrt MM as Function of TD,REAL;
A162: M= m1 | the carrier of TD by TMAP_1:def 4;
A163: for p be Point of Tn st p in the carrier of TD holds MM.p = 1-(|.p.|*
|.p.|)
proof
let x be Point of Tn;
NF.x = |.x.| by JGRAPH_4:def 1;
then NNF.x = |.x.| * |.x.| by VALUED_1:5;
then mNNF.x = -|.x.| * |.x.| by VALUED_1:8;
then m1.x = 1+-|.x.| * |.x.| by VALUED_1:2;
hence thesis by A162,FUNCT_1:49;
end;
A164: the carrier of TD = cl_Ball(0.Tn,1) by N,BROUWER:3;
A165:now
let r be Real;
assume r in rng MM;
then consider x be object such that
A166: x in dom MM
and
A167: MM.x =r by FUNCT_1:def 3;
reconsider x as Point of Tn by A161,A164,A166;
|.x.| <= 1 by A166,A164,TOPREAL9:11;
then |.x.| * |.x.| <= 1 *1 by XREAL_1:66;
then 1-|.x.| * |.x.| >= 1-1*1 by XREAL_1:10;
hence r>=0 by A163,A166,A167;
end;
then MM is nonnegative-yielding by PARTFUN3:def 4;
then reconsider SQR = |[Msqr]| as continuous Function of TD,TOP-REAL 1;
A168: dom (sqrt MM)=dom MM by PARTFUN3:def 5;
A169: rng id TD = the carrier of TD;
dom id TD = the carrier of TD;
then reconsider ID=id TD as continuous Function of TD,Tn
by A169,FUNCT_2:2,A164,PRE_TOPC:26;
reconsider SQR as continuous Function of TD,TOP-REAL ONE;
reconsider II=ID^^SQR as continuous Function of TD,TOP-REAL (N+ONE);
reconsider II as continuous Function of TD,Tn1;
A170: dom II = the carrier of TD by FUNCT_2:def 1;
dom (-sqrt MM)=dom sqrt MM by VALUED_1:8;
then
A171: dom SQR = (dom sqrt MM) by Def1;
for y,x be object holds y in rng H & x = II.y iff x in dom H & y = H.x
proof
let y,x be object;
hereby
assume that
A172: y in rng H
and
A173: x = II.y;
reconsider p=y as Point of Tn by A172, A142;
set p1 = 1-(|.p.|*|.p.|),sp =sqrt p1,ssp=|[ -sp ]|;
A174: ID.p=p by A172,FUNCT_1:17;
A175: MM.p = 1-(|.p.|*|.p.|) by A172,A163;
then (sqrt MM).p = sp by A172,A161,PARTFUN3:def 5,A168;
then Msqr.p = -sp by VALUED_1:8;
then SQR.p = ssp by Def1,A168,A171, A172,A161;
then
A176: II.p = p^ssp by A172, A170,A174,PRE_POLY:def 4;
II.p in rng II by A172, A170,FUNCT_1:def 3;
then reconsider IIp=II.p as Point of Tn1;
MM.p in rng MM by A172,A161,FUNCT_1:def 3;
then
A178: MM.p >=0 by A165;
A179: sqr IIp = (sqr p) ^ (sqr ssp) by RVSUM_1:144,A176;
sp^2 = (-sp)^2;
then sqr ssp = <*sp^2*> by RVSUM_1:55
.= <*MM.p*> by A178,SQUARE_1:def 2,A175;
then Sum sqr IIp = Sum (sqr p) + MM.p by A179,RVSUM_1:74
.= |.p.|^2 + MM.p by TOPREAL9:5
.= 1 by A175;
then
A180: |.IIp.| =1;
A181: len p = N by CARD_1:def 7;
then IIp.N1 = -sp by A176, FINSEQ_1:42;
then
A182: IIp in Sn by A175,A178,A28,A180;
hence x in dom H by A173,A140, PRE_TOPC:def 5;
FF.IIp = H.IIp by A182,A140,A141,A139,FUNCT_1:47;
hence H.x = (p^ssp) |N by A8,A176,A173
.= (p^ssp) | (dom p) by A181,FINSEQ_1:def 3
.= y by FINSEQ_1:21;
end;
assume that
A183: x in dom H
and
A184: y = H.x;
consider p be Point of Tn1 such that
A185: x=p
and
A186: p.N1<=0
and
A187: |.p.|=1 by A183,A28,A140,A141;
A188: p|N is FinSequence of REAL by RVSUM_1:145;
len p = N1 by CARD_1:def 7;
then len (p|N) = N by NAT_1:11,FINSEQ_1:59;
then reconsider pN=p|N as Point of Tn by A188,TOPREAL7:17;
A190: p =pN ^<*p.N1*> by CARD_1:def 7,FINSEQ_3:55;
A191: sqr <*p.N1*> = <*(p.N1)^2*> by RVSUM_1:55;
sqr p =sqr pN ^ sqr <*p.N1*> by A190,RVSUM_1:144;
then
A192: Sum sqr p = Sum sqr pN + (p.N1)^2 by RVSUM_1:74,A191
.= |.pN.|^2 + (p.N1)^2 by TOPREAL9:5;
then |.p.|^2 = |.pN.|^2 + (p.N1)^2 by TOPREAL9:5;
then |.p.|^2 >= |.pN.|^2 by XREAL_1:38;
then
A193: |.pN.| <= 1 by SQUARE_1:47,A187;
set p1 = 1-(|.pN.|*|.pN.|),sp =sqrt p1,ssp=|[ -sp ]|;
pN-0.Tn = pN by VECTSP_1:18;
then
A194: pN in rng H by A193, A142;
then MM.pN = 1-(|.pN.|*|.pN.|) by A163;
then (sqrt MM).pN = sp by A194,A161,PARTFUN3:def 5,A168;
then (Msqr).pN = -sp by VALUED_1:8;
then
A195: SQR.pN = ssp by Def1,A168,A171, A194,A161;
1^2 = |.pN.|^2 + (p.N1)^2 by A187, A192,TOPREAL9:5;
then
A196: -p.N1 = sqrt (1 - |.pN.|^2) by A186,SQUARE_1:23;
A197: FF.p = p|N by A8;
hence y in rng H by A194,A184,A185, A183,A139,FUNCT_1:47;
ID.pN=pN by A194,FUNCT_1:17;
then II.pN = pN^ssp by A194, A170, A195,PRE_POLY:def 4;
hence x = II.y by A196,A190,A184,A185, A197, A183,A139,FUNCT_1:47;
end;
then
A198: (H qua Function)"=II by A160, A170,A143,FUNCT_1:32;
|.N0.| = |. -1 .| by TOPREALC:13,A3
.= --1 by ABSVALUE:def 1;
then
A199:N0 in Sn by A28,A4;
for P being Subset of Tn1 |Sn holds P is open iff H.:P is open
proof
let P being Subset of Tn1 |Sn;
for i st i in dom F for h be Function of Tn1,R^1 st h = F.i
holds h is continuous
proof
let i such that
A200: i in dom F;
i <= N by A200,A6,FINSEQ_1:1;
then
A201: i <= N1 by NAT_1:13;
let h be Function of Tn1,R^1 such that
A202: h = F.i;
A203: h = PROJ(N1,i) by A200,A202,A7;
1 <= i by A200,A6,FINSEQ_1:1;
then i in Seg N1 by A201;
hence thesis by A203,TOPREALC:57;
end;
then
A204: FF is continuous by TIETZE_2:21;
FF| (Tn1|Sn) = FF|Sn by TMAP_1:def 4,A141;
then
A205:H is continuous by A204, A199,A139,PRE_TOPC:27;
hereby
rng II = dom H by A198,A160,FUNCT_1:33;
then reconsider ii=II as Function of TD,Tn1 |Sn by FUNCT_2:2,A170;
assume
A206: P is open;
A207: ii is continuous by PRE_TOPC:27;
dom H is non empty by A142,A140;
then ii"P is open by A207,A140,A206,TOPS_2:43;
hence H.:P is open by A144,FUNCT_1:def 4,FUNCT_1:84, A198;
end;
assume
A208: H.:P is open;
H"(H.:P)=P by A140, A144,FUNCT_1:def 4,FUNCT_1:94;
hence P is open by A208,TOPS_2:43,A205,A2;
end;
hence thesis by A140,A143,A160, A199,TOPGRP_1:25;
end;
theorem Th2:
for Sp,Sn be Subset of TOP-REAL n st
Sp = {s where s is Point of TOP-REAL n: s.n >= 0 & |.s.| = 1} &
Sn = {t where t is Point of TOP-REAL n: t.n <= 0 & |.t.| = 1}
holds Sp is closed & Sn is closed
proof
let Sp,Sn be Subset of TOP-REAL n such that
A1: Sp = {s where s is Point of TOP-REAL n: s.n>=0 & |.s.|=1}
and
A2: Sn= {t where t is Point of TOP-REAL n: t.n<=0 & |.t.|=1};
set Tn=TOP-REAL n;
per cases;
suppose
A4: n=0;
A5: Sn={}
proof
assume Sn<>{};
then consider x be object such that
A6: x in Sn by XBOOLE_0:def 1;
ex p be Point of Tn st x=p & p.n<=0 & |.p.|=1 by A2,A6;
hence contradiction by A4;
end;
Sp = {}
proof
assume Sp<>{};
then consider x be object such that
A7: x in Sp by XBOOLE_0:def 1;
ex p be Point of Tn st x=p & p.n>=0 & |.p.|=1 by A1,A7;
hence contradiction by A4;
end;
hence thesis by A5;
end;
suppose
A8: n>0;
set P2={ p where p is Point of Tn: 0<p/.n };
set P1={ p where p is Point of Tn: 0>p/.n };
A9: P1 c= the carrier of Tn
proof
let x be object;
assume x in P1;
then ex p be Point of Tn st p=x & 0>p/.n;
hence thesis;
end;
P2 c= the carrier of Tn
proof
let x be object;
assume x in P2;
then ex p be Point of Tn st p=x & 0<p/.n;
hence thesis;
end;
then reconsider P1,P2 as Subset of Tn by A9;
n in Seg n by FINSEQ_1:3,A8;
then reconsider P1,P2 as open Subset of Tn by JORDAN2B:13,12;
set S2=P2` /\ Sphere(0.Tn,1);
A10: Sn c= S2
proof
let xx be object;
assume xx in Sn;
then consider p be Point of Tn such that
A11: xx=p
and
A12: p.n<=0
and
A13: |.p.|=1 by A2;
p-0.Tn=p by RLVECT_1:13;
then
A14: p in Sphere(0.Tn,1) by A13;
len p =n by CARD_1:def 7;
then
A15: dom p = Seg n by FINSEQ_1:def 3;
A16: not p in P2
proof
assume p in P2;
then ex q be Point of Tn st p=q & 0<q/.n;
hence thesis by A15,PARTFUN1:def 6, FINSEQ_1:3,A8,A12;
end;
P2` = [#]Tn\P2 by SUBSET_1:def 4;
then p in P2` by A16,XBOOLE_0:def 5;
hence thesis by A14,XBOOLE_0:def 4,A11;
end;
A17: S2 c= Sn
proof
let xx be object;
A18: P2`=[#]Tn\P2 by SUBSET_1:def 4;
assume
A19: xx in S2;
then reconsider p=xx as Point of Tn;
len p =n by CARD_1:def 7;
then dom p = Seg n by FINSEQ_1:def 3;
then
A20: p/.n =p.n by PARTFUN1:def 6, FINSEQ_1:3,A8;
A21: p in P2` by A19,XBOOLE_0:def 4;
A22: p.n <= 0
proof
assume p.n >0;
then p in P2 by A20;
hence thesis by A21,A18,XBOOLE_0:def 5;
end;
p in Sphere(0.Tn,1) by A19,XBOOLE_0:def 4;
then |.p.|=1 by TOPREAL9:12;
hence thesis by A22,A2;
end;
set S1=P1` /\ Sphere(0.Tn,1);
A23: S1 c= Sp
proof
let xx be object;
A24: P1`=[#]Tn\P1 by SUBSET_1:def 4;
assume
A25: xx in S1;
then reconsider p=xx as Point of Tn;
len p =n by CARD_1:def 7;
then dom p = Seg n by FINSEQ_1:def 3;
then
A26: p/.n =p.n by PARTFUN1:def 6, FINSEQ_1:3,A8;
A27: p in P1` by A25,XBOOLE_0:def 4;
A28: p.n >= 0
proof
assume p.n <0;
then p in P1 by A26;
hence thesis by A27,A24,XBOOLE_0:def 5;
end;
p in Sphere(0.Tn,1) by A25,XBOOLE_0:def 4;
then |.p.|=1 by TOPREAL9:12;
hence thesis by A28,A1;
end;
Sp c= S1
proof
let xx be object;
assume xx in Sp;
then consider p be Point of Tn such that
A29: xx=p
and
A30: p.n>=0
and
A31: |.p.|=1 by A1;
p-0.Tn=p by RLVECT_1:13;
then
A32: p in Sphere(0.Tn,1) by A31;
len p =n by CARD_1:def 7;
then
A33: dom p = Seg n by FINSEQ_1:def 3;
A34: not p in P1
proof
assume p in P1;
then ex q be Point of Tn st p=q & 0>q/.n;
hence thesis by A33,PARTFUN1:def 6, FINSEQ_1:3,A8,A30;
end;
P1` = [#]Tn\P1 by SUBSET_1:def 4;
then p in P1` by A34,XBOOLE_0:def 5;
hence thesis by A32,XBOOLE_0:def 4,A29;
end;
hence thesis by A10,A17,XBOOLE_0:def 10,A23;
end;
end;
theorem Th3:
for TM be metrizable TopSpace st TM is finite-ind second-countable
for F be closed Subset of TM st ind (F`) <= n
for f be continuous Function of TM|F,Tunit_circle(n+1)
ex g being continuous Function of TM,Tunit_circle(n+1) st g|F=f
proof
defpred P[Nat] means
for TM be metrizable TopSpace st TM is finite-ind second-countable
for F be closed Subset of TM st ind F` <= $1
for f be continuous Function of TM|F,Tunit_circle($1 +1)
ex g being Function of TM,Tunit_circle($1+1) st g is continuous & g|F=f;
let TM be metrizable TopSpace such that
A1: TM is finite-ind second-countable;
let F be closed Subset of TM such that
A2: ind (F`) <= n;
A3:for n st P[n] holds P[n+1]
proof
let n;
set n1=n+1,n2=n1+1;
assume
A4: P[n];
set Tn1=TOP-REAL n1,Tn2=TOP-REAL n2,U=Tunit_circle(n1+1);
let TM be metrizable TopSpace;
assume
A5: TM is finite-ind second-countable;
let F be closed Subset of TM such that
A6: ind F` <= n1;
let f be continuous Function of (TM | F),U;
A7: [#](TM|F) = F by PRE_TOPC:def 5;
A8: dom f = the carrier of (TM|F) by FUNCT_2:def 1;
A9: dom f = the carrier of (TM|F) by FUNCT_2:def 1;
A10: [#](TM|F) = F by PRE_TOPC:def 5;
per cases;
suppose
A11: F is empty;
take g=TM-->the Point of U;
g|F={} by A11;
hence thesis by A11;
end;
suppose
A12: F is non empty;
set Sn= {p where p is Point of Tn2: p.n2<=0 & |.p.|=1};
set Sp= {p where p is Point of Tn2: p.n2>=0 & |.p.|=1};
A13: Sp c= the carrier of Tn2
proof
let x be object;
assume x in Sp;
then ex p be Point of Tn2 st p=x & p.n2>=0 & |.p.|=1;
hence thesis;
end;
Sn c= the carrier of Tn2
proof
let x be object;
assume x in Sn;
then ex p be Point of Tn2 st p=x & p.n2<=0 & |.p.|=1;
hence thesis;
end;
then reconsider Sp,Sn as Subset of Tn2 by A13;
A14: Sn = {t where t is Point of Tn2: t.(n1+1)<=0 & |.t.|=1};
A15: Sp = {l where l is Point of Tn2: l.(n1+1)>=0 & |.l.|=1};
then reconsider s1=Sp,s2=Sn as closed Subset of Tn2 by A14,Th2;
A16: [#] (Tn2|s2) = s2 by PRE_TOPC:def 5;
U = Tcircle(0.Tn2,1) by TOPREALB:def 7;
then
A17: the carrier of U = Sphere(0.Tn2,1) by TOPREALB:9;
A18: s1 c= the carrier of U
proof
let x be object;
assume x in s1;
then consider p be Point of Tn2 such that
A19: x=p
and
p.(n1+1)>=0
and
A20: |.p.|=1;
p-0.Tn2 = p by RLVECT_1:13;
hence thesis by A20,A19,A17;
end;
A21: s2 c= the carrier of U
proof
let x be object;
assume x in s2;
then consider p be Point of Tn2 such that
A22: x=p
and
p.(n1+1)<=0
and
A23: |.p.|=1;
p-0.Tn2 = p by RLVECT_1:13;
hence thesis by A23,A22,A17;
end;
then reconsider S1=s1,S2=s2 as Subset of U by A18;
reconsider A1=f"S1,A2=f"S2 as Subset of TM by A7,XBOOLE_1:1;
A24: f.:(A1/\A2) c= (f.:A1) /\(f.:A2) by RELAT_1:121;
A25: f.:A2 c= s2 by FUNCT_1:75;
S1 is closed by TSEP_1:8;
then f"S1 is closed by PRE_TOPC:def 6;
then
A26: A1 is closed by A7,TSEP_1:8;
Sphere(0.Tn2,1) c= S1\/S2
proof
let x be object;
assume
A27: x in Sphere(0.Tn2,1);
then reconsider p=x as Point of Tn2;
A28: p.n2 >=0 or p.n2 <=0;
|.p.| = 1 by A27,TOPREAL9:12;
then p in Sp or p in Sn by A28;
hence thesis by XBOOLE_0:def 3;
end;
then rng f c= S1\/S2 by A17;
then
A29: f"rng f c= f"(S1\/S2) by RELAT_1:143;
f"rng f = dom f by RELAT_1:134;
then
A30: F = f"(S1\/S2) by A29,A7,FUNCT_2:def 1;
then
A31: F = A1\/A2 by RELAT_1:140;
then reconsider TFA12=A1/\A2 as Subset of TM|F by XBOOLE_1:29,A10;
A32: [#]((TM|F) |TFA12) =TFA12 by PRE_TOPC:def 5;
reconsider fa=f|TFA12 as Function of (TM|F) |TFA12,U| (f.:TFA12)
by A10,A12,JORDAN24:12;
A33: fa is continuous by JORDAN24:13, A10,A12;
dom f /\ TFA12 = TFA12 by A8,XBOOLE_1:28;
then
A34: dom fa=the carrier of ((TM|F) |TFA12) by A32, RELAT_1:61;
A35: (TM|F) | (f"S1) = TM|A1 by PRE_TOPC:7, A7;
then reconsider f1=f|A1 as Function of TM|A1,U| (f.:A1)
by A12,A7,JORDAN24:12;
A36: f1 is continuous by A35, A12,A10,JORDAN24:13;
A37: rng f1 c=the carrier of (U| (f.:A1));
A38: [#](U| (f.:A1))= f.:A1 by PRE_TOPC:def 5;
then
A39: rng f1 c= the carrier of U by XBOOLE_1:1;
A40: (TM|F) | (f"S2) = TM|A2 by PRE_TOPC:7, A7;
then reconsider f2=f|A2 as Function of TM|A2,U| (f.:A2)
by A12,A7,JORDAN24:12;
A41: f2 is continuous by A40, A12,A10,JORDAN24:13;
A42: [#](U| (f.:A2))= f.:A2 by PRE_TOPC:def 5;
then
A43: rng f2 c= the carrier of U by XBOOLE_1:1;
dom f1 = dom f/\A1 by RELAT_1:61;
then
A44: dom f1 = A1 by A9,XBOOLE_1:28;
[#](TM|A1) = A1 by PRE_TOPC:def 5;
then reconsider f1 as Function of TM|A1,U by A39,FUNCT_2:2,A44;
A45: rng f2 c=the carrier of (U| (f.:A2));
dom f2 = dom f/\A2 by RELAT_1:61;
then
A46: dom f2 = A2 by A9,XBOOLE_1:28;
[#](TM|A2) = A2 by PRE_TOPC:def 5;
then reconsider f2 as Function of TM|A2,U by A43,A46,FUNCT_2:2;
f.:A2 c= s2 by FUNCT_1:75;
then
A47: rng f2 c= s2 by A42,A45;
S2 is closed by TSEP_1:8;
then f"S2 is closed by PRE_TOPC:def 6;
then
A48: A2 is closed by A7,TSEP_1:8;
TM|F` is second-countable by A5;
then consider X1,X2 be closed Subset of TM such that
A49: [#]TM = X1\/X2
and
A50: A1 c=X1
and
A51: A2 c=X2
and
A52: A1/\X2=A1/\A2
and
A53: A1/\A2=X1/\A2
and
A54: ind((X1/\X2)\(A1/\A2))<=n1 qua ExtReal -1
by A31,TOPDIM_2:24,A5,A6,A26,A48;
set TX=TM| (X1/\X2);
A55: [#]TX = X1/\X2 by PRE_TOPC:def 5;
then reconsider TXA12=A1/\A2 as Subset of TX by A50,A51,XBOOLE_1:27;
(X1/\X2)\(A1/\A2)=TXA12` by A55,SUBSET_1:def 4;
then
A56: ind TXA12` <= n by A5,TOPDIM_1:21,A54;
set Un=Tunit_circle(n+1);
set TD=Tdisk(0.Tn1,1);
deffunc ff(Nat)=PROJ(n2,$1);
consider FF be FinSequence such that
A57: len FF = n1 & for k be Nat st k in dom FF holds FF.k=ff(k)
from FINSEQ_1:sch 2;
A58: rng FF c= Funcs(the carrier of Tn2,the carrier of R^1)
proof
let x be object;
assume x in rng FF;
then consider i be object such that
A59: i in dom FF
and
A60: FF.i = x by FUNCT_1:def 3;
reconsider i as Nat by A59;
ff(i) in Funcs(the carrier of Tn2,the carrier of R^1)
by FUNCT_2:8;
hence thesis by A57,A59,A60;
end;
A61: Ball(0.Tn1,1) c= Int cl_Ball(0.Tn1,1) by TOPREAL9:16,TOPS_1:24;
then
A62: cl_Ball(0.Tn1,1) is compact non boundary convex;
reconsider FF as FinSequence of
Funcs(the carrier of Tn2,the carrier of R^1) by A58,FINSEQ_1:def 4;
reconsider FF as Element of n1-tuples_on
Funcs(the carrier of Tn2,the carrier of R^1) by A57,FINSEQ_2:92;
set FFF=<:FF:>;
A63: s1/\s2 c= s2 by XBOOLE_1:17;
A64: FFF.:s2= cl_Ball(0.Tn1,1) by A57,Th1,A15;
then
A65: s2 is non empty;
A66: dom FFF=the carrier of Tn2 by FUNCT_2:def 1;
then s1/\dom FFF=s1 by XBOOLE_1:28;
then
A67: dom (FFF|s1)= s1 by RELAT_1:61;
s2/\dom FFF=s2 by XBOOLE_1:28,A66;
then
A68: dom (FFF|s2)= s2 by RELAT_1:61;
A69: the carrier of TD = cl_Ball(0.Tn1,1) by BROUWER:3;
then rng (FFF|s2) c= the carrier of TD by RELAT_1:115,A64;
then reconsider Fs2=FFF|s2 as Function of Tn2|s2,TD
by FUNCT_2:2,A16,A68;
A70: [#](Tn2|s1) = s1 by PRE_TOPC:def 5;
Fs2 is being_homeomorphism by A57,Th1,A15;
then
A71: s2,cl_Ball(0.Tn1,1) are_homeomorphic
by T_0TOPSP:def 1,METRIZTS:def 1;
A72: FFF.:s1= cl_Ball(0.Tn1,1) by A57,Th1,A14;
then
A73: s1 is non empty;
rng (FFF|s1) c= the carrier of TD by RELAT_1:115, A72,A69;
then reconsider Fs1=FFF|s1 as Function of Tn2|s1,TD
by A67,FUNCT_2:2,A70;
A74: Fs1.:(s1/\s2) c= FFF.:(s1/\s2) by RELAT_1:128;
A75: Fs1 is being_homeomorphism by A57,Th1,A14;
then
A76: rng Fs1 = [#]TD by TOPS_2:def 5;
f.:A1 c= s1 by FUNCT_1:75;
then WE: (f.:A1)/\(f.:A2) c= s1/\s2 by A25,XBOOLE_1:27;
then f.:(A1/\A2) c= s1/\s2 by A24;
then
A78: Fs1.:(f.:(A1/\A2)) c= Fs1.:(s1/\s2) by RELAT_1:123;
s1/\s2 c= s1 by XBOOLE_1:17;
then
A79: f.:(A1/\A2) c= s1 by WE,A24;
[#](U| (f.:TFA12))=f.:TFA12 by PRE_TOPC:def 5;
then
A80: rng fa c= the carrier of Tn2|s1 by A79,A70;
then reconsider fa as Function of (TM|F) |TFA12,U
by XBOOLE_1:1,A70,A34,FUNCT_2:2;
A81: fa is continuous by A33,PRE_TOPC:26;
rng fa c= the carrier of Tn2 by A17,XBOOLE_1:1;
then reconsider fa as Function of (TM|F) |TFA12,Tn2 by FUNCT_2:2,A34;
A82: fa is continuous by A81,PRE_TOPC:26;
A83: Fs1" is continuous by A75,TOPS_2:def 5;
A84: FFF.:(s1/\s2) = Sphere(0.Tn1,1) by A57,Th1;
then Fs1.:(s1/\s2) = Sphere(0.Tn1,1) by XBOOLE_1:17,RELAT_1:129;
then
A85: (Fs1").:Sphere(0.Tn1,1) = Fs1"(Fs1.:(s1/\s2)) by TOPS_2:55,A75,A76
.= s1/\s2 by FUNCT_1:94,A67,A75,XBOOLE_1:17;
set A2X=A2 \/ (X1/\X2);
set A1X=A1 \/ (X1/\X2);
A86: X2=[#](TM|X2) by PRE_TOPC:def 5;
(TM|F) |TFA12 = TM| (A1/\A2) by PRE_TOPC:7, A31,XBOOLE_1:29;
then
A87: (TM|F) |TFA12 = TX |TXA12 by PRE_TOPC:7,A50,A51,XBOOLE_1:27;
then reconsider fa as Function of TX |TXA12,Tn2|s1
by A34,FUNCT_2:2,A80;
reconsider Ffa=Fs1*fa as Function of TX|TXA12,TD by A73;
A88: [#](TX |TXA12) = TXA12 by PRE_TOPC:def 5;
then
A89: dom Ffa = A1/\A2 by FUNCT_2:def 1;
rng Ffa = Ffa.:dom Ffa by RELAT_1:113
.= (Fs1*fa).:(A1/\A2) by A88,FUNCT_2:def 1
.= Fs1.:(fa.:(A1/\A2)) by RELAT_1:126;
then E: rng Ffa c= Fs1.:(f.:(A1/\A2)) by RELAT_1:123, RELAT_1:128;
then
A90: rng Ffa c= Fs1.:(s1/\s2) by A78;
A91: rng Ffa c= Sphere(0.Tn1,1) by E,A78,A74,A84;
fa is continuous by A82,PRE_TOPC:27,A87;
then
A92: Ffa is continuous by TOPS_2:46, A75, A73;
reconsider Ffa as Function of TX |TXA12,Tn1
by A91,XBOOLE_1:1,FUNCT_2:2,A89,A88;
Un = Tcircle(0.Tn1,1) by TOPREALB:def 7;
then
A93: the carrier of Un = Sphere(0.Tn1,1) by TOPREALB:9;
then reconsider H=Ffa as Function of TX |TXA12,Un
by FUNCT_2:2,A89,A88,A90,A74,XBOOLE_1:1,A84;
Ffa is continuous by A92,PRE_TOPC:26;
then reconsider H as continuous Function of TX |TXA12,Un
by PRE_TOPC:27;
TXA12 is closed by A26,A48,TSEP_1:8;
then consider g be Function of TX, Un such that
A94: g is continuous
and
A95: g|TXA12 = H by A5,A56, A4;
A96: rng g c= the carrier of Tn1 by A93,XBOOLE_1:1;
A97: dom g=the carrier of TX by FUNCT_2:def 1;
A98: rng g c= the carrier of Un;
reconsider g as Function of TX, Tn1 by A97,A96,FUNCT_2:2;
A99: g is continuous by A94,PRE_TOPC:26;
the carrier of Un c= the carrier of TD by A93,A69,TOPREAL9:17;
then reconsider g as Function of TX,TD by A98,XBOOLE_1:1,FUNCT_2:2,A97;
reconsider G=(Fs1")*g as Function of TX,Tn2|s1;
A100: dom G = the carrier of TX by FUNCT_2:def 1,A73;
g is continuous by A99,PRE_TOPC:27;
then
A101: G is continuous by A83,TOPS_2:46;
A102: rng G c= s1 by A70;
then reconsider G as Function of TX,Tn2 by XBOOLE_1:1,FUNCT_2:2,A100;
A103: G is continuous by PRE_TOPC:26,A101;
reconsider G as Function of TX,U by A18,A102,XBOOLE_1:1,FUNCT_2:2,A100;
A104: G is continuous by PRE_TOPC:27,A103;
A105: rng fa c= dom Fs1 by A67,A70;
A106: G|TXA12 = (Fs1")*(g|TXA12) by RELAT_1:83
.= (Fs1"*Fs1)*fa by RELAT_1:36, A95
.= (id dom Fs1)*fa by TOPS_2:52, A75,A76
.= fa by RELAT_1:53,A105;
A107: now
let xx be object;
assume
A108: xx in dom f1/\dom G;
then
A109: xx in A1 by A44,XBOOLE_0:def 4;
xx in X2 by A108,A55,XBOOLE_0:def 4;
then
A110: xx in A1/\A2 by A109,A52,XBOOLE_0:def 4;
hence G.xx = (G|TXA12).xx by FUNCT_1:49
.= f.xx by A110,FUNCT_1:49,A106
.= f1.xx by A109,FUNCT_1:49;
end;
A111: now
let xx be object;
assume
A112: xx in dom f2/\dom G;
then
A113: xx in A2 by A46,XBOOLE_0:def 4;
xx in X1 by A112,A55,XBOOLE_0:def 4;
then
A114: xx in A1/\A2 by A113,A53,XBOOLE_0:def 4;
hence G.xx = (G|TXA12).xx by FUNCT_1:49
.= f.xx by A114,FUNCT_1:49, A106
.= f2.xx by A113,FUNCT_1:49;
end;
rng G = G.:dom G by RELAT_1:113
.= (Fs1").:(g.:dom G) by RELAT_1:126
.= (Fs1").:(rng g) by A97,A100,RELAT_1:113;
then rng G c= s1/\s2 by A85,A93,A98,RELAT_1:123;
then rng G c= s2 by A63;
then
A115: rng f2 \/rng G c= s2 by XBOOLE_1:8, A47;
f2 is continuous by A41,PRE_TOPC:26;
then reconsider f2G=f2+*G as continuous Function of TM|A2X,U
by A111,PARTFUN1:def 4,A104,A48,TOPGEN_5:10;
A116: dom f2G = the carrier of TM|A2X by FUNCT_2:def 1;
A117: rng f2G c= rng f2 \/rng G by FUNCT_4: 17;
then rng f2G c= s2 by A115;
then reconsider f2G as Function of TM|A2X,Tn2
by XBOOLE_1:1,FUNCT_2:2,A116;
A118: f2G is continuous by PRE_TOPC:26;
reconsider f2G as Function of TM|A2X,Tn2|s2
by FUNCT_2:2,A116,A115,A117,XBOOLE_1:1,A16;
cl_Ball(0.Tn1,1) is compact non boundary convex by A61;
then consider H2 being Function of TM,Tn2|s2 such that
A119: H2 is continuous
and
A120: H2|A2X=f2G by A118,PRE_TOPC:27,A71, TIETZE_2:24, A48;
A121: TM is non empty by A12;
then reconsider H2X=H2|X2 as Function of TM|X2,(Tn2|s2) | (H2.:X2)
by JORDAN24:12,A65;
A122: H2X is continuous by JORDAN24:13,A65,A121,A119;
dom H2 = the carrier of TM by FUNCT_2:def 1,A65;
then
A123: dom H2X = X2/\the carrier of TM by RELAT_1:61;
then
A124: dom H2X= the carrier of TM|X2 by XBOOLE_1:28,A86;
f1 is continuous by A36,PRE_TOPC:26;
then reconsider f1G=f1+*G as continuous Function of TM|A1X,U
by A107,PARTFUN1:def 4,A104,A26,TOPGEN_5:10;
A125: dom f1G = the carrier of TM|A1X by FUNCT_2:def 1;
f.:A1 c= s1 by FUNCT_1:75;
then rng f1 c= s1 by A38,A37;
then
A126: rng f1 \/rng G c= s1 by A102,XBOOLE_1:8;
A127: rng f1G c= rng f1 \/rng G by FUNCT_4:17;
then rng f1G c= s1 by A126;
then reconsider f1G as Function of TM|A1X,Tn2
by XBOOLE_1:1,FUNCT_2:2,A125;
A128: f1G is continuous by PRE_TOPC:26;
reconsider f1G as Function of TM|A1X,Tn2|s1
by FUNCT_2:2,A125, A126,A127,XBOOLE_1:1,A70;
s1,cl_Ball(0.Tn1,1) are_homeomorphic
by T_0TOPSP:def 1,A75,METRIZTS:def 1;
then consider H1 being Function of TM,Tn2|s1 such that
A129: H1 is continuous
and
A130: H1|A1X=f1G by A62,A26,A128,PRE_TOPC:27,TIETZE_2:24;
reconsider H1X=H1|X1 as Function of TM|X1,(Tn2|s1) | (H1.:X1)
by A121,JORDAN24:12,A73;
A131: H1X is continuous by JORDAN24:13,A73,A121,A129;
[#]((Tn2|s1) | (H1.:X1)) = (H1.:X1) by PRE_TOPC:def 5;
then
A132: rng H1X c= the carrier of Tn2|s1 by XBOOLE_1:1;
dom H1 = the carrier of TM by FUNCT_2:def 1,A73;
then
A133: dom H1X = X1/\the carrier of TM by RELAT_1:61;
then
A134: dom H1X= X1 by XBOOLE_1:28;
X1=[#](TM|X1) by PRE_TOPC:def 5;
then
A135: dom H1X= the carrier of TM|X1 by A133,XBOOLE_1:28;
then reconsider H1X as Function of TM|X1,Tn2|s1 by A132, FUNCT_2:2;
A136: H1X is continuous by A131,PRE_TOPC:26;
A137: rng H1X c= s1 by A70;
[#]((Tn2|s2) | (H2.:X2)) = (H2.:X2) by PRE_TOPC:def 5;
then rng H2X c= the carrier of Tn2|s2 by XBOOLE_1:1;
then reconsider H2X as Function of TM|X2,Tn2|s2 by A124, FUNCT_2:2;
A138: H2X is continuous by A122,PRE_TOPC:26;
reconsider H1X as Function of TM|X1,Tn2
by A137,XBOOLE_1:1,A135,FUNCT_2:2;
A139: rng H2X c= s2 by A16;
then reconsider H2X as Function of TM|X2,Tn2
by XBOOLE_1:1,A124,FUNCT_2:2;
A140: H2X is continuous by A138,PRE_TOPC:26;
A141: now
let xx be object;
assume
A142: xx in dom H1X/\dom H2X;
then
A143: H2X.xx=H2.xx by A86,FUNCT_1:49;
xx in X1 by A142,A134,XBOOLE_0:def 4;
then
A144: H1X.xx=H1.xx by FUNCT_1:49;
A145: xx in X1/\X2 by A142, A123,XBOOLE_1:28,A134;
then
A146: xx in A2X by XBOOLE_0:def 3;
xx in A1X by A145, XBOOLE_0:def 3;
then
A147: H1.xx = (H1|A1X).xx by FUNCT_1:49;
A148: f2G.xx=G.xx by A145,A100,A55,FUNCT_4:13;
f1G.xx = G.xx by A145,A100,A55,FUNCT_4:13;
hence H1X.xx = H2X.xx
by A148,A147,A146,FUNCT_1:49,A144,A143,A120,A130;
end;
H1X is continuous by A136,PRE_TOPC:26;
then reconsider H12=H1X+*H2X as continuous Function of
TM| (X1\/X2),Tn2 by A140,A141,PARTFUN1:def 4,TOPGEN_5:10;
A149: TM| (X1\/X2) = the TopStruct of TM by A49,TSEP_1:93;
then reconsider H12 as Function of TM,Tn2;
A150: rng H12 c= rng H1X \/ rng H2X by FUNCT_4:17;
F/\X1 = (A1\/A2)/\X1 by A30,RELAT_1:140
.= (A1/\X1)\/(A2/\X1) by XBOOLE_1:23
.= A1 \/(A2/\X1) by A50,XBOOLE_1:28
.= A1 by A53,XBOOLE_1:17,XBOOLE_1:12;
then
A151: H1X|F= H1|A1 by RELAT_1:71;
f1G=G+*f1 by A107,PARTFUN1:def 4,FUNCT_4:34;
then
A152: f1G|A1 =f1 by FUNCT_4:23, A44;
A153: F/\X2 = (A1\/A2)/\X2 by A30,RELAT_1:140
.= (A1/\X2)\/(A2/\X2) by XBOOLE_1:23
.= (A1/\X2)\/A2 by A51,XBOOLE_1:28
.= A2 by A52,XBOOLE_1:17,XBOOLE_1:12;
A154: H2|A2 = f2G|A2 by A120,RELAT_1:74, XBOOLE_1:7;
rng H1X \/ rng H2X c= s1\/s2 by A139,A137,XBOOLE_1:13;
then
A155: rng H12 c= s1\/s2 by A150;
A156: dom H12 = the carrier of TM by FUNCT_2:def 1;
A157: H12 is continuous by PRE_TOPC:32,A149;
s1\/s2 c= Sphere(0.Tn2,1) by A18, A21,A17,XBOOLE_1:8;
then reconsider H12 as Function of TM,U
by A155,XBOOLE_1:1,A17,A156,FUNCT_2:2;
take H12;
thus H12 is continuous by PRE_TOPC:27,A157;
A158: H1|A1 = f1G|A1 by A130,XBOOLE_1:7,RELAT_1:74;
f2G=G+*f2 by A111,PARTFUN1:def 4,FUNCT_4:34;
then
A159: f2G|A2 =f2 by FUNCT_4:23,A46;
thus H12|F = H1X|F +*H2X|F by FUNCT_4:71
.= f1+*f2 by A152,A159,A158,A154,A151, RELAT_1:71,A153
.= f| (A1\/A2) by FUNCT_4:78
.= f by A31,A10;
end;
end;
let f be continuous Function of TM|F,Tunit_circle(n+1);
A160:P[0 qua Nat]
proof
reconsider Z=0 as Real;
set TR=TOP-REAL 1,U=Tunit_circle(0+1);
let TM be metrizable TopSpace;
assume
A161: TM is finite-ind second-countable;
let F be closed Subset of TM;
assume
A162: ind F` <= 0;
let f be continuous Function of TM|F,U;
A164: f"rng f = f"(the carrier of U) by RELAT_1:143,135;
U = Tcircle(0.TR,1) by TOPREALB:def 7;
then
A165: the carrier of U = Sphere(0.TR,1) by TOPREALB:9;
0.TR = 0*(0+1) by EUCLID:70
.= <*0 *> by FINSEQ_2:59;
then
A166: {<* Z qua ExtReal-1 *>,<* Z qua ExtReal+1 *>} =Fr Ball(0.TR,1)
by TOPDIM_2:18;
A167: Fr Ball(0.TR,1)= Sphere(0.TR,1) by JORDAN:24;
then reconsider mONE = <*-1*>,ONE=<*1*> as Point of U
by A165,TARSKI:def 2,A166;
reconsider Q={ONE},Q1={mONE} as closed Subset of U;
set F1=f"Q,F2=f"Q1;
A168: [#](TM|F)=F by PRE_TOPC:def 5;
then reconsider A1=F1,A2=F2 as Subset of TM by XBOOLE_1:1;
A169: dom f = F by A168,FUNCT_2:def 1;
Q\/Q1 = the carrier of U by A166,A167,A165,ENUMSET1:1;
then
A170: F1\/F2 = f"(the carrier of U) by RELAT_1:140
.= F by A164,RELAT_1:134,A169;
F2 is closed by PRE_TOPC:def 6;
then
A171: A2 is closed by TSEP_1:8,A168;
F1 is closed by PRE_TOPC:def 6;
then
A172: A1 is closed by TSEP_1:8,A168;
ONE<>mONE
proof
assume ONE=mONE;
then <*1*>.1 = -1 by FINSEQ_1:40;
hence thesis;
end;
then W: F1 misses F2 by ZFMISC_1:11,FUNCT_1:71;
TM|F` is second-countable by A161;
then consider X1,X2 be closed Subset of TM such that
A174: [#]TM = X1\/X2
and
A175: A1 c=X1
and
A176: A2 c=X2
and A1/\X2=A1/\A2 & A1/\A2=X1/\A2
and
A177: ind((X1/\X2)\(A1/\A2))<=0 qua ExtReal-1
by A161,A162,A170,TOPDIM_2:24,A172,A171;
ind (X1/\X2) >= -1 by TOPDIM_1:5,A161;
then
A178: X1/\X2 is empty by A177,W,XXREAL_0:1,TOPDIM_1:6,A161;
set h1=(TM|X1)-->ONE,h2=(TM|X2)-->mONE;
A179: [#](TM|X1)=X1 by PRE_TOPC:def 5;
A180: dom h2 = the carrier of (TM|X2);
A181: [#](TM|X2)=X2 by PRE_TOPC:def 5;
dom h1 = the carrier of (TM|X1);
then h1 tolerates h2
by A178,A179,A180,A181,XBOOLE_0:def 7,PARTFUN1:56;
then reconsider h12=h1+*h2 as continuous Function of TM| ([#]TM),U
by A174, TOPGEN_5:10;
[#] (TM| ([#]TM)) = [#]TM by PRE_TOPC:def 5;
then reconsider H12=h12 as Function of TM,U;
A182: for x be object st x in F holds (H12|F).x = f.x
proof
let x be object;
assume
A183: x in F;
then
A184: (H12|F).x=h12.x by FUNCT_1:49;
per cases by A183,A170,XBOOLE_0:def 3;
suppose
A185: x in F1;
then not x in dom h2 by A175,A178,XBOOLE_0:def 4,A181;
then
A186: H12.x=h1.x by FUNCT_4:11;
A187: f.x in {ONE} by A185,FUNCT_1:def 7;
h1.x = ONE by A185,A175,A179,FUNCOP_1:7;
hence thesis by A187,TARSKI:def 1,A186,A184;
end;
suppose
A188: x in F2;
then
A189: f.x in {mONE} by FUNCT_1:def 7;
A190: h2.x = mONE by A188,A176,A181,FUNCOP_1:7;
H12.x=h2.x by A188,A176,A180,A181,FUNCT_4:13;
hence thesis by A189,TARSKI:def 1,A190,A184;
end;
end;
take H12;
TM| ([#]TM) = the TopStruct of TM by TSEP_1:93;
hence H12 is continuous by PRE_TOPC:32;
dom H12 = the carrier of TM by FUNCT_2:def 1;
then dom (H12|F)=F by RELAT_1:62;
hence thesis by A182,A168,FUNCT_2:def 1;
end;
for n holds P[n] from NAT_1:sch 2(A160,A3);
then ex g be Function of TM, Tunit_circle(n+1) st
g is continuous & g|F=f by A1,A2;
hence thesis;
end;
theorem Th4:
not p in A & r>0 implies
ex h be Function of (TOP-REAL n) |A,(TOP-REAL n) |Sphere(p,r) st
h is continuous & h|Sphere(p,r) = id (A/\Sphere(p,r))
proof
set TR=TOP-REAL n;
assume that
A1: not p in A
and
A2: r>0;
set S=Sphere(p,r);
per cases;
suppose
A3: A is empty;
set h = the continuous Function of TR|A,TR;
reconsider H=h as Function of TR|A,TR|S by A3;
take H;
thus thesis by A3,PRE_TOPC:27;
end;
suppose
A4: A is non empty;
A<>{p} by A1,TARSKI:def 1;
then
A5: A\{p} <>{} by A4,ZFMISC_1:58;
set TRS=TR|S;
set nN=n NormF,t=transl(-p,TR),P=transl(p,TR);
A6: A\{p} c= (the carrier of TR)\{p} by XBOOLE_1:33;
(the carrier of TR)\{p}={p}` by SUBSET_1:def 4;
then reconsider cTRp=(the carrier of TR)\{p} as
non empty open Subset of TR by A5,A6;
set TRp=TR|cTRp,tt=t|TRp;
A7: [#]TRp = cTRp by PRE_TOPC:def 5;
then reconsider AA=A as Subset of TRp by A1,ZFMISC_1:57,A6;
reconsider Ir=tt[#]r as Function of TRp,TR by TOPREALC:37;
reconsider IrNt=Ir</>(nN*tt) as Function of TRp,TR by TOPREALC:46;
A8: tt = t|the carrier of TRp by TMAP_1:def 4;
not 0 in rng(nN*tt)
proof
assume 0 in rng(nN*tt);
then consider x be object such that
A9: x in dom (nN*tt)
and
A10: (nN*tt).x=0 by FUNCT_1:def 3;
tt.x in dom nN by A9,FUNCT_1:11;
then reconsider Tx=tt.x as Point of TR;
reconsider Tx as Element of REAL n by EUCLID:22;
A11: x in dom tt by A9,FUNCT_1:11;
then
A12: t.x=tt.x by A8,FUNCT_1:47;
x in dom t by A11,A8,RELAT_1:57;
then reconsider X=x as Point of TR;
0 = nN.Tx by A9,FUNCT_1:12,A10
.= |.Tx.| by JGRAPH_4:def 1;
then 0*n=Tx by EUCLID:8;
then 0.TR = Tx by EUCLID:70
.= -p+X by A12,RLTOPSP1:def 10;
then X = --p by RLVECT_1:def 10
.=p;
then x in {p} by TARSKI:def 1;
hence contradiction by A9,A7,XBOOLE_0:def 5;
end;
then nN*tt is non-empty by RELAT_1:def 9;
then reconsider IrNt as continuous Function of TRp,TR;
set h=(P*IrNt) | (TRp|AA);
A13: h= (P*IrNt) | the carrier of (TRp|AA) by TMAP_1:def 4;
reconsider h as continuous Function of (TRp|AA),TR by A4;
(TRp|AA) = TR|A by PRE_TOPC:7, A7;
then reconsider h as continuous Function of (TR|A),TR;
A14: [#](TR|A)=A by PRE_TOPC:def 5;
then
A15: dom h = A by FUNCT_2:def 1;
A16: dom tt = cTRp by A7,FUNCT_2:def 1;
A17: rng h c= S
proof
let y be object;
assume y in rng h;
then consider x be object such that
A18: x in dom h
and
A19: h.x=y by FUNCT_1:def 3;
reconsider x as Point of TR by A18,A15;
tt.x=t.x by A7,A18,A15,FUNCT_1:47,A8,A16;
then
A20: tt.x = -p+x by RLTOPSP1:def 10;
dom (nN*tt) = cTRp by A7,FUNCT_2:def 1;
then (nN*tt).x = nN.(tt.x) by A7,A18,A15,FUNCT_1:12;
then
A21: (nN*tt).x = |.-p+x.| by A20,JGRAPH_4:def 1;
A22: x in dom (P*IrNt) by A13,A18,RELAT_1:57;
then x in dom IrNt by FUNCT_1:11;
then
A23: IrNt.x = Ir.x (/) (nN*tt).x by VALUED_2:72;
dom Ir = cTRp by A7,FUNCT_2:def 1;
then Ir.x = r*(-p+x) by A20, A7,A18,A15,VALUED_2:def 39;
then
A24: IrNt.x = (1 / |.-p+x.|)*(r*(-p+x)) by A21,A23,VALUED_2:def 32;
then reconsider Fx=IrNt.x as Point of TR;
h.x = (P*IrNt).x by A13,A18,FUNCT_1:47;
then
A25: h.x = P.Fx by A22,FUNCT_1:12
.= p+Fx by RLTOPSP1:def 10;
--p=p;
then -p+x<>0.TR by A18,A1,A15,RLVECT_1:6;
then
A26: -p+x<>0*n by EUCLID:70;
A27: -p+x is Element of REAL n by EUCLID:22;
A28: p+Fx-p = Fx+(p+-p) by RLVECT_1:def 3
.= Fx+0.TR by RLVECT_1:def 10
.= Fx by RLVECT_1:def 4;
|.Fx.| = |.((1 / |.-p+x.|)*r)*(-p+x).| by A24,RLVECT_1:def 7
.= |. (1 / |.-p+x.|)*r .|* |.-p+x.| by EUCLID:11
.= |. 1 / |.-p+x.| .|* |.r.|* |.-p+x.| by COMPLEX1:65
.= |.1 / |.-p+x.|.|*r*|.-p+x.| by ABSVALUE:def 1,A2
.= |.1 / |.-p+x.|.|*r*|.|.-p+x.|.| by ABSVALUE:def 1
.= |.1 / |.-p+x.|.|*|.|.-p+x.|.|*r
.= 1*r by ABSVALUE:6, A26,EUCLID:8,A27
.=r;
hence thesis by A28,A25,A19;
end;
[#]TRS = S by PRE_TOPC:def 5;
then reconsider h as Function of TR|A,TR|S by A17,A14,A15,FUNCT_2:2;
A29: dom (h|S) = A/\S by A15,RELAT_1:61;
A31: for x be object st x in dom (h|S) holds (h|S).x = id(A/\S).x
proof
let y be object;
assume
A32: y in dom (h|S);
then reconsider x=y as Point of TR by A29;
A33: x in dom h by A32,RELAT_1:57;
then
A34: h.x = (P*IrNt).x by A13,FUNCT_1:47;
tt.x=t.x by A7,A33,A15,FUNCT_1:47,A8,A16;
then
A35: tt.x = -p+x by RLTOPSP1:def 10;
x-p = -p+x;
then
A36: |.-p+x.| =r by A32,TOPREAL9:9;
A37: x in dom (P*IrNt) by A13,A33,RELAT_1:57;
then x in dom IrNt by FUNCT_1:11;
then
A38: IrNt.x = Ir.x (/) (nN*tt).x by VALUED_2:72;
dom (nN*tt) = cTRp by A7, FUNCT_2:def 1;
then (nN*tt).x = nN.(tt.x) by A7,A33,A15,FUNCT_1:12;
then
A39: (nN*tt).x = |.-p+x.| by A35,JGRAPH_4:def 1;
dom Ir = cTRp by A7,FUNCT_2:def 1;
then Ir.x = r*(-p+x) by A35, A7,A33,A15,VALUED_2:def 39;
then
A40: IrNt.x = (1 / |.-p+x.|)*(r*(-p+x)) by A39,A38,VALUED_2:def 32
.= (1/r *r) *(-p+x) by A36,RLVECT_1:def 7
.= 1*(-p+x) by XCMPLX_1:87,A2
.= -p+x by RLVECT_1:def 8;
thus (h|S).y=h.x by A32,FUNCT_1:47
.=P.(-p+x) by A34, A37,FUNCT_1:12,A40
.= p+(-p+x) by RLTOPSP1:def 10
.= (p+-p)+x by RLVECT_1:def 3
.= 0.TR+x by RLVECT_1:def 10
.= x by RLVECT_1:def 4
.= id(A/\S).y by A32,A29,FUNCT_1:17;
end;
take h;
thus thesis by A31,A15,PRE_TOPC:27,RELAT_1:61;
end;
end;
theorem Th5:
r + |.p-q.| <= s implies Ball(p,r) c= Ball(q,s)
proof
assume
A1: r+|.p-q.| <= s;
let x be object;
assume
A2: x in Ball(p,r);
then reconsider x as Point of TOP-REAL n;
|.x-p.|+|.p-q.| < r+|.p-q.| by A2,TOPREAL9:7,XREAL_1:6;
then
A3: |.x-p.|+|.p-q.| < s by A1,XXREAL_0:2;
A4: x is Element of REAL n by EUCLID:22;
A5:p is Element of REAL n by EUCLID:22;
q is Element of REAL n by EUCLID:22;
then |.x-q.| <= |.x-p.| + |.p-q.| by A4,A5,EUCLID:19;
then |.x-q.| < s by A3,XXREAL_0:2;
hence thesis;
end;
theorem Th6:
A is non boundary implies ind A = n
proof
set TR=TOP-REAL n;
set E=the empty Subset of TR;
consider Ia be affinely-independent Subset of TR such that
E c= Ia & Ia c= [#]TR
and
A1: Affin Ia = Affin [#]TR by RLAFFIN1:60;
A2: the TopStruct of TR=TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider IA=Ia as finite Subset of Euclid n by TOPMETR:12;
IA <> {} by A1;
then consider X be object such that
A3: X in IA by XBOOLE_0:def 1;
reconsider X as Point of Euclid n by A3;
reconsider x=X as Point of TR by A2, TOPMETR:12;
A4: dim TR = n by RLAFFIN3:4;
[#]TR c= Affin [#]TR by RLAFFIN1:49;
then card Ia = (dim TR)+1 by A1,XBOOLE_0:def 10,RLAFFIN3:6;
then
A5: ind conv Ia = n by A4,SIMPLEX2:25;
set d=diameter IA;
A6: ind TR = n by SIMPLEX2:26;
Ia c= conv Ia by RLAFFIN1:2;
then
A7: conv Ia c= cl_Ball(X,d) by A3,SIMPLEX2:13;
assume A is non boundary;
then Int A <> {} by TOPS_1:48;
then consider y be object such that
A8: y in Int A by XBOOLE_0:def 1;
reconsider y as Point of TR by A8;
reconsider Y=y as Point of Euclid n by A2, TOPMETR:12;
consider r be Real such that
A9: r>0
and
A10: Ball(Y,r) c= A by A8,GOBOARD6:5;
set r2=r/2;
A11: n in NAT by ORDINAL1:def 12;
A12: Ball(Y,r)=Ball(y,r) by TOPREAL9:13;
d+0 < d+1 by XREAL_1:6;
then
A13: cl_Ball(x,d) c= Ball(x,d+1) by A11,JORDAN:21;
cl_Ball(X,d)=cl_Ball(x,d) by TOPREAL9:14;
then conv Ia c= Ball(x,d+1) by A13,A7;
then
A14: n <= ind Ball(x,d+1) by A5,TOPDIM_1:19;
d>=0 by TBSP_1:21;
then
A15: cl_Ball(x,d+1) is compact non boundary by Lm2;
cl_Ball(y,r2) c= Ball(y,r) by A9,XREAL_1:216,A11,JORDAN:21;
then cl_Ball(y,r2) c= A by A10,A12;
then
A16:ind cl_Ball(y,r2) <= ind A by TOPDIM_1:19;
cl_Ball(y,r2) is compact non boundary by A9, Lm2;
then ex h be Function of TR |cl_Ball(x,d+1),TR |cl_Ball(y,r2) st
h is being_homeomorphism & h.:Fr cl_Ball(x,d+1) = Fr cl_Ball(y,r2)
by A15,BROUWER2:7;
then cl_Ball(x,d+1),cl_Ball(y,r2) are_homeomorphic
by T_0TOPSP:def 1,METRIZTS:def 1;
then
A17:ind cl_Ball(x,d+1)=ind cl_Ball(y,r2) by TOPDIM_1:27;
Ball(x,d+1) c= cl_Ball(x,d+1) by TOPREAL9:16;
then ind Ball(x,d+1) <= ind cl_Ball(x,d+1) by TOPDIM_1:19;
then n <= ind cl_Ball(y,r2) by A17,A14, XXREAL_0:2;
then
A18: n<= ind A by A16,XXREAL_0:2;
ind A <= ind TR by TOPDIM_1:20;
hence thesis by A6,XXREAL_0:1,A18;
end;
::$N The Small Inductive Dimension of the Sphere
theorem Th7:
r>0 implies ind Sphere(p,r) = n-1
proof
set TR=TOP-REAL n;
A1: ind A <= i & ind B <=i & A is closed implies ind (A\/B)<=i
proof
set TT=the TopStruct of TR;
assume that
A2: ind A <= i
and
A3: ind B <=i
and
A4: A is closed;
reconsider a=A, b=B, AB=A\/B as Subset of TT;
A5: a is closed by A4,PRE_TOPC:31;
A6: TT|AB is second-countable;
A7: TT = TopSpaceMetr Euclid n by EUCLID:def 8;
A8: TT = TR| [#]TR by TSEP_1:93;
then
A9: ind b<=i by TOPDIM_1:22,A3;
ind a<= i by A8,TOPDIM_1:22,A2;
then ind AB <= i by A9,A5,A8, A7,A6,TOPDIM_2:5;
hence thesis by TOPDIM_1:22,A8;
end;
assume
A10: r>0;
per cases by NAT_1:25;
suppose
A11: n=0;
then
A12: p=0.TR by EUCLID:77;
Sphere(p,r)={}
proof
assume Sphere(p,r) <>{};
then consider x be object such that
A13: x in Sphere(p,r) by XBOOLE_0:def 1;
reconsider x as Point of TR by A13;
x = 0.TR by A11,EUCLID:77
.= 0*n by EUCLID:66;
then |.x.| = 0 by EUCLID:7;
hence contradiction by A12,A13,TOPREAL9:12,A10;
end;
hence thesis by TOPDIM_1:6,A11;
end;
suppose
A15: n=1;
then consider u be Real such that
A16: p=<*u*> by JORDAN2B:20;
set u1=|[u-r]|,u2=|[u+r]|;
card {u2}=1 by CARD_1:30;
then
A17: ind {u2} = 0 by TOPDIM_1:8, NAT_1:14;
card {u1}=1 by CARD_1:30;
then ind {u1}=0 by TOPDIM_1:8, NAT_1:14;
then
A18: ind ({u1}\/{u2}) = 0 by A17,A15,A1;
{<*u qua ExtReal-r*>,<*u qua ExtReal+r*>} = Fr Ball(p,r)
by A15,TOPDIM_2:18,A16,A10
.= Sphere(p,r) by A15,A10,JORDAN:24;
hence thesis by A18,ENUMSET1:1,A15;
end;
suppose
A19: n>1;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
reconsider n1 as non zero Element of NAT by A19;
set n2=n1+1;
set Tn1=TOP-REAL n1,Tn2=TOP-REAL n2,S=Sphere(0.Tn2,1);
set Sp = {s where s is Point of Tn2: s.n2>=0 & |.s.|=1},
Sn = {t where t is Point of Tn2: t.n2<=0 & |.t.|=1};
A20: Sp c= S
proof
let x be object;
assume x in Sp;
then consider s be Point of Tn2 such that
A21: x=s
and
s.n2>=0
and
A22: |.s.|=1;
s-0.Tn2 = s by RLVECT_1:13;
hence thesis by A22,A21;
end;
A23: [#](TR |cl_Ball(p,r)) = cl_Ball(p,r) by PRE_TOPC:def 5;
reconsider Spr=Sphere(p,r) as Subset of TR |cl_Ball(p,r)
by A23,TOPREAL9:17;
A24: cl_Ball(0.Tn2,1) is compact non boundary by Lm2;
cl_Ball(p,r) is compact non boundary by Lm2, A10;
then consider h be Function of TR | cl_Ball(p,r), Tn2 |cl_Ball(0.Tn2,1)
such that
A25: h is being_homeomorphism
and
A26: h.:Fr cl_Ball(p,r) = Fr cl_Ball(0.Tn2,1) by A24,BROUWER2:7;
A27: ind Spr = ind (h.:Spr) by A25,METRIZTS:3,TOPDIM_1:27;
A28: Sn c= S
proof
let x be object;
assume x in Sn;
then consider s be Point of Tn2 such that
A29: x=s
and
s.n2<=0
and
A30: |.s.|=1;
s-0.Tn2 = s by RLVECT_1:13;
hence thesis by A30,A29;
end;
then reconsider Sp,Sn as Subset of TOP-REAL n2 by A20,XBOOLE_1:1;
A31: S c= Sp\/Sn
proof
let x be object;
assume
A32: x in S;
then reconsider x as Point of Tn2;
A33: x.n2 >=0 or x.n2<=0;
|.x.|=1 by A32,TOPREAL9:12;
then x in Sp or x in Sn by A33;
hence thesis by XBOOLE_0:def 3;
end;
A34: Sn= {t where t is Point of TOP-REAL n2: t.n2<=0 & |.t.|=1};
then
A35: Sp is closed by Th2;
A36: Sp = {s where s is Point of TOP-REAL n2: s.n2>=0 & |.s.|=1};
A37: Sp,cl_Ball(0.Tn1,1) are_homeomorphic &
Sn,cl_Ball(0.Tn1,1) are_homeomorphic
proof
set TD=Tdisk(0.Tn1,1);
deffunc ff(Nat)=PROJ(n2,$1);
consider FF be FinSequence such that
A38: len FF = n1 & for k be Nat st k in dom FF holds FF.k=ff(k)
from FINSEQ_1:sch 2;
rng FF c= Funcs(the carrier of Tn2,the carrier of R^1)
proof
let x be object;
assume x in rng FF;
then consider i be object such that
A39: i in dom FF
and
A40: FF.i = x by FUNCT_1:def 3;
reconsider i as Nat by A39;
ff(i) in Funcs(the carrier of Tn2,the carrier of R^1) by FUNCT_2:8;
hence thesis by A38,A39,A40;
end;
then reconsider FF as FinSequence of
Funcs(the carrier of Tn2,the carrier of R^1) by FINSEQ_1:def 4;
reconsider FF as Element of n1-tuples_on
Funcs(the carrier of Tn2,the carrier of R^1) by A38,FINSEQ_2:92;
set FFF=<:FF:>;
A41: [#]TD = cl_Ball(0.Tn1,1) by PRE_TOPC:def 5;
FFF.:Sp= cl_Ball(0.Tn1,1) by A38,Th1,A34;
then
A42: rng (FFF|Sp) c= the carrier of TD by RELAT_1:115,A41;
A43: dom FFF=the carrier of Tn2 by FUNCT_2:def 1;
then Sn/\dom FFF=Sn by XBOOLE_1:28;
then
A44: dom (FFF|Sn)= Sn by RELAT_1:61;
Sp/\dom FFF=Sp by A43,XBOOLE_1:28;
then
A45: dom (FFF|Sp)= Sp by RELAT_1:61;
[#](Tn2|Sp) = Sp by PRE_TOPC:def 5;
then
reconsider Fsp=FFF|Sp as Function of Tn2|Sp,TD by A42,A45,FUNCT_2:2;
A46: [#] (Tn2|Sn) = Sn by PRE_TOPC:def 5;
FFF.:Sn= cl_Ball(0.Tn1,1) by A38,Th1,A36;
then rng (FFF|Sn) c= the carrier of TD by RELAT_1:115, A41;
then reconsider Fsn=FFF|Sn as Function of Tn2|Sn,TD by A46,FUNCT_2:2,A44;
A47: Fsn is being_homeomorphism by A38,Th1,A36;
Fsp is being_homeomorphism by A38,Th1,A34;
hence thesis by A47,T_0TOPSP:def 1,METRIZTS:def 1;
end;
A48: ind cl_Ball(0.Tn1,1) = n1 by Lm2,Th6;
then
A49: ind Sp=n1 by A37,TOPDIM_1:27;
Sp c= Sp\/Sn by XBOOLE_1:7;
then
A50: n1 <= ind (Sp\/Sn) by A49, TOPDIM_1:19;
ind Sn=n1 by A37,A48,TOPDIM_1:27;
then ind (Sp\/Sn) <= n1 by A35,A49,A1;
then
A51: ind (Sp\/Sn) = n1 by A50,XXREAL_0:1;
Fr cl_Ball(p,r) = Sphere(p,r) by BROUWER2:5,A10;
then h.:Spr = S by A26, BROUWER2:5;
then
A52: ind (h.:Spr) = ind S by TOPDIM_1:21;
Sp\/Sn c= S by A20,A28,XBOOLE_1:8;
then ind S= n1 by A31,XBOOLE_0:def 10,A51;
hence thesis by TOPDIM_1:21,A52,A27;
end;
end;
begin :: A Characterization of Open Sets in Euclidean Space
:: in Terms of Continuous Transformations
theorem Th8:
for p st n>0 & p in A & for r st r>0
ex U be open Subset of (TOP-REAL n) |A st
p in U & U c= Ball(p,r) &
for f be Function of (TOP-REAL n) | (A\U),Tunit_circle(n) st
f is continuous
ex h be Function of (TOP-REAL n) |A,Tunit_circle(n) st
h is continuous & h| (A\U) = f
holds p in Fr A
proof
let p;
set TRn=TOP-REAL n,cTRn=the carrier of TRn;
set CL=cl_Ball(0.TRn,1),S=Sphere(0.TRn,1);
set TS=Tunit_circle(n);
assume
A1: n > 0;
cTRn\{0.TRn}={0.TRn}` by SUBSET_1:def 4;
then reconsider cTR0=cTRn\{0.TRn} as non empty open Subset of TRn by A1;
set nN=n NormF;
set TRn0=TRn|cTR0;
A2: Int A c= A by TOPS_1:16;
set G= transl(p,TRn);
reconsider I=incl TRn0 as continuous Function of TRn0,TRn by TMAP_1:87;
A3: [#]TRn0=cTR0 by PRE_TOPC:def 5;
A4: nN|TRn0=nN|the carrier of TRn0 by TMAP_1:def 4;
not 0 in rng(nN|TRn0)
proof
assume 0 in rng(nN|TRn0);
then consider x be object such that
A5: x in dom(nN|TRn0)
and
A6: (nN|TRn0).x=0 by FUNCT_1:def 3;
x in dom nN by A4,A5,RELAT_1:57;
then reconsider x as Element of TRn;
reconsider X=x as Element of REAL n by EUCLID:22;
0 = nN.x by A4,A5,A6,FUNCT_1:47
.= |.X.| by JGRAPH_4:def 1;
then x=0*n by EUCLID:8;
then x=0.TRn by EUCLID:70;
then x in {0.TRn} by TARSKI:def 1;
hence contradiction by A3,A5,XBOOLE_0:def 5;
end;
then reconsider nN0=nN|TRn0 as non-empty continuous Function of TRn0,R^1
by RELAT_1:def 9;
reconsider b=I</>nN0 as Function of TRn0,TRn by TOPREALC:46;
A7: Int A in the topology of TRn by PRE_TOPC:def 2;
set En=Euclid n,TM=TopSpaceMetr En;
assume that
A8: p in A
and
A9: for r st r>0 ex U be open Subset of TRn|A st p in U & U c= Ball(p,r)
& for f be Function of (TRn) | (A\U),Tunit_circle(n) st f is continuous
ex h be Function of TRn |A,Tunit_circle(n) st
h is continuous & h| (A\U) = f;
reconsider e=p as Point of En by EUCLID:67;
A10:the TopStruct of TRn = TM by EUCLID:def 8;
then reconsider IA=Int A as Subset of TM;
TS = Tcircle(0.TRn,1) by TOPREALB:def 7;
then TS=TRn|S by TOPREALB:def 6;
then
A11: [#]TS=S by PRE_TOPC:def 5;
assume
not p in Fr A;
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 be open Subset of TRn|A such that
A14: p in U
and
A15: U c= Ball(p,r2)
and
A16: for f be Function of (TRn) | (A\U),TS st f is continuous
ex h be Function of TRn |A,TS st h is continuous & h| (A\U) = f
by A12, A9;
reconsider Sph=Sphere(p,r2) as non empty Subset of TRn by A1, A12;
consider au be 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,r2) c= Ball(p,r) by JORDAN:21,A18, A12,XREAL_1:216;
A21: Sph = cl_Ball(p,r2) \ Ball(p,r2) by JORDAN:19,A18;
then W: au in cl_Ball(p,r2) by A17,XBOOLE_0:def 5;
A22: au in IA by W,A20,A19,A13;
reconsider r2 as non zero Real by A12;
reconsider CL2=cl_Ball(p,r2) as non empty Subset of TRn by A12;
A23: Sph c= CL2 by A21,XBOOLE_1:36;
[#](TRn|CL2)= CL2 by PRE_TOPC:def 5;
then reconsider sph=Sph as non empty Subset of TRn|CL2 by A21,XBOOLE_1:36;
A24:(TRn|CL2) |sph = TRn|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 TRn by A22,A2,XBOOLE_0:def 5;
set TAU=TRn | AU;
set t= transl(-p,TRn),T= t| TAU;
A25: [#]TAU = A\U by PRE_TOPC:def 5;
then
A26: dom T = A\U by FUNCT_2:def 1;
A27: T=t|the carrier of TAU by TMAP_1:def 4;
A28:rng T c= cTR0
proof
let y be object;
assume y in rng T;
then consider x be object such that
A29: x in dom T
and
A30: T.x=y by FUNCT_1:def 3;
reconsider x as Point of TRn by A29,A26;
A31: T.x=t.x by A29,A27,FUNCT_1:47;
A32: t.x= x+-p by RLTOPSP1:def 10;
assume not y in cTR0;
then T.x in {0.TRn} by A31,XBOOLE_0:def 5,A30;
then x-p = 0.TRn by TARSKI:def 1,A32,A31;
then x= p by RLVECT_1:21;
hence thesis by A29, A25,XBOOLE_0:def 5, A14;
end;
then reconsider T0=T as continuous Function of TAU, TRn0
by A26,FUNCT_2:2,A3,A25,PRE_TOPC:27;
A33: [#](TRn|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 be Point of TRn st p in cTR0 holds
b.p=1/|.p.|*p & |.(1/|.p.|)*p.|=1
proof
let p be Point of TRn;
A38: |. 1/|.p.| .|=1/|.p.| by ABSVALUE:def 1;
assume
A39: p in cTR0;
then
A40: I.p=p by A3,TMAP_1:84;
A41:nN0.p=nN.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;
A42:p<>0.TRn 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;
end;
rng b c=S
proof
let y be object;
assume y in rng b;
then consider x be object such that
A43: x in dom b
and
A44: b.x=y by FUNCT_1:def 3;
reconsider x as Point of TRn by A36,A43;
A45: |.(1/|.x.|)*x.|=1 by A3,A37,A43;
A46: (1/|.x.|)*x-0.TRn=(1/|.x.|)*x by RLVECT_1:13;
y = 1/|.x.|*x by A3,A37,A43,A44;
hence thesis by A46,A45;
end;
then reconsider B=b as Function of TRn0,TS by A3,A11,A36,FUNCT_2:2;
A47:[#](TRn|CL2|sph )=sph by PRE_TOPC:def 5;
set m = mlt(r2,TRn), M= m|TS;
reconsider M= m|TS as continuous Function of TS,TRn by A1;
A48:M=m|the carrier of TS by TMAP_1:def 4;
A49: [#](TRn|A) = A by PRE_TOPC:def 5;
then reconsider clB= CL2 as Subset of TRn|A by A34,A2,XBOOLE_1:1;
A50:(TRn|A) |clB = TRn|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 be Function of TRn |A,TS such that
A51: h is continuous
and
A52: h| (A\U) = B*T0 by A16;
M*h is continuous Function of TRn|A,TRn by A1,A51,TOPS_2:46;
then reconsider GHM=G*(M*h) as continuous Function of TRn|A,TRn
by TOPS_2:46;
A53:dom h = the carrier of (TRn|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;
assume y in rng GHM;
then consider q be object such that
A56: q in dom GHM
and
A57: GHM.q=y by FUNCT_1:def 3;
A58:y = G.((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 as Point of TRn by A59;
h.q in S by A63,A11;
then reconsider hq=h.q as Point of TRn;
A64:m.(h.q) = r2 * hq by RLTOPSP1:def 13;
M.(h.q)=m.(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.TRn) 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 thesis by A66,A65,A54;
end;
dom GHM = A by A49,FUNCT_2:def 1;
then reconsider ghm=GHM as Function of TRn|A,TRn|Sph
by A55,A49,A33,FUNCT_2:2;
ghm is continuous by PRE_TOPC:27;
then reconsider ghM=ghm| ((TRn|A) |clB ) as continuous
Function of TRn|CL2,(TRn|CL2) |sph by A8,A50,A24;
A68:dom ghM = the carrier of (TRn|CL2) by FUNCT_2:def 1;
A69:ghM =ghm|the carrier of ((TRn|A) |clB ) by TMAP_1:def 4, A8;
for w be Point of TRn|CL2 st w in Sph holds ghM.w=w
proof
let w be Point of TRn|CL2;
assume
A70: w in Sph;
then reconsider q=w as Point of TRn;
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)=m.(h.q) by A48,FUNCT_1:47;
t.q = q+-p by RLTOPSP1:def 10;
then
A80: T.q=q-p by A26,A27,A75,FUNCT_1:47;
q in dom T0 by A76,FUNCT_1:11;
then
A81: T.q in rng T by FUNCT_1:def 3;
h.q in S by A78,A11;
then reconsider hq=h.q as Point of TRn;
ghM.q=ghm.q by A68,A69, FUNCT_1:47;
then
A82: ghM.q = G.((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;
m.(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.TRn by RLVECT_1:def 10
.= q by RLVECT_1:4;
hence thesis;
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: CL2 is non boundary by A12;
Fr CL2 = Sph by A12,BROUWER2:5;
hence
contradiction by A84,A85,A47,BROUWER2:9,BORSUK_1:def 17;
end;
theorem Th9:
for p st p in Fr A & A is closed
for r st r>0
ex U be open Subset of (TOP-REAL n) |A st
p in U & U c= Ball(p,r) &
for f be Function of (TOP-REAL n) | (A\U),Tunit_circle(n) st
f is continuous
ex h be Function of (TOP-REAL n) |A,Tunit_circle(n) st
h is continuous & h| (A\U) = f
proof
set TR=TOP-REAL n;
let p;
assume that
A1: p in Fr A
and
A2: A is closed;
A3:Fr A c= A by TOPS_1:35, A2;
n>0
proof
assume n<=0;
then n=0;
then
A4: the carrier of TR = {0.TR} by EUCLID:77,22;
[#]TR is open;
hence thesis by A4, A1,ZFMISC_1:33;
end;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
set TU=Tunit_circle(n);
A5: p is Element of REAL n by EUCLID:22;
let r;
assume
A6: r>0;
set r3=r/3,r2=2*r3;
set B=Ball(p,r3);
p is Element of REAL n by EUCLID:22;
then |. p-p .|=0;
then p in B by A6;
then A` meets B by A1,TOPS_1:28;
then consider x be object such that
A7: x in A`
and
A8: x in B by XBOOLE_0:3;
reconsider x as Element of TR by A7;
set u=Ball(x,r2), clU=cl_Ball(x,r2);
A9:n in NAT by ORDINAL1:def 12;
A10:u c= clU by TOPREAL9:16;
A11:[#](TR|A)=A by PRE_TOPC:def 5;
then reconsider U=u/\A as Subset of TR|A by XBOOLE_1:17;
u in the topology of TR by PRE_TOPC:def 2;
then U in the topology of TR|A by PRE_TOPC:def 4,A11;
then reconsider U as open Subset of TR|A by PRE_TOPC:def 2;
take U;
x is Element of REAL n by EUCLID:22;
then
A12: |.x-p.| =|.p-x.| by EUCLID:18, A5;
|.x-p.|+r2 < r3+r2 by A8,TOPREAL9:7,XREAL_1:6;
then
A13: u c= Ball(p,r) by Th5;
r2 > r3 by A6,XREAL_1:155;
then |.x-p.| < r2 by A8,TOPREAL9:7,XXREAL_0:2;
then
A14: p in u by A12;
hence p in U by A3, A1,XBOOLE_0:def 4;
U c= u by XBOOLE_1:17;
hence U c= Ball(p,r) by A13;
let f be Function of TR | (A\U),TU such that
A15: f is continuous;
per cases;
suppose
A16: A\U is empty;
set h = the continuous Function of TR |A,Tunit_circle(n1+1);
reconsider H=h as Function of (TOP-REAL n) |A,TU;
take H;
f={} by A16;
hence thesis by A16;
end;
suppose
A17: A\U is non empty;
set S = Sphere(x,r2);
reconsider AUS=(A\U)\/S as non empty Subset of TR by A17;
A18: TR|AUS is metrizable & TR|AUS is finite-ind second-countable
proof
reconsider aus=AUS as Subset of the TopStruct of TR;
A19: the TopStruct of TR = TopSpaceMetr Euclid n by EUCLID:def 8;
TR|AUS = (the TopStruct of TR) |aus by PRE_TOPC:36;
hence thesis by A19;
end;
A20: [#] (TR|AUS) = AUS by PRE_TOPC:def 5;
then reconsider AU=A\U,SS=S as Subset of TR|AUS by XBOOLE_1:7;
AU` = (AUS)\AU by SUBSET_1:def 4,A20
.= S\AU by XBOOLE_1:40;
then
A21: AU` c= SS by XBOOLE_1:36;
ind S = n1 by A6,Th7;
then ind SS =n1 by TOPDIM_1:21;
then
A22: ind (AU`) <= n1 by TOPDIM_1:19,A21;
A23: TR| (A\U) = TR|AUS| (AU) by A20,PRE_TOPC:7;
then reconsider F=f as Function of TR |AUS| AU,TU;
A\U = A\u by XBOOLE_1:47;
then
A24: A\U is closed by A2,YELLOW_8:20;
then AU is closed by TSEP_1:8;
then consider g be continuous Function of TR |AUS, Tunit_circle(n1+1)
such that
A25: g|AU=F by Th3, A23,A15, A18,A22;
A26: [#](TR|A) = A by PRE_TOPC:def 5;
then reconsider AclU=A/\clU, au=A\U as Subset of TR|A by XBOOLE_1:17,36;
set T3=TR |A | AclU, T4=TR |A | au;
A27: (A/\U) \/ au = A by XBOOLE_1:51;
A`= ([#]TR)\A by SUBSET_1:def 4;
then not x in A by A7,XBOOLE_0:def 5;
then consider h be Function of TR |A,TR |S such that
A28: h is continuous
and
A29: h|S = id (A/\S) by A6,Th4;
A30: n1+1 = n;
then
A31: dom h = the carrier of (TR|A) by A6,FUNCT_2:def 1;
A32: [#](TR|S)=S by PRE_TOPC:def 5;
then rng h c= the carrier of TR by XBOOLE_1:1;
then reconsider h1=h as Function of TR|A,TR by A31,FUNCT_2:2;
A33: S c= AUS by XBOOLE_1:7;
rng h c= [#](TR|S);
then reconsider h2=h1 as Function of TR|A,TR|AUS
by A33,A32,XBOOLE_1:1,A31,FUNCT_2:2,A20;
h1 is continuous by A28,PRE_TOPC:26;
then
A34: h2 is continuous by PRE_TOPC:27;
set T2=TR |AUS|AU;
A35: TR |AUS | AU = TR| (A\U) by PRE_TOPC:7, XBOOLE_1:7;
A36: clU\u = S by JORDAN:19,A9;
A37: (A/\A)/\u = A/\(A/\u) by XBOOLE_1: 16;
A38: g|T2 = g|the carrier of T2 by TMAP_1:def 4;
TR |A | au = TR| (A\U) by XBOOLE_1:36,PRE_TOPC:7;
then reconsider gT2=g|T2 as continuous Function of T4,Tunit_circle(n1+1)
by A35,A17;
A39: [#]T3 =AclU by PRE_TOPC:def 5;
AclU is non empty by A10,A14, A3, A1,XBOOLE_0:def 4;
then reconsider gh2T3=g*(h2|T3) as continuous
Function of T3,Tunit_circle(n1+1) by A34;
A40: [#]T4 = au by PRE_TOPC:def 5;
A41: h2|T3 = h2|the carrier of T3 by A3, A1, TMAP_1:def 4;
A42: now
let x be object such that
A43: x in dom gh2T3 /\ dom gT2;
A44: not x in U by A43,A40,XBOOLE_0:def 5;
x in A by A43,A40,XBOOLE_0:def 5;
then
A45: not x in u by A44,XBOOLE_0:def 4;
A46: x in dom gh2T3 by A43,XBOOLE_0:def 4;
then x in clU by A39,XBOOLE_0:def 4;
then
A47: x in S by A45,A36,XBOOLE_0:def 5;
A48: x in dom gT2 by A43,XBOOLE_0:def 4;
x in A by A46,A39,XBOOLE_0:def 4;
then
A49: x in A/\S by A47,XBOOLE_0:def 4;
x in dom (h2|T3) by A46,FUNCT_1:11;
then (h2|T3).x = h2.x by A41,FUNCT_1:47
.= (h|S).x by A47,FUNCT_1:49
.= x by A29,A49,FUNCT_1:17;
hence gh2T3.x = g.x by A46,FUNCT_1:12
.= gT2.x by A38,A48,FUNCT_1:47;
end;
A50: AclU is closed by A2,TSEP_1:8;
au is closed by A24,TSEP_1:8;
then reconsider G=gh2T3+* gT2 as continuous
Function of TR|A| ( AclU\/au),Tunit_circle(n1+1)
by A50,A42,PARTFUN1:def 4,TOPGEN_5:10;
W: A/\u c= AclU by TOPREAL9:16,XBOOLE_1:26;
A = AclU\/au by A26,W,A27,A37,XBOOLE_1:9;
then
A51: TR|A| (AclU\/au) = TR|A by A26,TSEP_1:93;
then reconsider GG=G as Function of TR|A, TU;
take GG;
thus GG is continuous by A51;
A52: [#](TR| (A\U)) = A\U by PRE_TOPC:def 5;
A53: dom gT2 =the carrier of T4 by FUNCT_2:def 1;
A54: now let x;
assume
A55: x in dom f;
hence (GG| (A\U)).x = GG.x by A52,FUNCT_1:49
.= gT2.x by FUNCT_4:13, A55,A52,A40,A53
.= g.x by A38,A40,A52,A53,A55,FUNCT_1:47
.= f.x by A25, A55,A52,FUNCT_1:49;
end;
dom GG = A by A26,FUNCT_2:def 1;
then
A56: dom (GG| (A\U)) = A /\ ( A\U) by RELAT_1:61
.= A\U by XBOOLE_1:36,XBOOLE_1:28;
dom f = A\U by A30,A52,FUNCT_2:def 1;
hence thesis by A54,A56;
end;
end;
Lm3: for A,B be Subset of TOP-REAL n st n = 0
for h be Function of (TOP-REAL n) |A,(TOP-REAL n) |B st
h is being_homeomorphism
for p be Point of TOP-REAL n
holds (p in Fr A implies h.p in Fr B) &
(p in Int A implies h.p in Int B)
proof
set TR=TOP-REAL n;
A1: Int ([#]TR)=[#]TR by TOPS_1:15;
let A,B be Subset of TR such that
A2: n = 0;
A3:the carrier of TR = {0.TR} by A2,EUCLID:77,22;
let h be Function of TR |A,TR |B such that
A4:h is being_homeomorphism;
A5: dom h = [#](TR|A) by A4, TOPS_2:def 5;
let p be Point of TR;
[#]TR is open;
hence p in Fr A implies h.p in Fr B by A3,ZFMISC_1:33;
A6: A = [#](TR|A) by PRE_TOPC:def 5;
A7: Int A c= A by TOPS_1:16;
assume p in Int A;
then
A8: h.p in rng h by A7,A5,A6,FUNCT_1:def 3;
A9: B=[#](TR|B) by PRE_TOPC:def 5;
then B=[#]TR by A8,ZFMISC_1:33,A3;
hence thesis by A8,A1,A9;
end;
begin :: Brouwer Invariance of Domain Theorem - Special case
theorem Th10:
A is closed & p in Fr A implies
for h be Function of (TOP-REAL n) |A,(TOP-REAL n) |B st
h is being_homeomorphism
holds h.p in Fr B
proof
set TRn=TOP-REAL n;
assume that
A1: A is closed
and
A2: p in Fr A;
A3:Fr A c= A by A1, TOPS_1:35;
let h be Function of TRn|A,TRn|B such that
A4: h is being_homeomorphism;
A5: [#](TRn|A) = A by PRE_TOPC:def 5;
then
A6: dom h = A by A4,TOPS_2:def 5;
then
A7: h.p in rng h by A3,A2,FUNCT_1:def 3;
A8: [#](TRn|B) = B by PRE_TOPC:def 5;
then
A9: rng h = B by A4,TOPS_2:def 5;
then reconsider hp=h.p as Point of TRn by A7;
per cases;
suppose n=0;
hence thesis by Lm3,A4, A2;
end;
suppose
A10: n>0;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
A11: the TopStruct of TRn=TopSpaceMetr Euclid n by EUCLID:def 8;
for r st r>0 ex U be open Subset of TRn|B st
hp in U & U c= Ball(hp,r) &
for f be Function of TRn | (B\U),Tunit_circle(n) st
f is continuous ex h be Function of TRn |B,Tunit_circle(n) st
h is continuous & h| (B\U) = f
proof
reconsider P =p as Point of Euclid n by A11, TOPMETR:12;
let r such that
A13: r>0;
reconsider BB=B/\Ball(hp,r) as Subset of TRn|B by A8,XBOOLE_1:17;
Ball(hp,r) in the topology of TRn by PRE_TOPC:def 2;
then BB in the topology of (TRn|B) by A8,PRE_TOPC:def 4;
then reconsider BB as open Subset of TRn|B by PRE_TOPC:def 2;
h"BB is open by A7,A4,A8, TOPS_2:43;
then h"BB in the topology of TRn|A by PRE_TOPC:def 2;
then consider U be Subset of TRn such that
A14: U in the topology of TRn
and
A15: h"BB = U/\[#](TRn|A) by PRE_TOPC:def 4;
reconsider U as open Subset of TRn by A14,PRE_TOPC:def 2;
A16: Int U = U by TOPS_1:23;
hp is Element of REAL n by EUCLID:22;
then |. hp-hp .|=0;
then hp in Ball(hp,r) by A13;
then hp in BB by A7,A8,XBOOLE_0:def 4;
then p in h"BB by A3,A2, A6,FUNCT_1:def 7;
then p in U by A15,XBOOLE_0:def 4;
then consider s be Real such that
A17: s>0
and
A18: Ball(P,s) c= U by A16,GOBOARD6:5;
consider W be open Subset of TRn|A such that
A19: p in W
and
A20: W c= Ball(p,s)
and
A21: for f be Function of TRn | (A\W),Tunit_circle(n) st
f is continuous ex h be Function of
(TOP-REAL n) |A,Tunit_circle(n)
st h is continuous & h| (A\W) = f by A1,A17,Th9, A2;
Ball(p,s)=Ball(P,s) by TOPREAL9:13;
then
A22: Ball(p,s)/\A c= U/\A by A18, XBOOLE_1: 27;
W/\A=W by A5,XBOOLE_1:28;
then W c= Ball(p,s)/\A by A20, XBOOLE_1: 27;
then W c= U/\A by A22;
then h.:W c= h.:(U/\A) by RELAT_1:123;
then
A23: h.:W c= BB by FUNCT_1:77,A8,A9,A15,A5;
TRn|B is non empty by A3,A2, A6;
then
reconsider hW=h.:W as open Subset of TRn|B by A3,A2,A4,TOPGRP_1:25;
take hW;
BB c= Ball(hp,r) by XBOOLE_1:17;
hence hp in hW & hW c= Ball(hp,r)
by A3,A2,A6,FUNCT_1:def 6,A19,A23;
set AW=A\W,haw=h| AW,T=Tunit_circle(n);
A24: [#](TRn | (B\hW))=B\hW by PRE_TOPC:def 5;
reconsider aw=AW as Subset of TRn|A by XBOOLE_1:36,A5;
let f be Function of TRn | (B\hW),T such that
A25: f is continuous;
per cases;
suppose
A26: B\hW is empty;
set h = the continuous Function of TRn |B,Tunit_circle(n1+1);
reconsider H=h as Function of (TOP-REAL n) |B,T;
take H;
f={} by A26;
hence thesis by A26;
end;
suppose
A27: B\hW is non empty;
set AW=A\W,haw=h| AW,T=Tunit_circle(n);
reconsider haw as Function of (TRn |A) | aw,(TRn|B) | (h.:AW)
by A3,A2,A7,JORDAN24:12;
A28: h.:AW = (h.:A) \ (h.:W) by A4, FUNCT_1:64
.= B\hW by RELAT_1:113,A6,A9;
then
A29: (TRn|B) | (h.:AW) = TRn | (B\hW) by XBOOLE_1:36,PRE_TOPC:7;
A30: (TRn |A) | aw = TRn |AW by PRE_TOPC:7, XBOOLE_1:36;
then reconsider HAW =haw as Function of TRn |AW,TRn | (B\hW)
by A29;
reconsider fhW=f*HAW as Function of TRn | AW,Tunit_circle(n)
by A27;
fhW is continuous
by A27,JORDAN24:13,A4,A3,A2,A7,A29,A30,A25,TOPS_2:46;
then consider HW be Function of TRn |A,T such that
A31: HW is continuous
and
A32: HW| AW = fhW by A21;
reconsider HWh=HW*(h") as Function of TRn|B,T by A3,A2;
take HWh;
h" is continuous by A4,TOPS_2:def 5;
hence HWh is continuous by TOPS_2:46, A3,A2,A31;
A33: dom f = B\hW by A10,A24, FUNCT_2:def 1;
A34: rng ((h") | (B \ hW)) = (h").:(B\hW) by RELAT_1:115
.= h"(h.:AW ) by A28,A8,A9,A4,TOPS_2:55
.= AW by FUNCT_1:94,A6,A4,XBOOLE_1:36;
thus HWh | (B \ hW) = HW* ((h") | (B \ hW)) by RELAT_1:83
.= HW * ((id (AW))*((h") | (B \ hW))) by A34, RELAT_1:53
.= (HW * (id (AW)))*((h") | (B \ hW)) by RELAT_1:36
.= (HW |AW)*((h") | (B \ hW)) by RELAT_1:65
.=( (f*h) |AW ) * ((h") | (B \ hW)) by A32,RELAT_1:83
.=( (f*h) *(id AW )) * ((h") | (B \ hW)) by RELAT_1:65
.= (f*h) *((id AW ) * ((h") | (B \ hW))) by RELAT_1:36
.= (f*h) *( (h") | (B \ hW)) by A34,RELAT_1:53
.= ((f*h) * (h")) | (B \ hW) by RELAT_1:83
.= (f*(h * h")) | (B \ hW) by RELAT_1:36
.= (f*id B) | (B \ hW) by TOPS_2:52,A9, A4, A8
.= f | (dom f) by A33, XBOOLE_1:36,RELAT_1:51
.=f;
end;
end;
hence thesis by Th8, A7,A8, A10;
end;
end;
theorem Th11:
B is closed & p in Int A implies
for h be Function of (TOP-REAL n) |A,(TOP-REAL n) |B st
h is being_homeomorphism holds h.p in Int B
proof
set TRn=TOP-REAL n,T=Tunit_circle(n);
assume that
A1: B is closed
and
A2: p in Int A;
A3: Int A c= A by TOPS_1:16;
A4: the TopStruct of TRn=TopSpaceMetr Euclid n by EUCLID:def 8;
let h be Function of TRn|A,TRn|B such that
A5: h is being_homeomorphism;
A6: h" is continuous by A5,TOPS_2:def 5;
A7: [#](TRn|A) = A by PRE_TOPC:def 5;
then A8: dom h = A by A5,TOPS_2:def 5;
A9: [#](TRn|B) = B by PRE_TOPC:def 5;
then A10: rng h = B by A5,TOPS_2:def 5;
per cases;
suppose n=0;
hence thesis by Lm3,A2,A5;
end;
suppose
A11: n>0;
A12: h.p in rng h by A2,A3,A8,FUNCT_1:def 3;
then reconsider hp=h.p as Point of TRn by A10;
ex r st r>0 & for U be open Subset of TRn |B st
hp in U & U c= Ball(hp,r) ex f be Function of TRn | (B\U),T st
f is continuous & for h be Function of TRn |B,T
st h is continuous holds h| (B\U) <> f
proof
reconsider hP =hp as Point of Euclid n by A4, TOPMETR:12;
not p in Fr A by A2, TOPS_1:39,XBOOLE_0:3;
then consider r such that
A14: r>0
and
A15: for U be open Subset of TRn |A st p in U & U c= Ball(p,r)
ex f be Function of TRn | (A\U),T st f is continuous &
for h be Function of TRn |A,T st h is continuous holds
h| (A\U) <> f by A11, A2,A3,Th8;
reconsider BA=Ball(p,r) /\A as Subset of TRn|A by A7,XBOOLE_1: 17;
Ball(p,r) in the topology of TRn by PRE_TOPC:def 2;
then BA in the topology of (TRn|A) by A7,PRE_TOPC:def 4;
then reconsider BA as open Subset of TRn|A by PRE_TOPC:def 2;
h.:BA is open by A5,A2,A3,A12, TOPGRP_1:25;
then h.:BA in the topology of TRn|B by PRE_TOPC:def 2;
then consider U be Subset of TRn such that
A16: U in the topology of TRn
and
A17: h.:BA = U/\[#](TRn|B) by PRE_TOPC :def 4;
reconsider U as open Subset of TRn by A16,PRE_TOPC:def 2;
A18: Int U = U by TOPS_1:23;
p is Element of REAL n by EUCLID:22;
then |. p-p .|=0;
then p in Ball(p,r) by A14;
then p in BA by A2,A3,XBOOLE_0:def 4;
then hp in h.:BA by A7,A8,FUNCT_1:def 6;
then hp in U by A17,XBOOLE_0:def 4;
then consider s be Real such that
A19: s>0
and
A20: Ball(hP,s) c= U by A18,GOBOARD6:5;
take s;
thus s>0 by A19;
let W be open Subset of TRn |B such that
A21: hp in W
and
A22: W c= Ball(hp,s);
A23: W/\B=W by A9,XBOOLE_1:28;
Ball(hp,s)=Ball(hP,s) by TOPREAL9:13;
then W c= U by A22,A20;
then
A24: W c= U/\B by A23, XBOOLE_1:27;
h"(U/\B) = h"(h.:BA ) by A17, PRE_TOPC:def 5
.= BA by FUNCT_1:94, XBOOLE_1:17,A8, A5;
then
A25: h"W c= BA by A24,RELAT_1:143;
reconsider hW=h"W as open Subset of TRn|A by TOPS_2:43,A5,A9,A12;
A26: BA c= Ball(p,r) by XBOOLE_1:17;
set BW=B\W;
reconsider bw=BW as Subset of TRn|B by XBOOLE_1:36,A9;
A27: [#](TRn | (A\hW))=A\hW by PRE_TOPC:def 5;
p in h"W by A8,A2,A3,A21,FUNCT_1:def 7;
then consider F be Function of TRn | (A\hW),T such that
A28: F is continuous
and
A29: for h be Function of TRn |A,T st h is continuous holds
h| (A\hW) <> F by A15, A25,A26,XBOOLE_1:1;
A30: BW c= B by XBOOLE_1:36;
then
A31: h".:BW = h"BW by TOPS_2:55,A9,A10, A5
.= (h"B) \ hW by FUNCT_1:69
.=A\hW by RELAT_1:134,A8,A10;
per cases;
suppose
A32: A\hW is empty;
reconsider n1=n-1 as Element of NAT by NAT_1:20, A11;
set h = the continuous Function of TRn |A,Tunit_circle(n1+1);
reconsider H=h as Function of TRn |A,T;
A33: H| (A\hW) = {} by A32;
H| (A\hW) <> F by A29;
hence thesis by A33, A32;
end;
suppose
A34: A\hW is non empty;
reconsider hbw=(h") | (B\W) as Function of
(TRn |B) | bw, (TRn|A) | (h".:BW) by A2,A3,A12,JORDAN24:12;
A35: (TRn |B) | bw = TRn |BW by PRE_TOPC:7, XBOOLE_1:36;
A36: (TRn|A) | (h".:BW) = TRn | (A\hW) by A31, PRE_TOPC:7,A7;
then reconsider HBW =hbw as Function of TRn |BW, TRn | (A\hW)
by A35;
reconsider fhW=F*HBW as Function of TRn | BW,Tunit_circle(n)
by A34;
take fhW;
thus fhW is continuous by A34,JORDAN24:13,
A6,A2,A3,A12,A36,A35,A28,TOPS_2:46;
let g be Function of TRn |B,T such that
A37: g is continuous;
reconsider gh=g*h as Function of TRn |A,T by A12;
A38: gh is continuous by A5, A12,A37,TOPS_2:46;
assume
A39: g| BW = fhW;
A40: dom F = A\hW by FUNCT_2:def 1, A11,A27;
A41: rng (h| (A\hW)) = h.:(A\hW) by RELAT_1:115
.=h.:(h"BW) by TOPS_2:55,A9,A10,A31, A5,A30
.=BW by FUNCT_1:77,A10, XBOOLE_1:36;
gh| (A\hW) = g*(h| (A\hW)) by RELAT_1:83
.=g*((id BW)*(h| (A\hW))) by A41,RELAT_1:53
.=(g*(id BW))*(h| (A\hW)) by RELAT_1:36
.=(g|BW)*(h| (A\hW)) by RELAT_1:65
.=F*(((h") | (B\W)) * (h| (A\hW))) by A39, RELAT_1:36
.=F*(((h") *id BW) * (h| (A\hW))) by RELAT_1:65
.=F*((h") *(id BW * (h| (A\hW)))) by RELAT_1:36
.=F*((h") * (h| (A\hW))) by A41,RELAT_1:53
.=F*((h" * h) | (A\hW)) by RELAT_1:83
.=(F*(h" * h)) | (A\hW) by RELAT_1:83
.=(F*(id A)) | (A\hW) by TOPS_2:52,A8,A10, A5,A9
.=F | dom F by A40, XBOOLE_1:36,RELAT_1:51
.=F;
hence contradiction by A38,A29;
end;
end;
then not hp in Fr B by A1,Th9;
then hp in B\Fr B by A12,A9,XBOOLE_0:def 5;
hence thesis by TOPS_1:40;
end;
end;
theorem
A is closed & B is closed implies
for h be Function of (TOP-REAL n) |A,(TOP-REAL n) |B st
h is being_homeomorphism
holds h.:Int A = Int B & h.:Fr A = Fr B
proof
assume that
A1: A is closed
and
A2: B is closed;
set TR=TOP-REAL n;
A3: [#](TR|A) = A by PRE_TOPC:def 5;
A4: Int B c= B by TOPS_1:16;
A5: [#](TR|B)=B by PRE_TOPC:def 5;
let h be Function of TR |A,TR |B such that
A6: h is being_homeomorphism;
A7: dom h = [#](TR|A) by A6,TOPS_2:def 5;
A8: rng h = [#](TR|B) by A6,TOPS_2:def 5;
A9: Fr A \/Int A = (A \Int A) \/Int A by A1,TOPS_1:43
.= A\/Int A by XBOOLE_1:39
.= A by TOPS_1:16,XBOOLE_1:12;
thus
A10: h.:Int A = Int B
proof
thus h.:Int A c= Int B
proof
let y be object;
assume y in h.:Int A;
then ex x be object st x in dom h & x in Int A & h.x=y
by FUNCT_1:def 6;
hence thesis by A2,A6,Th11;
end;
let y be object;
assume
A11: y in Int B;
then consider x be object such that
A12: x in dom h
and
A13: h.x=y by A4,A8,A5,FUNCT_1:def 3;
reconsider x as Point of TR by A7,A3,A12;
assume
A14: not y in h.:Int A;
not x in Int A by A12,FUNCT_1:def 6,A14,A13;
then x in Fr A by A12,A9,A3,XBOOLE_0:def 3;
then h.x in Fr B by Th10,A1,A6;
hence thesis by A11,A13, TOPS_1:39,XBOOLE_0:3;
end;
Fr A = A \Int A by A1,TOPS_1:43;
then h.:Fr A = (h.:A) \ (h.:Int A) by A6,FUNCT_1:64
.= B\ (h.:Int A) by RELAT_1:113,A7,A8,A3,A5
.= Fr B by A10,A2,TOPS_1:43;
hence thesis;
end;
begin :: Topological Invariance of Dimension - An Introduction to Manifolds
theorem Th13:
for r st r>0
for U be Subset of Tdisk(p,r) st U is open non empty
for A be Subset of TOP-REAL n st A = U holds Int A is non empty
proof
set TR=TOP-REAL n;
let r be Real such that
A1: r>0;
let U be Subset of Tdisk(p,r) such that
A2: U is open non empty;
consider q be object such that
A3: q in U by A2;
A4: [#]Tdisk(p,r) = cl_Ball(p,r) by PRE_TOPC:def 5;
then q in cl_Ball(p,r) by A3;
then reconsider q as Point of TR;
the TopStruct of TR=TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider Q=q as Point of Euclid n by TOPMETR:12;
A5: |.q-p.|<= r by A3,A4,TOPREAL9:8;
U in the topology of Tdisk(p,r) by A2,PRE_TOPC:def 2;
then consider W be Subset of TR such that
A6: W in the topology of TR
and
A7: U = W /\ [#]Tdisk(p,r) by PRE_TOPC:def 4;
reconsider W as open Subset of TR by A6,PRE_TOPC:def 2;
Int W=W by TOPS_1:23;
then q in Int (W) by A3,A7,XBOOLE_0:def 4;
then consider s be Real such that
A8: s>0
and
A9: Ball(Q,s) c= W by GOBOARD6:5;
set m=min(s,r),mr=m/(2*r);
A10: 0< m by A8,A1, XXREAL_0:21;
then
A11: m/2 < m by XREAL_1:216;
set qp = (-mr)*(q-p)+q;
A12: qp -q = (-mr)*(q-p)+(q-q) by RLVECT_1:def 3
.=(- mr)*(q-p)+0.TR by RLVECT_1:def 10
.=(-mr)*(q-p) by RLVECT_1:def 4;
|.-mr.| =--mr by A10, A1,ABSVALUE:def 1;
then
A13: |.qp-q.| = mr *|.q-p.| by A12,EUCLID:11;
mr *r = m/2/r*r by XCMPLX_1:78
.= m/2*(r/r)
.= m/2*1 by XCMPLX_1:60,A1
.= m/2;
then |.qp-q.| <= m/2 by A5,XREAL_1:66, A10,A13;
then
A14: |.qp-q.| < m by A11,XXREAL_0:2;
m <= s by XXREAL_0: 17;
then |.qp-q.| <s by A14,XXREAL_0:2;
then
A15: qp in Ball(q,s);
let A be Subset of TR such that
A16: A=U;
A17: Ball(p,r) c= cl_Ball(p,r) by TOPREAL9:16;
A18: -mr+1 <0+1 by XREAL_1:8, A10, A1;
A19: (1-mr)*|. q-p .| < r
proof
per cases;
suppose |. q-p .| =0;
hence thesis by A1;
end;
suppose |. q-p .| >0;
then (1-mr)*|. q-p .| < 1*|. q-p .| by A18,XREAL_1:68;
hence thesis by A5,XXREAL_0:2;
end;
end;
A20: r/(2*r) = r/r/2 by XCMPLX_1:78
.= 1/2 by XCMPLX_1:60,A1;
mr <= r/(2*r) by A1, XXREAL_0:17, XREAL_1:72;
then 1-mr >= 1-1/2 by A20,XREAL_1:10;
then
A21: |.1-mr.|=1-mr by ABSVALUE:def 1;
qp - p =(-mr)*(q-p)+(q-p) by RLVECT_1:def 3
.=(-mr)*(q-p)+1*(q-p) by RLVECT_1:def 8
.=(1-mr)*(q-p) by RLVECT_1:def 6;
then |.qp - p.| <r by A19, A21,EUCLID:11;
then qp in Ball(p,r);
then
A22:qp in Ball(q,s)/\Ball(p,r) by A15,XBOOLE_0:def 4;
Ball(q,s) c= W by A9, TOPREAL9:13;
hence thesis by A17,XBOOLE_1:27,A7,A4,A16,A22,TOPS_1:22;
end;
theorem
for T be non empty TopSpace
for A,B be Subset of T
for r,s st r>0 & s>0
for pA be Point of TOP-REAL n,pB be Point of TOP-REAL m st
T|A,Tdisk(pA,r) are_homeomorphic &
T|B,Tdisk(pB,s) are_homeomorphic &
Int A meets Int B
holds n = m
proof
let T be non empty TopSpace;
let A,B be Subset of T;
let r,s be Real such that
A1: r>0
and
A2: s>0;
A3: Int B c= B by TOPS_1:16;
A4: Int A/\Int B c= Int B by XBOOLE_1:17;
A5: [#](T|B) = B by PRE_TOPC:def 5;
then reconsider IB=Int A/\Int B as Subset of T|B by A3,A4,XBOOLE_1:1;
let pA be Point of TOP-REAL n, pB be Point of TOP-REAL m such that
A6: T|A, Tdisk(pA,r) are_homeomorphic
and
A7: T|B,Tdisk(pB,s) are_homeomorphic
and
A8: Int A meets Int B;
consider hB be Function of T|B,Tdisk(pB,s) such that
A9: hB is being_homeomorphism by A7,T_0TOPSP:def 1;
A10: (T|B) | IB = T| (Int A/\Int B) by A3,A4,XBOOLE_1:1, PRE_TOPC:7;
A11: [#]Tdisk(pB,s) = cl_Ball(pB,s) by PRE_TOPC:def 5;
then reconsider hBI=hB.:IB as Subset of TOP-REAL m by XBOOLE_1:1;
A12: Int A/\Int B in the topology of T by PRE_TOPC:def 2;
Int A/\Int B is non empty by A8;
then consider p be set such that
A13: p in Int A/\Int B;
reconsider p as Point of T by A13;
A14: dom hB =[#](T|B) by A9, TOPS_2:def 5;
then
A15: hB.p in hB.:IB by A13,FUNCT_1:def 6;
p in Int B by A13,XBOOLE_0:def 4;
then Tdisk(pB,s) is non empty by A14, A3;
then reconsider f=hB|IB as Function of (T|B) | IB,Tdisk(pB,s) | (hB.:IB)
by A13,JORDAN24:12;
A16: Int A c= A by TOPS_1:16;
IB/\B =IB by A3,A4,XBOOLE_1:1,XBOOLE_1:28;
then IB in the topology of (T|B) by A12,A5,PRE_TOPC :def 4;
then IB is open by PRE_TOPC:def 2;
then hB.:IB is open by A13,A9, TOPGRP_1:25, A2;
then Int hBI is non empty by A13,A2,Th13;
then hBI is non boundary;
then
A17: ind hBI = m by Th6;
A18: Int A/\Int B c= Int A by XBOOLE_1:17;
A19: Tdisk(pB,s) | (hB.:IB) = (TOP-REAL m) |hBI by PRE_TOPC:7,A11;
then reconsider F=f as Function of T| (Int A/\Int B),(TOP-REAL m) |hBI
by A10;
F is being_homeomorphism by A9,METRIZTS:2,A19,A10;
then
A20:F" is being_homeomorphism by TOPS_2:56, A15;
consider hA be Function of T|A,Tdisk(pA,r) such that
A21: hA is being_homeomorphism by A6,T_0TOPSP:def 1;
A22: [#](T|A) = A by PRE_TOPC:def 5;
then reconsider IA=Int A/\Int B as Subset of T|A by A16,A18,XBOOLE_1:1;
A23: (T|A) | IA = T| (Int A/\Int B) by A16,A18,XBOOLE_1:1, PRE_TOPC:7;
A24: dom hA =[#](T|A) by A21, TOPS_2:def 5;
then
A25: hA.p in hA.:IA by A13,FUNCT_1:def 6;
p in Int A by A13,XBOOLE_0:def 4;
then Tdisk(pA,r) is non empty by A24, A16;
then reconsider g=hA|IA as Function of (T|A) | IA,Tdisk(pA,r) | (hA.:IA)
by A13,JORDAN24:12;
A26: [#]Tdisk(pA,r) = cl_Ball(pA,r) by PRE_TOPC:def 5;
then reconsider hAI=hA.:IA as Subset of TOP-REAL n by XBOOLE_1:1;
A27: Tdisk(pA,r) | (hA.:IA) = (TOP-REAL n) |hAI by PRE_TOPC:7,A26;
then reconsider G=g as Function of T| (Int A/\Int B),(TOP-REAL n) |hAI
by A23;
reconsider GF=G*(F") as Function of (TOP-REAL m) |hBI,(TOP-REAL n) |hAI
by A13;
G is being_homeomorphism by A21,METRIZTS:2,A27,A23;
then GF is being_homeomorphism by A20,TOPS_2:57, A25, A15, A13;
then hBI,hAI are_homeomorphic by T_0TOPSP:def 1,METRIZTS:def 1;
then
A28: ind hBI=ind hAI by TOPDIM_1:27;
IA/\A =IA by A16,A18,XBOOLE_1:1,XBOOLE_1:28;
then IA in the topology of (T|A) by A12,A22,PRE_TOPC :def 4;
then IA is open by PRE_TOPC:def 2;
then hA.:IA is open by A13,A21, TOPGRP_1:25, A1;
then Int hAI is non empty by A13,A1,Th13;
then hAI is non boundary;
hence thesis by A17,Th6,A28;
end;
theorem
for T be non empty TopSpace
for A,B be Subset of T
for r,s st r>0 & s>0
for pA be Point of TOP-REAL n, pB be Point of TOP-REAL m st
T|A,(TOP-REAL n) |Ball(pA,r) are_homeomorphic &
T|B,Tdisk(pB,s) are_homeomorphic &
Int A meets Int B
holds n = m
proof
let T be non empty TopSpace;
let A,B be Subset of T;
let r,s be Real such that
A1: r>0
and
A2: s>0;
let pA be Point of TOP-REAL n, pB be Point of TOP-REAL m such that
A3: T|A,(TOP-REAL n) |Ball(pA,r) are_homeomorphic
and
A4: T|B,Tdisk(pB,s) are_homeomorphic
and
A5: Int A meets Int B;
A6: Int A c= A by TOPS_1:16;
set TBALL=(TOP-REAL n) |Ball(pA,r);
consider hA be Function of T|A,TBALL such that
A7: hA is being_homeomorphism by A3,T_0TOPSP:def 1;
A8: Int A/\Int B c= Int A by XBOOLE_1:17;
A9: [#](T|A) = A by PRE_TOPC:def 5;
then reconsider IA=Int A/\Int B as Subset of T|A by A6,A8,XBOOLE_1:1;
A10: (T|A) | IA = T| (Int A/\Int B) by A6,A8,XBOOLE_1:1, PRE_TOPC:7;
A11: [#]TBALL = Ball(pA,r) by PRE_TOPC:def 5;
then reconsider hAI=hA.:IA as Subset of TOP-REAL n by XBOOLE_1:1;
A12: Int A/\Int B in the topology of T by PRE_TOPC:def 2;
Int A/\Int B is non empty by A5;
then consider p be set such that
A13: p in Int A/\Int B;
reconsider p as Point of T by A13;
A14: dom hA =[#](T|A) by A7, TOPS_2:def 5;
then
A15: hA.p in hA.:IA by A13,FUNCT_1:def 6;
p in Int A by A13,XBOOLE_0:def 4;
then TBALL is non empty by A14, A6;
then reconsider g=hA|IA as Function of (T|A) | IA,TBALL | (hA.:IA)
by A13,JORDAN24:12;
A16: Int B c= B by TOPS_1:16;
IA/\A =IA by A6,A8,XBOOLE_1:1,XBOOLE_1:28;
then IA in the topology of (T|A) by A12,A9,PRE_TOPC :def 4;
then IA is open by PRE_TOPC:def 2;
then hA.:IA is open by A13,A7, TOPGRP_1:25, A1;
then hAI is open by A11,TSEP_1:9;
then Int hAI is non empty by TOPS_1:23,A15;
then
A17: hAI is non boundary;
consider hB be Function of T|B,Tdisk(pB,s) such that
A18: hB is being_homeomorphism by A4,T_0TOPSP:def 1;
A19: TBALL | (hA.:IA) = (TOP-REAL n) |hAI by PRE_TOPC:7,A11;
then reconsider G=g as Function of T| (Int A/\Int B),(TOP-REAL n) |hAI
by A10;
A20: Int A/\Int B c= Int B by XBOOLE_1:17;
A21: [#](T|B) = B by PRE_TOPC:def 5;
then reconsider IB=Int A/\Int B as Subset of T|B by A16,A20,XBOOLE_1:1;
A22: (T|B) | IB = T| (Int A/\Int B) by A16,A20,XBOOLE_1:1, PRE_TOPC:7;
A23: dom hB =[#](T|B) by A18, TOPS_2:def 5;
then
A24: hB.p in hB.:IB by A13,FUNCT_1:def 6;
p in Int B by A13,XBOOLE_0:def 4;
then Tdisk(pB,s) is non empty by A23, A16;
then reconsider f=hB|IB as Function of (T|B) | IB,Tdisk(pB,s) | (hB.:IB)
by A13,JORDAN24:12;
A25: [#]Tdisk(pB,s) = cl_Ball(pB,s) by PRE_TOPC:def 5;
then reconsider hBI=hB.:IB as Subset of TOP-REAL m by XBOOLE_1:1;
A26: Tdisk(pB,s) | (hB.:IB) = (TOP-REAL m) |hBI by PRE_TOPC:7,A25;
then reconsider F=f as Function of T| (Int A/\Int B),(TOP-REAL m) |hBI
by A22;
F is being_homeomorphism by A18,METRIZTS:2,A26,A22;
then
A27:F" is being_homeomorphism by TOPS_2:56,A24;
reconsider GF=G*(F") as Function of (TOP-REAL m) |hBI,(TOP-REAL n) |hAI
by A13;
G is being_homeomorphism by A7,METRIZTS:2,A19,A10;
then GF is being_homeomorphism by A27,TOPS_2:57, A15, A24, A13;
then hBI,hAI are_homeomorphic by T_0TOPSP:def 1,METRIZTS:def 1;
then
A28: ind hBI=ind hAI by TOPDIM_1:27;
IB/\B =IB by A16,A20,XBOOLE_1:1,XBOOLE_1:28;
then IB in the topology of (T|B) by A12,A21,PRE_TOPC :def 4;
then IB is open by PRE_TOPC:def 2;
then hB.:IB is open by A13,A18, TOPGRP_1:25, A2;
then Int hBI is non empty by A13,A2,Th13;
then hBI is non boundary;
then ind hBI = m by Th6;
thus then thesis by A17,Th6,A28;
end;
theorem Th15:
transl(p,TOP-REAL n).: Ball(q,r) = Ball(q+p,r) &
transl(p,TOP-REAL n).: cl_Ball(q,r) = cl_Ball(q+p,r) &
transl(p,TOP-REAL n).: Sphere(q,r) = Sphere(q+p,r)
proof
set TR=TOP-REAL n,T=transl(p,TR);
A2:now let q;
q-p+p = q -(p-p) by RLVECT_1:29
.= q-0.TR by RLVECT_1:def 10
.= q by RLVECT_1:13;
hence transl(p,TR).(q-p)= q by RLTOPSP1:def 10;
end;
A3:now
let x be Point of TR;
thus (x+p) - (q+p) = ((x+p) - p)-q by RLVECT_1:27
.=(x+(p - p))-q by RLVECT_1:28
.= (x+0.TR)-q by RLVECT_1:def 10
.= x- q by RLVECT_1:def 4;
end;
A4:dom T = [#]TR by FUNCT_2:def 1;
thus T.: Ball(q,r) = Ball(q+p,r)
proof
thus T.: Ball(q,r) c= Ball(q+p,r)
proof
let y be object;
assume y in transl(p,TR).:Ball(q,r);
then consider x be object such that
A5: x in dom T
and
A6: x in Ball(q,r)
and
A7: T.x = y by FUNCT_1:def 6;
reconsider x as Point of TR by A5;
A8: y = x+p by A7,RLTOPSP1:def 10;
A9: (x+p) - (q+p) =x-q by A3;
|.x-q.| < r by A6,TOPREAL9:7;
hence thesis by A9,A8;
end;
let y be object;
assume
A10:y in Ball(q+p,r);
then reconsider y as Point of TR;
A11: (y-p) - q = y-(p + q ) by RLVECT_1:27;
|. y-(q+p).| < r by A10,TOPREAL9:7;
then A12: y-p in Ball(q,r) by A11;
T.(y-p)= y by A2;
hence thesis by A12,A4,FUNCT_1:def 6;
end;
thus T.: cl_Ball(q,r) = cl_Ball(q+p,r)
proof
thus T.: cl_Ball(q,r) c= cl_Ball(q+p,r)
proof
let y be object;
assume y in T.:cl_Ball(q,r);
then consider x be object such that
A13: x in dom T
and
A14: x in cl_Ball(q,r)
and
A15: T.x = y by FUNCT_1:def 6;
reconsider x as Point of TR by A13;
A16: y = x+p by A15,RLTOPSP1:def 10;
A17: (x+p) - (q+p) =x-q by A3;
|.x-q.| <= r by A14,TOPREAL9:8;
hence thesis by A17,A16;
end;
let y be object;
assume
A18:y in cl_Ball(q+p,r);
then reconsider y as Point of TR;
A19: (y-p) - q = y-(p + q ) by RLVECT_1:27;
|. y-(q+p).| <= r by A18,TOPREAL9:8;
then A20: y-p in cl_Ball(q,r) by A19;
T.(y-p)= y by A2;
hence thesis by A20,A4,FUNCT_1:def 6;
end;
thus T.: Sphere(q,r) c= Sphere(q+p,r)
proof
let y be object;
assume y in T.:Sphere(q,r);
then consider x be object such that
A21: x in dom T
and
A22: x in Sphere(q,r)
and
A23: T.x = y by FUNCT_1:def 6;
reconsider x as Point of TR by A21;
A24: y = x+p by A23,RLTOPSP1:def 10;
A25: (x+p) - (q+p) = x- q by A3;
|.x-q.| = r by A22,TOPREAL9:9;
hence thesis by A25,A24;
end;
let y be object;
assume
A26:y in Sphere(q+p,r);
then reconsider y as Point of TR;
A27: (y-p) - q = y-(p + q ) by RLVECT_1:27;
|. y-(q+p).| = r by A26,TOPREAL9:9;
then A28: y-p in Sphere(q,r) by A27;
T.(y-p)= y by A2;
hence thesis by A28,A4,FUNCT_1:def 6;
end;
theorem Th16:
for s st s > 0 holds
mlt(s,TOP-REAL n).: Ball(p,r) = Ball(s*p,r*s) &
mlt(s,TOP-REAL n).: cl_Ball(p,r) = cl_Ball(s*p,r*s) &
mlt(s,TOP-REAL n).: Sphere(p,r) = Sphere(s*p,r*s)
proof
let s such that
A1:s>0;
set TR=TOP-REAL n,M=mlt(s,TR),ss=|.s.|,s1=1/s;
A2:ss =s by A1,ABSVALUE:def 1;
A4:dom M = [#]TR by FUNCT_2:def 1;
A5:s*s1 = 1 by A1,XCMPLX_1:87;
thus M.: Ball(p,r) = Ball(s*p,r*s)
proof
thus M.: Ball(p,r) c= Ball(s*p,r*s)
proof
let y be object;
assume y in M.:Ball(p,r);
then consider x be object such that
A6: x in dom M
and
A7: x in Ball(p,r)
and
A8: M.x = y by FUNCT_1:def 6;
reconsider q=x as Point of TR by A6;
A9: y = s*q by A8, RLTOPSP1:def 13;
(s*q) - (s*p) =s*(q-p) by RLVECT_1:34;
then A10: |. (s*q) - (s*p).| = s* |.q-p.| by A2,EUCLID:11;
s*|.q-p.| < r*s by A7,TOPREAL9:7,A1,XREAL_1:68;
hence thesis by A10,A9;
end;
let y be object;
A11: r*s*s1 = r*(s*s1);
assume
A12:y in Ball(s*p,r*s);
then reconsider q=y as Point of TR;
A13: |.(s1*q)-p.|*s*s1 = |.(s1*q)-p.|*(s*s1);
A14:s*(s1*q) = (s*s1)*q by RLVECT_1:def 7
.= 1*q by A1,XCMPLX_1:87
.= q by RLVECT_1:def 8;
then |.q-s*p.| = |.s*((s1*q)-p).| by RLVECT_1:34
.= s*|.(s1*q)-p.| by A2,EUCLID:11;
then |.(s1*q)-p.| < r
by A11,A13,A5,A12,TOPREAL9:7,A1,XREAL_1:68;
then A15: s1*q in Ball(p,r);
M.(s1*q) = q by A14,RLTOPSP1:def 13;
hence thesis by A4,A15,FUNCT_1:def 6;
end;
thus M.: cl_Ball(p,r) = cl_Ball(s*p,r*s)
proof
thus M.: cl_Ball(p,r) c= cl_Ball(s*p,r*s)
proof
let y be object;
assume y in M.:cl_Ball(p,r);
then consider x be object such that
A16: x in dom M
and
A17: x in cl_Ball(p,r)
and
A18: M.x = y by FUNCT_1:def 6;
reconsider q=x as Point of TR by A16;
A19: y = s*q by A18, RLTOPSP1:def 13;
(s*q) - (s*p) =s*(q-p) by RLVECT_1:34;
then A20: |. (s*q) - (s*p).| = s* |.q-p.| by A2,EUCLID:11;
s*|.q-p.| <= r*s by A17,TOPREAL9:8,A1,XREAL_1:64;
hence thesis by A20,A19;
end;
let y be object;
A21: r*s*s1 = r*(s*s1);
assume
A22:y in cl_Ball(s*p,r*s);
then reconsider q=y as Point of TR;
A23: |.(s1*q)-p.|*s*s1 = |.(s1*q)-p.|*(s*s1);
A24:s*(s1*q) = (s*s1)*q by RLVECT_1:def 7
.= 1*q by A1,XCMPLX_1:87
.= q by RLVECT_1:def 8;
then |.q-s*p.| = |.s*((s1*q)-p).| by RLVECT_1:34
.= s*|.(s1*q)-p.| by A2,EUCLID:11;
then
|.(s1*q)-p.| <= r by A21,A23,A5,A22,TOPREAL9:8,A1,XREAL_1:64;
then A25: s1*q in cl_Ball(p,r);
M.(s1*q) = q by A24,RLTOPSP1:def 13;
hence thesis by A4,A25,FUNCT_1:def 6;
end;
thus M.: Sphere(p,r) c= Sphere(s*p,r*s)
proof
let y be object;
assume y in M.:Sphere(p,r);
then consider x be object such that
A26: x in dom M
and
A27: x in Sphere(p,r)
and
A28: M.x = y by FUNCT_1:def 6;
reconsider q=x as Point of TR by A26;
(s*q) - (s*p) =s*(q-p) by RLVECT_1:34;
then A29: |. (s*q) - (s*p).| = s* |.q-p.| by A2,EUCLID:11;
s*|.q-p.| = r*s by A27,TOPREAL9:9;
then s*q in Sphere(s*p,r*s) by A29;
hence thesis by A28, RLTOPSP1:def 13;
end;
let y be object;
assume
A30:y in Sphere(s*p,r*s);
then reconsider q=y as Point of TR;
A31: |.(s1*q)-p.|*s*s1 = |.(s1*q)-p.|*(s*s1);
A32: r*s*s1 = r*(s*s1);
A33:s*(s1*q) = (s*s1)*q by RLVECT_1:def 7
.= 1*q by A1,XCMPLX_1:87
.= q by RLVECT_1:def 8;
then |.q-s*p.| = |.s*((s1*q)-p).| by RLVECT_1:34
.= s*|.(s1*q)-p.| by A2,EUCLID:11;
then |.(s1*q)-p.| = r by A32, A31,A5, A30,TOPREAL9:9;
then A34: s1*q in Sphere(p,r);
M.(s1*q) = q by A33,RLTOPSP1:def 13;
hence thesis by A4,A34,FUNCT_1:def 6;
end;
theorem Th17:
for f be rotation homogeneous additive Function of
TOP-REAL n,TOP-REAL n st f is onto
holds f.: Ball(p,r) = Ball(f.p,r) &
f.: cl_Ball(p,r) = cl_Ball(f.p,r) &
f.: Sphere(p,r) = Sphere(f.p,r)
proof
set TR=TOP-REAL n;
let f be rotation homogeneous additive Function of TR,TR;
assume
f is onto;
A2: -f.p = (-1)*(f.p) by RLVECT_1:16
.= f.((-1)*p) by TOPREAL9:def 4
.= f.(-p) by RLVECT_1:16;
A3:rng f = the carrier of TR by FUNCT_2:def 3;
thus f.:Ball(p,r) = Ball(f.p,r)
proof
thus f.:Ball(p,r) c= Ball(f.p,r)
proof
let y be object;
assume y in f.:Ball(p,r);
then consider x be object such that
A4: x in dom f
and
A5: x in Ball(p,r)
and
A6: f.x = y by FUNCT_1:def 6;
reconsider q=x as Point of TR by A4;
f.q-f.p = f.(q-p) by A2,VECTSP_1:def 20;
then A7: |.f.q-f.p.|= |.q-p.| by MATRTOP3:def 4;
|.q-p.| < r by A5,TOPREAL9:7;
hence thesis by A7,A6;
end;
let y be object;
assume
A8:y in Ball(f.p,r);
then consider x be object such that
A9: x in dom f
and
A10: f.x=y by A3,FUNCT_1:def 3;
reconsider x as Point of TR by A9;
f.x-f.p = f.(x-p) by A2,VECTSP_1:def 20;
then A11: |.f.x-f.p.|= |.x-p.| by MATRTOP3:def 4;
|.f.x-f.p.| < r by A8,A10,TOPREAL9:7;
then x in Ball(p,r) by A11;
hence thesis by A9,A10,FUNCT_1:def 6;
end;
thus f.:cl_Ball(p,r) = cl_Ball(f.p,r)
proof
thus f.:cl_Ball(p,r) c= cl_Ball(f.p,r)
proof
let y be object;
assume y in f.:cl_Ball(p,r);
then consider x be object such that
A12: x in dom f
and
A13: x in cl_Ball(p,r)
and
A14: f.x = y by FUNCT_1:def 6;
reconsider q=x as Point of TR by A12;
f.q-f.p = f.(q-p) by A2,VECTSP_1:def 20;
then A15: |.f.q-f.p.|= |.q-p.| by MATRTOP3:def 4;
|.q-p.| <= r by A13,TOPREAL9:8;
hence thesis by A15,A14;
end;
let y be object;
assume
A16:y in cl_Ball(f.p,r);
then consider x be object such that
A17: x in dom f
and
A18: f.x=y by A3,FUNCT_1:def 3;
reconsider x as Point of TR by A17;
f.x-f.p = f.(x-p) by A2,VECTSP_1:def 20;
then A19: |.f.x-f.p.|= |.x-p.| by MATRTOP3:def 4;
|.f.x-f.p.| <= r by A16,A18,TOPREAL9:8;
then x in cl_Ball(p,r) by A19;
hence thesis by A17,A18,FUNCT_1:def 6;
end;
thus f.:Sphere(p,r) c= Sphere(f.p,r)
proof
let y be object;
assume y in f.:Sphere(p,r);
then consider x be object such that
A20: x in dom f
and
A21: x in Sphere(p,r)
and
A22: f.x = y by FUNCT_1:def 6;
reconsider q=x as Point of TR by A20;
f.q-f.p = f.(q-p) by A2,VECTSP_1:def 20;
then A23: |.f.q-f.p.|= |.q-p.| by MATRTOP3:def 4;
|.q-p.| = r by A21,TOPREAL9:9;
hence thesis by A23,A22;
end;
let y be object;
assume
A24:y in Sphere(f.p,r);
then consider x be object such that
A25: x in dom f
and
A26: f.x=y by A3,FUNCT_1:def 3;
reconsider x as Point of TR by A25;
f.x-f.p = f.(x-p) by A2,VECTSP_1:def 20;
then A27: |.f.x-f.p.|= |.x-p.| by MATRTOP3:def 4;
|.f.x-f.p.| = r by A24,A26,TOPREAL9:9;
then x in Sphere(p,r) by A27;
hence thesis by A25,A26,FUNCT_1:def 6;
end;
Lm4: for n be non zero Element of NAT
for p be Point of TOP-REAL (n+1) st r <= 1 & |.p.| >= 1 & |.p.| < 1 +r
& p.(n+1)>0 & p|n = 0* n
ex c be Real, h be Function of
(TOP-REAL (n+1)) | (Sphere(0. TOP-REAL (n+1),1) /\ cl_Ball(p,r)),
Tdisk(0.TOP-REAL n,c)
st c>0 & h is being_homeomorphism &
h.:(Sphere(0.TOP-REAL (n+1),1) /\ Sphere(p,r)) = Sphere(0.TOP-REAL n,c)
proof
let n be non zero Element of NAT;
set n1=n+1;
set TR=TOP-REAL n,TR1=TOP-REAL n1;
set Sp= {q where q is Point of TR1: q.n1>=0 & |.q.|=1};
set Sn= {q where q is Point of TR1: q.n1<=0 & |.q.|=1};
A1:Sp c= the carrier of TR1
proof
let x be object;
assume x in Sp;
then ex p be Point of TR1 st p=x & p.n1>=0 & |.p.|=1;
hence thesis;
end;
Sn c= the carrier of TR1
proof
let x be object;
assume x in Sn;
then ex p be Point of TR1 st p=x & p.n1<=0 & |.p.|=1;
hence thesis;
end;
then reconsider Sp,Sn as Subset of TR1 by A1;
deffunc f(Nat)=PROJ(n1,$1);
consider F be FinSequence such that
A2: len F = n & for k be Nat st k in dom F holds F.k=f(k)
from FINSEQ_1:sch 2;
rng F c= Funcs(the carrier of TR1,the carrier of R^1)
proof
let x be object;
assume x in rng F;
then consider i be object such that
A3: i in dom F
and
A4: F.i = x by FUNCT_1:def 3;
reconsider i as Nat by A3;
f(i) in Funcs(the carrier of TR1,the carrier of R^1) by FUNCT_2:8;
hence thesis by A2,A3,A4;
end;
then reconsider F as FinSequence of
Funcs(the carrier of TR1,the carrier of R^1) by FINSEQ_1:def 4;
reconsider F as Element of n-tuples_on
Funcs(the carrier of TR1,the carrier of R^1) by A2,FINSEQ_2:92;
set FF=<:F:>;
let p be Point of TR1 such that
A5: r <= 1
and
A6: |.p.| >= 1
and
A7: |.p.| < 1 +r
and
A8: p.n1 > 0
and
A9: p|n = 0* n;
set pn1=p.n1;
A10: 1+0 < 1+pn1 *pn1 by A8,XREAL_1:6;
rng p c= REAL;
then A11: p is FinSequence of REAL by FINSEQ_1:def 4;
len p = n1 by CARD_1:def 7;
then reconsider P=p as Element of REAL n1 by A11,FINSEQ_2:92;
|. (P|n) .| = 0 by A9,EUCLID:7;
then |. (P|n) .| ^2=0;
then |.p.|^2 = 0 + pn1^2 by REAL_NS1:10;
then A12: |.p.| = pn1 or |.p.| = - pn1 by SQUARE_1:40;
then A13: pn1 -1 < r by A8,A7,XREAL_1:19;
set SP=Sphere(0.TR1,1),CL =cl_Ball(p,r);
A15: for q be Point of TR1 holds p - q = (-q) +*(n1, pn1-q.n1)
proof
let q be Point of TR1;
set q1=(-q) +*(n1, pn1-q.n1);
A16: len (p-q) = n1 by CARD_1:def 7;
A17: len (-q)=n1 by CARD_1:def 7;
for i st 1<=i & i <=n1 holds (p-q).i = q1.i
proof
let i such that
A19: 1<=i
and
A20: i <= n1;
A21: i in dom (- q) by A19,A20,A17, FINSEQ_3: 25;
i in dom (p-q) by A19,A20,A16, FINSEQ_3: 25;
then A22: (p-q).i = (p.i) - (q.i) by VALUED_1:13;
per cases by A20,NAT_1:8;
suppose
A23:i <= n;
then i < n1 by NAT_1:13;
then A24: q1.i = (-q).i by FUNCT_7:32
.= -(q.i) by VALUED_1:8;
p.i = p| (Seg n).i by A23,A19,FINSEQ_1:1,FUNCT_1:49;
then p.i = 0 by A9;
hence thesis by A24,A22;
end;
suppose i = n1;
hence thesis by A21,FUNCT_7:31,A22;
end;
end;
hence thesis by A16,CARD_1:def 7;
end;
set dd=(pn1*pn1+1-r*r) / (2*pn1),cc = 1 -dd*dd;
set c = sqrt cc;
set TD=Tdisk(0.TR,1),Tc = Tdisk(0.TR,c);
A25: [#]TD = cl_Ball(0.TR,1) by PRE_TOPC:def 5;
1<1+r by A6,A7,XXREAL_0:2;
then A26: r>0 by XREAL_1:32;
then r*r <= 1*1 by A5,XREAL_1:66;
then r*r < 1+pn1 *pn1 by A10,XXREAL_0:2;
then A27: 0 < 1+pn1 *pn1 - r*r by XREAL_1:50;
A28:1<= n1 by NAT_1:11;
A29:for q be Point of TR1 holds |.q -p.|^2= |.q.|^2 - 2*q.n1*pn1 + pn1*pn1
proof
let q be Point of TR1;
set pqn=pn1-q.n1;
A30:(-q).n1=-(q.n1) by VALUED_1:8;
len (-q)= n1 by CARD_1:def 7;
then A31: n1 in dom (-q) by A28,FINSEQ_3:25;
|.q -p.| = |.-(q-p).| by EUCLID:10
.= |.p-q.| by RLVECT_1:33;
hence |.q-p.|^2 = Sum sqr (p-q) by TOPREAL9:5
.=Sum sqr ((-q) +*(n1,pqn)) by A15
.= Sum sqr (-q) - ((-q).n1)^2 + pqn^2 by A31,MATRTOP3:3
.=|.-q.|^2 - ((-q).n1)^2 + pqn^2 by TOPREAL9:5
.= |.q.|^2 - (-(q.n1))*(-(q.n1)) + pqn^2 by A30,EUCLID:10
.= |.q.|^2 - 2*q.n1*pn1 + pn1*pn1;
end;
A32: SP /\ CL c= Sp
proof
let x be object;
assume
A33: x in SP/\CL;
then reconsider x as Point of TR1;
x in CL by A33,XBOOLE_0:def 4;
then A34: |. x-p.| <= r by TOPREAL9:8;
set xn1=x.n1;
rng x c= REAL;
then A35: x is FinSequence of REAL by FINSEQ_1:def 4;
len x = n1 by CARD_1:def 7;
then reconsider X=x as Element of REAL n1 by A35,FINSEQ_2:92;
x in SP by A33,XBOOLE_0:def 4;
then A36: |.x.| = 1 by TOPREAL9:12;
|.x -p.|^2= |.x.|^2 - 2*xn1*pn1 + pn1*pn1 by A29;
then - 2*xn1*pn1 + (1+pn1*pn1) <=r*r by A34,XREAL_1:66,A36;
then -2*xn1*pn1 <= r*r-(1+pn1*pn1) by XREAL_1:19;
then -2*xn1*pn1 <= -(1+pn1*pn1-r*r);
then xn1 >=0 by XREAL_1:24, A8,A27;
hence thesis by A36;
end;
A37:FF.:(SP /\ CL) c= cl_Ball(0.TR,c)
proof
let y be object;
assume y in FF.:(SP /\ CL);
then consider x be object such that
A38: x in dom FF
and
A39: x in SP/\CL
and
A40: FF.x= y by FUNCT_1:def 6;
reconsider x as Point of TR1 by A38;
rng x c= REAL;
then A41: x is FinSequence of REAL by FINSEQ_1:def 4;
len x = n1 by CARD_1:def 7;
then reconsider X=x as Element of REAL n1 by A41,FINSEQ_2:92;
x in SP by A39,XBOOLE_0:def 4;
then A42: |.x.| = 1 by TOPREAL9:12;
FF.x in rng FF by A38,FUNCT_1:def 3;
then reconsider Y=y as Point of TR by A40;
set xn1=x.n1;
A43: Y-0.TR = Y by RLVECT_1:13;
x in CL by A39,XBOOLE_0:def 4;
then A44: |. x-p.| <= r by TOPREAL9:8;
|.x -p.|^2= |.x.|^2 - 2*xn1*pn1 + pn1*pn1 by A29;
then - 2*xn1*pn1 + (1+pn1*pn1) <=r*r by A44,XREAL_1:66,A42;
then -2*xn1*pn1 <= r*r-(1+pn1*pn1) by XREAL_1:19;
then -2*xn1*pn1 <= -(1+pn1*pn1-r*r);
then (2*pn1)*xn1 >= 1+pn1*pn1-r*r by XREAL_1:24;
then xn1 >= (1+pn1*pn1-r*r) / (2*pn1) by A8,XREAL_1:79;
then A45: xn1*xn1 >= dd*dd by A8,A27,XREAL_1:66;
|.x.|^2 = 1 by A42;
then 1 - (X. n1)^2 = |. (X|n) .| ^2 + (X. n1)^2 -(X. n1)^2
by REAL_NS1:10
.= |. (X|n) .| ^2;
then |. (X|n) .| ^2 <= cc by A45,XREAL_1:10;
then A46:sqrt |. (X|n) .| ^2 <= sqrt cc by SQUARE_1:26;
FF.x = x|n by A2,Th1;
then |. Y .| <= c by SQUARE_1:def 2,A46,A40;
hence thesis by A43;
end;
[#](TR1 |Sp) = Sp by PRE_TOPC:def 5;
then reconsider SC = SP /\ CL as Subset of TR1 |Sp by A32;
A47:(TR1 |Sp) |SC = TR1 | (SP/\CL) by A32,PRE_TOPC:7;
A48:Sn = {t where t is Point of TR1: t.n1 <=0 & |.t.|=1};
then A49: <:F:>.:Sp = cl_Ball(0.TR,1) by A2,Th1;
then reconsider FS=FF|Sp as Function of TR1 |Sp,TD by JORDAN24:12;
Sp = {l where l is Point of TR1: l.n1>=0 & |.l.|=1};
then reconsider s1=Sp,s2=Sn as closed Subset of TR1 by Th2,A48;
A50: Ball(0.TR,1) c= cl_Ball(0.TR,1) by TOPREAL9:16;
A51: pn1-1 >=0 by A12,A8,A6,XREAL_1:48;
then A52: (pn1-1)*r < r*r by A13,XREAL_1:68;
(pn1-1)*(pn1-1) <= (pn1-1)*r by A13,A51,XREAL_1:66;
then pn1*pn1+1-2*pn1 < r*r by A52,XXREAL_0:2;
then pn1*pn1+1-r*r < 2*pn1 by XREAL_1:11;
then A53: dd <1 by A27,XREAL_1:189;
then dd*dd < dd*1 by A8,A27,XREAL_1:68;
then dd *dd < 1 by A53,XXREAL_0:2;
then A54:cc >0 by XREAL_1:50;
then A55: cc = c^2 by SQUARE_1:def 2;
1-dd*dd < 1-0 by A8,A27,XREAL_1:10;
then A56: c < sqrt 1 by SQUARE_1:27,A54;
then cl_Ball(0.TR,c) c= Ball(0.TR,1) by JORDAN:21;
then A57: cl_Ball(0.TR,c) c= cl_Ball(0.TR,1) by A50;
cl_Ball(0.TR,c) c= FF.:(SP /\ CL)
proof
let y be object;
A58: dd^2=dd*dd;
assume
A59: y in cl_Ball(0.TR,c);
then consider x be object such that
A60: x in dom FF
and
A61: x in Sp
and
A62: FF.x = y by A57,A49,FUNCT_1:def 6;
y in rng FF by A60,A62,FUNCT_1:def 3;
then reconsider Y=y as Point of TR;
A63: |.Y.| <= c by A59,TOPREAL9:11;
consider q be Point of TR1 such that
A64: q=x
and
A65: q.n1 >=0
and
A66: |.q.|=1 by A61;
set qn1=q.n1;
rng q c= REAL;
then A67: q is FinSequence of REAL by FINSEQ_1:def 4;
len q = n1 by CARD_1:def 7;
then reconsider Q=q as Element of REAL n1 by A67,FINSEQ_2:92;
A68: |.Q.|^2 = 1 by A66;
then 1 = |.(Q|n).|^2 + qn1^2 by REAL_NS1:10
.= |.Y.|^2 + qn1*qn1 by A2,Th1,A62,A64;
then 1-(qn1*qn1) <= c*c by A63,XREAL_1:66;
then A69: qn1*qn1 >= dd*dd by A55,XREAL_1:10;
qn1^2 =qn1 *qn1;
then (pn1*pn1+1-r*r) / (2*pn1) <= qn1 by A69,A65,A58,SQUARE_1:47;
then (pn1*pn1+1-r*r) / (2*pn1)*(2*pn1) <= qn1*(2*pn1)
by A8,XREAL_1: 64;
then pn1*pn1+1-r*r <= qn1*(2*pn1) by A8,XCMPLX_1:87;
then A70: pn1*pn1+1-qn1*(2*pn1) <= r*r by XREAL_1:12;
|.q -p.|^2= 1 - 2*qn1*pn1 + pn1*pn1 by A68,A29;
then |.q -p.|^2 <= r^2 by A70;
then |.q -p.| <= r by SQUARE_1:47,A26;
then A71:q in CL;
q-0.TR1 = q by RLVECT_1:13;
then q in SP by A66;
then q in SP/\CL by A71,XBOOLE_0:def 4;
hence thesis by A60,A64,FUNCT_1:def 6,A62;
end;
then FS.:SC = cl_Ball(0.TR,c) by A37,A32,RELAT_1:129;
then A72: TD| (FS.:SC) = Tc by A25,PRE_TOPC:7;
SP /\ CL is non empty
proof
A73: pn1 -1 <= 1+r -1 by A12,A8,A7,XREAL_1:9;
pn1-1 >=0 by A12,A8,A6,XREAL_1:48;
then A74: (pn1-1)*(pn1-1) <=r*r by A73,XREAL_1:66;
set q = (0*n1)+*(n1,1);
rng q c= REAL;
then
W: q is FinSequence of REAL by FINSEQ_1:def 4;
len q = n1 by CARD_1:def 7;
then reconsider q as Point of TR1 by W,EUCLID:76;
A75:n1 in Seg n1 by FINSEQ_1:4;
A76: |.q.| = |. 1 .| by FINSEQ_1:4,TOPREALC:13
.= 1 by ABSVALUE:def 1;
A77: n1 in dom (0*n1) by A75;
|.q.|^2 = 1*1 by A76;
then |.q -p.|^2= 1*1 - 2*q.n1*pn1 + pn1*pn1 by A29
.= 1*1-2*1*pn1 +pn1*pn1 by A77,FUNCT_7:31
.= (1-pn1)*(1-pn1);
then |.q -p.|^2 <= r^2 by A74;
then |.q -p.| <= r by A26,SQUARE_1:47;
then A78: q in CL;
q-0.TR1 = q by RLVECT_1:13;
then q in SP by A76;
hence thesis by A78,XBOOLE_0:def 4;
end;
then reconsider H=FS | SC as Function of TR1 | (SP/\CL),Tc
by A47,A72,JORDAN24 :12;
take c,H;
for H be Function of TR1 |Sp,Tdisk(0.TOP-REAL n,1) st H= <:F:>|Sp
holds H is being_homeomorphism by A2,A48,Th1;
hence c>0 & H is being_homeomorphism by A47,A72, A54,METRIZTS:2;
A79: Sphere(p,r) c= CL by TOPREAL9:17;
then SP/\Sphere(p,r) c= SC by XBOOLE_1:27;
then
A80: FS.:(SP/\Sphere(p,r)) = FF.:(SP/\Sphere(p,r))
by A32,XBOOLE_1:1,RELAT_1:129;
Sphere(0.TR,c) c= Ball(0.TR,1) by A56,JORDAN:22;
then A81: Sphere(0.TR,c) c= cl_Ball(0.TR,1) by A50;
A82: Sphere(0.TOP-REAL n,c) c= FF.:(SP /\ Sphere(p,r))
proof
let y be object;
A83: dd^2=dd*dd;
assume
A84: y in Sphere(0.TOP-REAL n,c);
then consider x be object such that
A85: x in dom FF
and
A86: x in Sp
and
A87: FF.x = y by A81,A49,FUNCT_1:def 6;
y in rng FF by A85,A87,FUNCT_1:def 3;
then reconsider Y=y as Point of TR;
A88: |.Y.| = c by A84,TOPREAL9:12;
consider q be Point of TR1 such that
A89: q=x
and
A90: q.n1 >=0
and
A91: |.q.|=1 by A86;
rng q c= REAL;
then A92: q is FinSequence of REAL by FINSEQ_1:def 4;
len q = n1 by CARD_1:def 7;
then reconsider Q=q as Element of REAL n1 by A92,FINSEQ_2:92;
set qn1=q.n1;
A93: qn1^2 =qn1 *qn1;
A94: |.Q.|^2 = 1 by A91;
then 1 = |.(Q|n).|^2 + qn1^2 by REAL_NS1:10
.= |.Y.|^2 + qn1*qn1 by A2,Th1,A87,A89;
then dd = qn1 or dd = -qn1 by A88,A55,A93,A83,SQUARE_1:40;
then pn1*pn1+1-r*r = qn1*(2*pn1) by A90, A8,A27,XCMPLX_1:87;
then A95: pn1*pn1+1-qn1*(2*pn1) = r*r;
|.q -p.|^2= 1 - 2*qn1*pn1 + pn1*pn1 by A94,A29;
then |.q -p.|^2 = r^2 by A95;
then |.q -p.| = r or |.q -p.| = -r by SQUARE_1:40;
then A96:q in Sphere(p,r) by A26;
q-0.TR1 = q by RLVECT_1:13;
then q in SP by A91;
then q in SP/\Sphere(p,r) by A96,XBOOLE_0:def 4;
hence thesis by A85, A89,FUNCT_1:def 6,A87;
end;
FF.:(SP /\ Sphere(p,r)) c= Sphere(0.TOP-REAL n,c)
proof
let y be object;
assume y in FF.:(SP /\ Sphere(p,r));
then consider x be object such that
A98: x in dom FF
and
A99: x in SP/\Sphere(p,r)
and
A100: FF.x= y by FUNCT_1:def 6;
reconsider x as Point of TR1 by A98;
FF.x in rng FF by A98,FUNCT_1:def 3;
then reconsider Y=y as Point of TR by A100;
set xn1=x.n1;
rng x c= REAL;
then A101: x is FinSequence of REAL by FINSEQ_1:def 4;
len x = n1 by CARD_1:def 7;
then reconsider X=x as Element of REAL n1 by A101,FINSEQ_2:92;
x in SP by A99,XBOOLE_0:def 4;
then A102: |.x.| = 1 by TOPREAL9:12;
then |.x.|^2 = 1;
then A103: 1 - (X. n1)^2 = |. (X|n) .| ^2 + (X. n1)^2 -(X. n1)^2
by REAL_NS1:10
.= |. (X|n) .| ^2;
x in Sphere(p,r) by A99,XBOOLE_0:def 4;
then A104: |. x-p.| = r by TOPREAL9:9;
|.x -p.|^2= |.x.|^2 - 2*xn1*pn1 + pn1*pn1 by A29;
then (2*pn1)*xn1 = 1+pn1*pn1-r*r by A102,A104;
then xn1 = (1+pn1*pn1-r*r) / (2*pn1) by A8,XCMPLX_1:89;
then |. (X|n) .| = c or |. (X|n) .| = -c by A103,SQUARE_1:def 2;
then A105: |. Y .| = c by A54,A100, A2,Th1;
Y-0.TR = Y by RLVECT_1:13;
hence thesis by A105;
end;
hence thesis by A80, A82,A79,XBOOLE_1:27,RELAT_1:129;
end;
theorem
for p,q be Point of TOP-REAL (n+1)
for r,s st s <= r & r <= |.p-q.| & s < |.p-q.| &
|.p-q.|< s+ r
ex h be Function of (TOP-REAL (n+1)) | (Sphere(p,r)/\ cl_Ball(q,s)),
Tdisk(0.TOP-REAL n,1)
st h is being_homeomorphism &
h.:(Sphere(p,r) /\ Sphere(q,s)) = Sphere(0.TOP-REAL n,1)
proof
N:n in NAT by ORDINAL1:def 12;
set n1=n+1,TR=TOP-REAL n,TR1=TOP-REAL n1;
let p,q be Point of TR1;
let r,s be Real such that
A1: s <= r
and
A2: r <= |.p-q.|
and
A3: s < |.p-q.|
and
A4: |.p -q.|< s+r;
reconsider r1=1/r as Real;
A5:r>0 by A1,A4;
then A6:r*r1=1 by XCMPLX_1:87;
set A=Sphere(p,r)/\ cl_Ball(q,s);
set TR=TOP-REAL n;
set y=(1/r)*(q-p);
set T=transl(-p,TR1),M= mlt(r1,TR1);
A7: 0*n1 = 0.TR1 by EUCLID:70;
A8: -p + p = 0.TR1 by RLVECT_1:5;
A9: |.y.| = |. r1 .|*|.q-p.| by EUCLID:11
.= r1*|.q-p.| by A5,ABSVALUE:def 1;
set Y=0*n1 +*(n1,|.y.|);
rng Y c= REAL;
then
W: Y is FinSequence of REAL by FINSEQ_1:def 4;
A10: len Y = n1 by CARD_1:def 7;
then Y is Element of REAL n1 by W,FINSEQ_2:92;
then reconsider Y as Point of TR1 by EUCLID:22;
set S=Sphere(0.TR1,1),CL=cl_Ball(Y,s*r1);
A11: [#](TR1| (S/\CL)) = S/\CL by PRE_TOPC:def 5;
A12: |.Y.| = |. |.y.| .| by TOPREALC:13,FINSEQ_1:3;
then A13: |.Y.| = |.y.| by ABSVALUE:def 1;
ex ROT be homogeneous additive rotation Function of TR1,TR1 st
ROT is being_homeomorphism & ROT.y=Y
proof
per cases;
suppose n=0;
then ex ROT be homogeneous additive Function of TR1,TR1 st
( ROT is rotation)& ROT.y = Y &
(AutMt ROT = AxialSymmetry(n1,n1) or AutMt ROT = 1.(F_Real,n1))
by A13,MATRTOP3:40;
hence thesis;
end;
suppose n>0;
then n1<>1;
then ex ROT be homogeneous additive Function of TR1,TR1 st
( ROT is base_rotation)& ROT.y = Y by A13,MATRTOP3:41;
hence thesis;
end;
end;
then consider ROT be homogeneous additive rotation Function of TR1,TR1
such that
ROT is being_homeomorphism
and
A14: ROT.y=Y;
set h=ROT*M*T;
A15: |.ROT.(0.TR1).| = |. 0.TR1.| by MATRTOP3:def 4
.= |.0*n1.| by EUCLID:70
.= 0 by EUCLID:7;
A16: h.:Sphere(q,s) = (ROT*M).:(T.:Sphere(q,s))by RELAT_1:126
.= (ROT*M).:(Sphere(-p+q,s)) by Th15
.= ROT.:(M.:(Sphere(-p+q,s))) by RELAT_1:126
.= ROT.:(Sphere(r1*(q-p),s*r1)) by Th16, A5
.= Sphere(Y,s*r1) by A14,Th17;
ROT.(0.TR1) is Element of REAL n1 by EUCLID:22;
then A17: ROT.(0.TR1) = 0.TR1 by A15,A7,EUCLID:8;
A18: h.:Sphere(p,r) = (ROT*M).:(T.:Sphere(p,r))by RELAT_1:126
.= (ROT*M).:(Sphere(-p+p,r)) by Th15
.= ROT.:(M.:(Sphere(0.TR1,r))) by A8,RELAT_1:126
.= ROT.:(Sphere(r1*0.TR1,r*r1)) by Th16, A5
.= ROT.:(Sphere(r1*0.TR1,1)) by A5,XCMPLX_1:87
.= ROT.:(Sphere(0.TR1,1)) by RLVECT_1:10
.= Sphere(0.TR1,1) by Th17,A17;
reconsider hA=h|A as Function of TR1|A,TR1| (h.:A) by JORDAN24:12;
ROT*M is being_homeomorphism by A5,TOPS_2:57;
then A19: h is being_homeomorphism by TOPS_2:57;
then A20:hA is being_homeomorphism by METRIZTS:2;
reconsider TD = Tdisk(0.TR,1) as non empty TopSpace;
A21: the carrier of Tdisk(0.TR,1) = cl_Ball(0.TR,1) by N,BROUWER:3;
h.:cl_Ball(q,s) = (ROT*M).:(T.:cl_Ball(q,s))by RELAT_1:126
.= (ROT*M).:(cl_Ball(-p+q,s)) by Th15
.= ROT.:(M.:(cl_Ball(-p+q,s))) by RELAT_1:126
.= ROT.:(cl_Ball(y,s*r1)) by Th16, A5
.= cl_Ball(Y,s*r1) by A14,Th17;
then A22:h.:A = S/\CL by A18,A5,FUNCT_1:62;
|.p-q.| - s < s+r-s by A4,XREAL_1:9;
then A23: r1*(|.p-q.|-s) < 1 by A6, A5,XREAL_1:68;
A24:dom (0*n1) = Seg n1;
q-p = - (p-q) by RLVECT_1:33;
then A25: |.p-q.| = |.q-p.| by EUCLID:10;
|.p-q.|+s >= r+s by A2,XREAL_1:6;
then |.p-q.|+s > |.p-q.| by A4,XXREAL_0:2;
then |.p-q.|+s > r by A2,XXREAL_0:2;
then A26: r1*(|.p-q.|+s) > 1 by A6, A5,XREAL_1:68;
A27:s>0
proof
assume s <=0;
then s+r <= r+0 by XREAL_1:6;
hence thesis by A4,XXREAL_0:2,A2;
end;
per cases;
suppose
A28: n=0;
set E=Euclid n1;
reconsider YY=Y as Point of E by EUCLID:67;
Y.1 = |.y.| by A24,FINSEQ_1:3,A28,FUNCT_7:31;
then A29:YY = <*|.y.|*> by CARD_1:def 7,A28,FINSEQ_1:40;
then
A30: cl_Ball(YY,s*r1) =
{<*w*> where w is Real: |.y.| qua ExtReal -(s qua ExtReal*r1) <= w &
w <= |.y.| qua ExtReal + (s qua ExtReal*r1)}
by A28,TOPDIM_2:17;
A31:[#]TR = {0.TR} by A28,EUCLID:22,EUCLID:77;
then reconsider ZZ = 0.TR as Point of TD by A21,ZFMISC_1:33;
A32: [#]Tdisk(0.TR,1) ={0.TR} by A21,A31,ZFMISC_1:33;
reconsider z=0,yy=|.y.| as Real;
0.TR1 = <* z *> by A7,A28,FINSEQ_2:59;
then A33: Fr Ball(0.TR1,1) = {<*z qua ExtReal-1*>,<*z qua ExtReal+1*>}
by A28,TOPDIM_2:18;
A34: Fr Ball(0.TR1,1) = S by JORDAN:24;
then A35: <*z+1*> in S by A33,TARSKI:def 2;
A36: cl_Ball(YY,s*r1) = cl_Ball(Y,s*r1) by TOPREAL9:14;
then A37: <*z qua ExtReal+1*> in CL by A23,A9,A25,A26,A30;
then A38: A is non empty by A22, A35,XBOOLE_0:def 4;
reconsider SCL=S/\CL as non empty Subset of TR1 by A35,A37,XBOOLE_0:def 4;
reconsider zz= <* 1 *> as Point of TR1| SCL
by A35,A37,XBOOLE_0:def 4,A11;
set h1 = TR1| SCL --> ZZ,h2 = TD --> zz;
S/\CL c= {<*z+1*>}
proof
let v be object;
assume
A39: v in Sphere(0.TR1,1)/\cl_Ball(Y,s*r1);
then v in Sphere(0.TR1,1) by XBOOLE_0:def 4;
then A40:v = <*z+1*> or v = <*z-1*> by A34,A33,TARSKI:def 2;
assume
A41: not v in {<*z+1*>};
v in cl_Ball(Y,s*r1) by A39, XBOOLE_0:def 4;
then ex w be Real st <*z-1*>=<*w*> & |.y.| -s*r1 <= w &
w <= |.y .| + s*r1 by A41,A40,TARSKI:def 1,A30,A36;
then r1*(|.p-q.|-s) <= - r1*r by FINSEQ_1:76,A9,A25,A6;
then r1*(|.p-q.|-s) <= r1*(-r);
then A42: r <= -(|.p-q.|-s) by A5,XREAL_1:68,XREAL_1:25;
s - |.p-q.| < |.p-q.|-|.p-q.| by A3,XREAL_1:14;
hence thesis by A42, A5;
end;
then A43:h1 = zz .--> 0.TR by A11,ZFMISC_1:33;
then rng h1 = {0.TR} by FUNCOP_1:88;
then h1 is onto by A32,FUNCT_2:def 3;
then A44: h1" = (zz .--> 0.TR )" by A43,TOPS_2:def 4;
reconsider HA=hA as Function of TR1|A,TR1| SCL by A22;
reconsider HH =h1*HA as Function of TR1 | (Sphere(p,r)/\ cl_Ball(q,s)),
Tdisk(0. TR,1);
take HH;
A45: dom h1 = [#](TR1| (S/\CL));
A46:HA is being_homeomorphism by A19,METRIZTS:2,A22;
h2 = 0.TR .--> zz by A21,A31,ZFMISC_1:33;
then A47: h1" is continuous by NECKLACE:9,A44;
rng h1 = [#]Tdisk(0.TR,1) by ZFMISC_1:33,A32;
then h1 is being_homeomorphism by A45, A43,A47,TOPS_2:def 5;
hence HH is being_homeomorphism by A38, TOPS_2:57,A46;
A48: Fr Ball(Y,s*r1) = Sphere(Y,s*r1) by A1,A27,JORDAN:24;
A49: Fr Ball(Y,s qua ExtReal*r1) =
{<*|.y.| qua ExtReal-s *r1*>,<*|.y.|qua ExtReal+s *r1*>}
by A1,A27,A29,A28,TOPDIM_2:18;
S /\ Sphere(Y,s*r1) ={}
proof
assume S /\ Sphere(Y,s*r1) <>{};
then consider z be object such that
A50: z in S /\ Sphere(Y,s*r1) by XBOOLE_0:def 1;
A51: z in Sphere(Y,s*r1) by A50,XBOOLE_0:def 4;
A52: z in S by A50,XBOOLE_0:def 4;
per cases by A52,A34,A33, TARSKI:def 2, A51, A48,A49;
suppose z = <* 1 *> & z = <*|.y.|-s*r1*>;
hence thesis by FINSEQ_1:76, A23,A9,A25;
end;
suppose z = <* 1 *> & z = <*|.y.|+s*r1*>;
hence thesis by FINSEQ_1:76, A26,A9,A25;
end;
suppose z = <* -1 *> & z = <*|.y.|-s*r1*>;
then -1 = r1*(|.p-q.|-s) by FINSEQ_1:76,A9,A25;
then |.p-q.|-s < 0 by A5;
then |.p-q.|-s+s < 0+ s by XREAL_1:6;
hence thesis by A3;
end;
suppose z = <* -1 *> & z = <*|.y.|+s*r1*>;
hence thesis by FINSEQ_1:76, A26,A9,A25;
end;
end;
then h .: (Sphere(p,r) /\ Sphere(q,s)) = {} by A18,A16,FUNCT_1:62,A5;
then HA.: (Sphere(p,r) /\ Sphere(q,s)) ={} by XBOOLE_1:3,RELAT_1:128;
then A53: HH.:(Sphere(p,r) /\ Sphere(q,s))= h1.:{} by RELAT_1:126
.= {};
Sphere(0.TR,1)={}
proof
assume Sphere(0.TR,1) <>{};
then consider w be object such that
A54: w in Sphere(0.TR,1) by XBOOLE_0:def 1;
w = 0.TR by A54, A28,EUCLID:77;
then A55: |.0.TR.| = 1 by A54, TOPREAL9:12;
0.TR = 0*n by EUCLID:70;
hence contradiction by A55,EUCLID:7;
end;
hence thesis by A53;
reconsider P=p,Q=q as Point of E by EUCLID:67;
end;
suppose
A56:n>0;
A57:len (0*n) = n by CARD_1:def 7;
r1*|.p-q.| < r1*(s+r) by A27,A1,A4,XREAL_1:68;
then |.Y.| < r1*r + r1*s by A9,A25, A12,ABSVALUE:def 1;
then A58: |.Y.| < 1 +r1*s by A1,A27, XCMPLX_1:106;
A59:n < n1 by NAT_1:13;
then A60: len (Y|n) = n by A10,FINSEQ_1:59;
A61: now
let k be Nat;
assume that
A64: 1<= k
and
A65: k <= n;
A66: Y.k = (0*n1).k by A65,A59,FUNCT_7:32;
(Y|n).k = Y.k by A64,A65,FINSEQ_1:1,FUNCT_1:49;
hence (Y|n).k = (0*n).k by A66;
end;
A68: r1 * r = 1 by A1,A27, XCMPLX_1:106;
then A69:r1*s <=1 by A1,XREAL_1:64,A27;
|.y.| >= 1 by XREAL_1:64,A27,A1,A2,A9,A25,A68;
then A70: |.Y.| >=1 by A12,ABSVALUE:def 1;
Y.n1 >0 by A2, A5,A9,A25, FINSEQ_1:3,FUNCT_7:31,A24;
then consider c be Real, H be Function of TR1| (S/\ CL),
Tdisk(0.TR,c) such that
A71: c>0
and
A72: H is being_homeomorphism
and
A73: H.:(S /\ Sphere(Y,r1*s)) = Sphere(0.TR,c)
by A56,Lm4,A69,A70,A58,A61,FINSEQ_1:14,A57,A60;
rng H = [#]Tdisk(0.TR,c) by A72,TOPS_2:def 5;
then A74:A is non empty by A71,A22;
then reconsider HH=H*hA as Function of TR1|A,Tdisk(0.TR,c) by A22;
A75: HH is being_homeomorphism by A71,A72,A74,A20,A22,TOPS_2:57;
reconsider c1=1/c as Real;
set MM= mlt(c1,TR);
A76: c1 * 0.TR = 0.TR by RLVECT_1:10;
A77:c1*c = 1 by A71,XCMPLX_1:106;
then A78: MM.:cl_Ball(0.TR,c) = cl_Ball(0.TR,1) by A71,A76,Th16;
then reconsider MM1=MM |cl_Ball(0.TR,c) as
Function of Tdisk(0.TR,c), Tdisk(0.TR,1) by JORDAN24:12;
reconsider MH=MM1*HH as Function of TR1|A,Tdisk(0.TR,1) by A71;
take MH;
MM1 is being_homeomorphism by METRIZTS:2,A71,A78;
hence MH is being_homeomorphism by A75, A71,A74,TOPS_2:57;
Sphere(q,s) c= cl_Ball(q,s) by TOPREAL9:17;
then hA.:(Sphere(p,r) /\ Sphere(q,s)) = h.:(Sphere(p,r) /\ Sphere(q,s))
by XBOOLE_1:27,RELAT_1:129;
then HH.:(Sphere(p,r) /\ Sphere(q,s))
= H.:(h.:(Sphere(p,r) /\ Sphere(q,s))) by RELAT_1:126
.= Sphere(0.TR,c) by A73,A18,A16,FUNCT_1:62,A5;
hence MH.:(Sphere(p,r) /\ Sphere(q,s)) = MM1.:Sphere(0.TR,c)
by RELAT_1:126
.= MM.:Sphere(0.TR,c) by TOPREAL9:17,RELAT_1:129
.= Sphere(0.TR,1) by Th16,A71,A76,A77;
end;
end;