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;