:: Projections in n-Dimensional Euclidean Space to Each Coordinates :: by Roman Matuszewski and Yatsuka Nakamura :: :: Received November 3, 1997 :: Copyright (c) 1997-2021 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 NUMBERS, REAL_1, SUBSET_1, XBOOLE_0, PRE_TOPC, EUCLID, NAT_1, FINSEQ_1, PARTFUN1, RELAT_1, FUNCT_1, TOPMETR, STRUCT_0, SUPINF_2, CARD_1, FINSEQ_2, ARYTM_1, ARYTM_3, XXREAL_0, RFINSEQ, CARD_3, FUNCT_4, ORDINAL4, COMPLEX1, SQUARE_1, RVSUM_1, RCOMP_1, PCOMPS_1, METRIC_1, TARSKI, ORDINAL2, TOPS_2, VALUED_1, MCART_1, FUNCT_2; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RVSUM_1, FUNCT_1, PARTFUN1, RELSET_1, FINSEQ_1, FUNCT_2, BINOP_1, RFINSEQ, FINSEQ_2, NAT_D, VALUED_0, STRUCT_0, TOPS_2, SQUARE_1, FUNCT_7, TOPMETR, PRE_TOPC, METRIC_1, RLVECT_1, EUCLID, PSCOMP_1, PCOMPS_1, FINSEQOP, XXREAL_0; constructors REAL_1, SQUARE_1, FINSEQOP, FINSEQ_4, FINSOP_1, RFINSEQ, NAT_D, FUNCT_7, TOPS_2, TOPMETR, PSCOMP_1, BINOP_2, FUNCSDOM, MONOID_0, PCOMPS_1, PRE_POLY; registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, EUCLID, TOPMETR, VALUED_0, FINSEQ_1, MONOID_0, RELSET_1, FUNCT_2, SQUARE_1, RVSUM_1, PRE_POLY, FUNCT_7, ORDINAL1; 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; reserve s,w1,w2 for Real; reserve n,i for Element of 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; registration let n be Nat; cluster -> REAL-valued for Element of TOP-REAL n; end; theorem :: JORDAN2B:1 for n being Nat ex f being Function of TOP-REAL n,R^1 st for p being Element of TOP-REAL n holds f.p=p/.i; theorem :: JORDAN2B:2 for i st i in Seg n holds (0.TOP-REAL n)/.i=0; theorem :: JORDAN2B:3 for r,p,i st i in Seg n holds (r*p)/.i=r*p/.i; theorem :: JORDAN2B:4 for p,i st i in Seg n holds (-p)/.i=-p/.i; theorem :: JORDAN2B:5 for p1,p2,i st i in Seg n holds (p1+p2)/.i=p1/.i+p2/.i; theorem :: JORDAN2B:6 for p1,p2,i st i in Seg n holds (p1-p2)/.i=p1/.i-p2/.i; theorem :: JORDAN2B:7 i<=n implies (0*n) | i=0*i; theorem :: JORDAN2B:8 (0*n)/^i=0*(n-'i); theorem :: JORDAN2B:9 Sum(0*i)=0; theorem :: JORDAN2B:10 for r being Real st i in Seg n holds Sum((0*n)+*(i,r))=r; theorem :: JORDAN2B:11 for q being Element of REAL n,p,i st i in Seg n & q=p holds p/.i<=|.q.| & (p/.i)^2<=|.q.|^2; begin :: 2. CONTINUITY OF PROJECTIONS theorem :: JORDAN2B:12 for s1,P,i st P = { p: s1>p/.i } & i in Seg n holds P is open; theorem :: JORDAN2B:13 for s1,P,i st P = { p: s1
0 & P=Ball(u,r) holds f"P is open)
implies f is continuous;
theorem :: JORDAN2B:17
for u being Point of RealSpace,r,u1 being Real st u1=u
holds Ball(u,r)={s:u1-r=<*|.s.|*>;
theorem :: JORDAN2B:20
for p being Element of TOP-REAL 1 ex r being Real st p=<*r*>;
notation
let r be Real;
synonym |[ r ]| for <*r*>;
end;
definition
let r be Real;
redefine func |[ r ]| -> Point of TOP-REAL 1;
end;
theorem :: JORDAN2B:21
s*|[ r ]|=|[ s*r ]|;
theorem :: JORDAN2B:22
|[ r1+r2 ]|=|[ r1 ]|+|[ r2 ]|;
theorem :: JORDAN2B:23
|[r1]|=|[r2]| implies r1=r2;
theorem :: JORDAN2B:24
for P being Subset of R^1,b being Real st P = { s: s=u
holds Ball(u,r)={<*s*>:u1-r