Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Projections in $n$-Dimensional Euclidean Space to Each Coordinates

**by****Roman Matuszewski, and****Yatsuka Nakamura**- Received November 3, 1997
- MML identifier: JORDAN2B

- [ Mizar article, MML identifier index ]

environ vocabulary ARYTM, PRE_TOPC, EUCLID, METRIC_1, TOPMETR, FINSEQ_1, FINSEQ_2, BORSUK_1, FUNCT_1, FUNCOP_1, RELAT_1, ARYTM_1, RFINSEQ, BOOLE, RLVECT_1, FUNCT_4, COMPLEX1, SQUARE_1, RVSUM_1, ABSVALUE, ARYTM_3, PCOMPS_1, ORDINAL2, TOPS_2, SUBSET_1, MCART_1, FUNCT_5, FINSEQ_4, SEQ_1; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, FINSEQ_4, RVSUM_1, STRUCT_0, ABSVALUE, RELAT_1, FINSEQ_1, TOPS_2, FUNCT_1, FUNCT_2, BINOP_1, SQUARE_1, FUNCT_7, TOPREAL1, TOPMETR, PRE_TOPC, BORSUK_1, METRIC_1, EUCLID, RFINSEQ, FINSEQ_2, BINARITH, PSCOMP_1, PCOMPS_1, FINSEQOP; constructors ABSVALUE, TOPS_2, REAL_1, TOPMETR, RFINSEQ, TOPREAL1, SQUARE_1, FUNCT_7, PSCOMP_1, FINSEQOP, BINARITH, FINSEQ_4; clusters STRUCT_0, RELSET_1, EUCLID, TOPMETR, METRIC_1, PCOMPS_1, FINSEQ_2, FUNCT_7, XREAL_0, ARYTM_3, SEQ_1, MEMBERED, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin ::1. PROJECTIONS reserve x,x1,x2,y,z,z1 for set; reserve s1,r,r1,r2 for real number; reserve s,w1,w2 for Real; reserve n,i,j for Nat; reserve X for non empty TopSpace; reserve p,p1,p2,p3 for Point of TOP-REAL n; reserve P for Subset of TOP-REAL n; definition let n,i be Nat,p be Element of TOP-REAL n; func Proj(p,i) -> Real means :: JORDAN2B:def 1 for g being FinSequence of REAL st g=p holds it=g/.i; end; theorem :: JORDAN2B:1 ex f being map of TOP-REAL n,R^1 st for p being Element of TOP-REAL n holds f.p=Proj(p,i); theorem :: JORDAN2B:2 for i st i in Seg n holds (0*n).i=0; theorem :: JORDAN2B:3 for i st i in Seg n holds Proj(0.REAL n,i)=0; theorem :: JORDAN2B:4 for r,p,i st i in Seg n holds Proj(r*p,i)=r*Proj(p,i); theorem :: JORDAN2B:5 for p,i st i in Seg n holds Proj(-p,i)=-Proj(p,i); theorem :: JORDAN2B:6 for p1,p2,i st i in Seg n holds Proj(p1+p2,i)=Proj(p1,i)+Proj(p2,i); theorem :: JORDAN2B:7 for p1,p2,i st i in Seg n holds Proj(p1-p2,i)=Proj(p1,i)-Proj(p2,i); theorem :: JORDAN2B:8 len (0*n)=n; theorem :: JORDAN2B:9 i<=n implies (0*n)|i=0*i; theorem :: JORDAN2B:10 (0*n)/^i=0*(n-'i); theorem :: JORDAN2B:11 Sum(0*i)=0; theorem :: JORDAN2B:12 for w being FinSequence,r being set,i holds len (w+*(i,r))=len w; theorem :: JORDAN2B:13 for D being non empty set, w being FinSequence of D, r being Element of D st i in dom w holds w+*(i,r)=(w|(i-'1))^<*r*>^(w/^i); theorem :: JORDAN2B:14 for r being Real st i in Seg n holds Sum( (0*n)+*(i,r))=r; theorem :: JORDAN2B:15 for q being Element of REAL n,p,i st i in Seg n & q=p holds Proj(p,i)<=|.q.| & (Proj(p,i))^2<=|.q.|^2; begin :: 2. CONTINUITY OF PROJECTIONS theorem :: JORDAN2B:16 for s1,P,i st P = { p: s1>Proj(p,i) } & i in Seg n holds P is open; theorem :: JORDAN2B:17 for s1,P,i st P = { p: s1<Proj(p,i) } & i in Seg n holds P is open; theorem :: JORDAN2B:18 for P being Subset of TOP-REAL n,a,b being real number, i st P = { p where p is Element of TOP-REAL n: a<Proj(p,i) & Proj(p,i)<b } & i in Seg n holds P is open; theorem :: JORDAN2B:19 for a,b being real number,f being map of TOP-REAL n,R^1,i st (for p being Element of TOP-REAL n holds f.p=Proj(p,i)) holds f"({s:a<s & s<b})={p where p is Element of TOP-REAL n: a<Proj(p,i) & Proj(p,i)<b}; theorem :: JORDAN2B:20 for M being non empty MetrSpace,f being map of X,TopSpaceMetr(M) holds (for r being real number,u being Element of the carrier of M,P being Subset of TopSpaceMetr(M) st r>0 & P=Ball(u,r) holds f"P is open) implies f is continuous; theorem :: JORDAN2B:21 for u being Point of RealSpace,r,u1 being real number st u1=u & r>0 holds Ball(u,r)={s:u1-r<s & s<u1+r}; theorem :: JORDAN2B:22 for f being map of TOP-REAL n,R^1,i st i in Seg n & (for p being Element of TOP-REAL n holds f.p=Proj(p,i)) holds f is continuous; begin ::3. 1-DIMENSIONAL AND 2-DIMENSIONAL CASES theorem :: JORDAN2B:23 for s holds abs <*s*>=<*abs(s)*>; theorem :: JORDAN2B:24 for p being Element of TOP-REAL 1 ex r being Real st p=<*r*>; theorem :: JORDAN2B:25 for w being Element of Euclid 1 ex r being Real st w=<*r*>; definition let r be real number; func |[ r ]| -> Point of TOP-REAL 1 equals :: JORDAN2B:def 2 <*r*>; end; theorem :: JORDAN2B:26 s*|[ r ]|=|[ s*r ]|; theorem :: JORDAN2B:27 |[ r1+r2 ]|=|[ r1 ]|+|[ r2 ]|; theorem :: JORDAN2B:28 |[ 0 ]|=0.REAL 1; theorem :: JORDAN2B:29 |[r1]|=|[r2]| implies r1=r2; theorem :: JORDAN2B:30 for P being Subset of R^1,b being real number st P = { s: s<b } holds P is open; theorem :: JORDAN2B:31 for P being Subset of R^1,a being real number st P = { s: a<s } holds P is open; theorem :: JORDAN2B:32 for P being Subset of R^1,a,b being real number st P = { s: a<s & s<b } holds P is open; theorem :: JORDAN2B:33 for u being Point of Euclid 1,r,u1 being real number st <*u1*>=u & r>0 holds Ball(u,r)={<*s*>:u1-r<s & s<u1+r}; theorem :: JORDAN2B:34 for f being map of TOP-REAL 1,R^1 st (for p being Element of TOP-REAL 1 holds f.p=Proj(p,1)) holds f is_homeomorphism; theorem :: JORDAN2B:35 for p being Element of TOP-REAL 2 holds Proj(p,1)=p`1 & Proj(p,2)=p`2; theorem :: JORDAN2B:36 for p being Element of TOP-REAL 2 holds Proj(p,1)=proj1.p & Proj(p,2)=proj2.p;

Back to top