:: Projections in n-Dimensional Euclidean Space to Each Coordinates
:: by Roman Matuszewski and Yatsuka Nakamura
::
:: Received November 3, 1997
:: Copyright (c) 1997-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 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;
definitions TARSKI, RELAT_1;
equalities EUCLID, FINSEQ_2, RVSUM_1, SQUARE_1, STRUCT_0, VALUED_1;
expansions TARSKI;
theorems TARSKI, EUCLID, TOPMETR, TOPS_1, METRIC_1, FUNCT_1, RFINSEQ, FUNCT_2,
RELAT_1, TBSP_1, NAT_1, FINSEQ_3, FINSEQ_1, ABSVALUE, SQUARE_1, FINSEQ_2,
TOPS_2, RVSUM_1, TOPREAL3, FUNCOP_1, FINSEQ_4, FUNCT_7, SEQ_2, PSCOMP_1,
XREAL_0, XBOOLE_0, COMPLEX1, XREAL_1, XXREAL_0, FINSOP_1, PARTFUN1,
NAT_D, VALUED_1, PRE_TOPC, CARD_1;
schemes FUNCT_2;
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;
Lm1: for n,i being Nat,p being Element of TOP-REAL n ex q
being Real,g being FinSequence of REAL st g=p & q=g/.i
proof
let n,i be Nat,p be Element of TOP-REAL n;
p is Element of REAL n by EUCLID:22;
then p in { s where s is Element of REAL*: len s = n };
then consider s being Element of REAL* such that
A1: p=s and
len s=n;
s/.i=s/.i;
hence thesis by A1;
end;
registration let n be Nat;
cluster -> REAL-valued for Element of TOP-REAL n;
coherence;
end;
theorem
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
proof
let n be Nat;
defpred P[object,object] means
for p being Element of TOP-REAL n st $1=p holds $2= p/.i;
A1: for x being object st x in REAL n ex y being object st y in REAL & P[x,y]
proof
let x be object;
assume x in REAL n;
then reconsider px=x as Element of TOP-REAL n by EUCLID:22;
consider q being Real,g being FinSequence of REAL such that
A2: g=px and
q=g/.i by Lm1;
for p being Element of TOP-REAL n st x=p holds g/.i=p/.i by A2;
hence thesis;
end;
ex f being Function of REAL n,REAL st
for x being object st x in REAL n holds P[x,f.x] from FUNCT_2:sch 1(A1);
then consider f being Function of REAL n,REAL such that
A3: for x being object st x in REAL n
for p being Element of TOP-REAL n st x=p
holds f.x=p/.i;
the carrier of TOP-REAL n=REAL n by EUCLID:22;
then reconsider f1=f as Function of TOP-REAL n,R^1 by TOPMETR:17;
for p being Element of TOP-REAL n holds f1.p=p/.i
proof
let p be Element of TOP-REAL n;
p in the carrier of TOP-REAL n;
then p in REAL n by EUCLID:22;
hence thesis by A3;
end;
hence thesis;
end;
theorem
for i st i in Seg n holds (0.TOP-REAL n)/.i=0
proof
let i;
assume
A1: i in Seg n;
len (0*n)=n by CARD_1:def 7;
then
A2: i in dom (0*n) by A1,FINSEQ_1:def 3;
(0.TOP-REAL n)/.i=(0*n)/.i by EUCLID:70
.=(0*n).i by A2,PARTFUN1:def 6
.=0 by A1,FUNCOP_1:7;
hence thesis;
end;
theorem
for r,p,i st i in Seg n holds (r*p)/.i=r*p/.i
proof
let r,p,i;
reconsider w1=p as Element of REAL n by EUCLID:22;
reconsider w3=w1 as Element of n-tuples_on REAL;
reconsider w=r*p as Element of REAL n by EUCLID:22;
assume
A1: i in Seg n;
then i in Seg len w1 by CARD_1:def 7;
then
A2: i in dom w1 by FINSEQ_1:def 3;
len w=n by CARD_1:def 7;
then
A3: i in dom w by A1,FINSEQ_1:def 3;
A4: p/.i =w3.i by A2,PARTFUN1:def 6;
(r*p)/.i = w.i by A3,PARTFUN1:def 6
.= (r*w3).i
.= r*p/.i by A4,RVSUM_1:45;
hence thesis;
end;
theorem
for p,i st i in Seg n holds (-p)/.i=-p/.i
proof
let p,i;
assume
A1: i in Seg n;
reconsider w1=p as Element of REAL n by EUCLID:22;
len w1=n by CARD_1:def 7;
then
A2: i in dom w1 by A1,FINSEQ_1:def 3;
reconsider w3=w1 as Element of n-tuples_on REAL;
A3: p/.i =w3.i by A2,PARTFUN1:def 6;
reconsider w=-p as Element of REAL n by EUCLID:22;
len w=n by CARD_1:def 7;
then
i in dom w by A1,FINSEQ_1:def 3;
then (-p)/.i = w.i by PARTFUN1:def 6
.=(-w3).i
.= (-1)*p/.i by A3,RVSUM_1:45
.=-p/.i;
hence thesis;
end;
theorem
for p1,p2,i st i in Seg n holds (p1+p2)/.i=p1/.i+p2/.i
proof
let p1,p2,i;
reconsider w1=p1 as Element of REAL n by EUCLID:22;
reconsider w3=w1 as Element of n-tuples_on REAL;
reconsider w5=p2 as Element of REAL n by EUCLID:22;
reconsider w7=w5 as Element of n-tuples_on REAL;
reconsider w=p1+p2 as Element of REAL n by EUCLID:22;
assume
A1: i in Seg n;
then i in Seg len w by CARD_1:def 7;
then
A2: i in dom w by FINSEQ_1:def 3;
len w5=n by CARD_1:def 7;
then
i in dom w5 by A1,FINSEQ_1:def 3;
then A3: p2/.i =w7.i by PARTFUN1:def 6;
len w1=n by CARD_1:def 7;
then
i in dom w1 by A1,FINSEQ_1:def 3;
then A4: p1/.i =w3.i by PARTFUN1:def 6;
(p1+p2)/.i = w.i by A2,PARTFUN1:def 6
.= (w3 + w7).i
.=p1/.i+p2/.i by A4,A3,RVSUM_1:11;
hence thesis;
end;
theorem Th6:
for p1,p2,i st i in Seg n holds (p1-p2)/.i=p1/.i-p2/.i
proof
let p1,p2,i;
reconsider w1=p1 as Element of REAL n by EUCLID:22;
reconsider w3=w1 as Element of n-tuples_on REAL;
reconsider w5=p2 as Element of REAL n by EUCLID:22;
reconsider w7=w5 as Element of n-tuples_on REAL;
reconsider w=p1-p2 as Element of REAL n by EUCLID:22;
assume
A1: i in Seg n;
then i in Seg len w5 by CARD_1:def 7;
then
A2: i in dom w5 by FINSEQ_1:def 3;
len w1=n by CARD_1:def 7;
then
i in dom w1 by A1,FINSEQ_1:def 3;
then A3: p1/.i =w3.i by PARTFUN1:def 6;
len w=n by CARD_1:def 7;
then
A4: i in dom w by A1,FINSEQ_1:def 3;
A5: p2/.i =w7.i by A2,PARTFUN1:def 6;
(p1-p2)/.i = w.i by A4,PARTFUN1:def 6
.= (w3 - w7).i
.=p1/.i-p2/.i by A3,A5,RVSUM_1:27;
hence thesis;
end;
theorem Th7:
i<=n implies (0*n) | i=0*i
proof
assume
A1: i<=n;
then i<=len (0*n) by CARD_1:def 7;
then
A2: len ((0*n) | i)=i by FINSEQ_1:59;
A3: for j be Nat st 1<=j & j<=i holds ((0*n) | i).j=(0*i).j
proof
let j be Nat;
assume that
A4: 1<=j and
A5: j<=i;
j<=n by A1,A5,XXREAL_0:2;
then
A6: j in Seg n by A4,FINSEQ_1:1;
A7: ((0*n) | i).j=(n|->0).j by A5,FINSEQ_3:112
.=0 by A6,FUNCOP_1:7;
j in Seg i by A4,A5,FINSEQ_1:1;
hence thesis by A7,FUNCOP_1:7;
end;
i=len (0*i) by CARD_1:def 7;
hence thesis by A2,A3,FINSEQ_1:14;
end;
theorem Th8:
(0*n)/^i=0*(n-'i)
proof
A1: len ((0*n)/^i) = len (0*n)-'i by RFINSEQ:29
.=n-'i by CARD_1:def 7;
A2: n=len (0*n) by CARD_1:def 7;
A3: for j be Nat st 1<=j & j<=n-'i holds ((0*n)/^i).j=(0*(n-'i)).j
proof
let j be Nat;
assume that
A4: 1<=j and
A5: j<=n-'i;
now
assume n<i;
then n-i<i-i by XREAL_1:9;
hence contradiction by A4,A5,XREAL_0:def 2;
end;
then n-'i=n-i by XREAL_1:233;
then
A6: j+i<=n-i+i by A5,XREAL_1:6;
1<=j+i by A4,NAT_1:12;
then
A7: j+i in Seg n by A6,FINSEQ_1:1;
A8: j in Seg (n-'i) by A4,A5,FINSEQ_1:1;
then
A9: j in dom ((0*n)/^i) by A1,FINSEQ_1:def 3;
now
per cases;
case
i<=len (0*n);
hence ((0*n)/^i).j=(n |-> (0 qua Real)).(j+i) by A9,RFINSEQ:def 1
.=0 by A7,FUNCOP_1:7
.= (0*(n-'i)).j by A8,FUNCOP_1:7;
end;
case
A10: i>len (0*n);
then i-i>n-i by A2,XREAL_1:9;
then
A11: n-'i=0 by XREAL_0:def 2;
((0*n)/^i).j = (<*>REAL).j by A10,RFINSEQ:def 1;
hence thesis by A11;
end;
end;
hence thesis;
end;
n-'i=len (0*(n-'i)) by CARD_1:def 7;
hence thesis by A1,A3,FINSEQ_1:14;
end;
theorem Th9:
Sum(0*i)=0
proof
thus Sum(0*i) = i*0 by RVSUM_1:80
.= 0;
end;
theorem Th10:
for r being Real st i in Seg n holds Sum((0*n)+*(i,r))=r
proof
let r be Real;
A1: len(0*n) = n by CARD_1:def 7;
reconsider w=0*n as FinSequence of REAL;
assume
A2: i in Seg n;
then
A3: i<=n by FINSEQ_1:1;
reconsider r as Element of REAL by XREAL_0:def 1;
1<=i by A2,FINSEQ_1:1;
then i in dom (0*n) by A3,A1,FINSEQ_3:25;
then Sum( w+*(i,r))=Sum((w | (i-'1))^<*r*>^(w/^i)) by FUNCT_7:98
.= Sum(((0*n) | (i-'1))^<*r*>)+Sum((0*n)/^i) by RVSUM_1:75
.= Sum((0*n) | (i-'1))+Sum<*r*>+Sum((0*n)/^i) by RVSUM_1:75
.= Sum((0*n) | (i-'1))+r+Sum((0*n)/^i) by FINSOP_1:11
.= Sum(0*(i-'1))+r+Sum((0*n)/^i) by A3,Th7,NAT_D:44
.= 0+r+Sum((0*n)/^i) by Th9
.= 0+r+Sum(0*(n-'i)) by Th8
.= r by Th9;
hence thesis;
end;
theorem Th11:
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
proof
let q be Element of REAL n,p,i;
assume that
A1: i in Seg n and
A2: q=p;
reconsider pd = (p/.i)^2 as Element of REAL by XREAL_0:def 1;
A3: Sum( (0*n)+*(i,pd))= pd by A1,Th10;
len (0*n)=n by CARD_1:def 7;
then len ((0*n)+*(i,pd))=n by FUNCT_7:97;
then reconsider
w1= (0*n)+*(i,pd) as Element of n-tuples_on REAL by FINSEQ_2:92;
A4: len w1=n by CARD_1:def 7;
reconsider w2=sqr q as Element of n-tuples_on REAL;
A5: Sum sqr q>=0 by RVSUM_1:86;
A6: len q=n by CARD_1:def 7;
A7: for j be Nat st j in Seg n holds w1.j<=w2.j
proof
let j be Nat such that
A8: j in Seg n;
set r1=w1.j, r2=w2.j;
per cases;
suppose
A9: j=i;
then j in dom q by A1,A6,FINSEQ_1:def 3;
then
A10: q/.j=q.j by PARTFUN1:def 6;
A11: dom 0*n=Seg len 0*n by FINSEQ_1:def 3
.=Seg n by CARD_1:def 7;
i in dom w1 by A1,A4,FINSEQ_1:def 3;
then r1=w1/.i by A9,PARTFUN1:def 6
.=(q/.i)^2 by A2,A1,A11,FUNCT_7:36;
hence thesis by A9,A10,VALUED_1:11;
end;
suppose
A12: j<>i;
A13: dom 0*n=Seg len 0*n by FINSEQ_1:def 3
.=Seg n by CARD_1:def 7;
dom q=Seg n by A6,FINSEQ_1:def 3;
then q/.j=q.j by A8,PARTFUN1:def 6;
then
A14: r2=(q/.j)^2 by VALUED_1:11;
j in dom w1 by A4,A8,FINSEQ_1:def 3;
then r1=w1/.j by PARTFUN1:def 6
.=(0*n)/.j by A8,A12,A13,FUNCT_7:37
.=(n|->0).j by A8,A13,PARTFUN1:def 6
.=0 by A8,FUNCOP_1:7;
hence thesis by A14,XREAL_1:63;
end;
end;
then Sum w1<=Sum w2 by RVSUM_1:82;
then 0<=(p/.i)^2 & (p/.i)^2<=(sqrt Sum sqr q)^2 by A5,A3,SQUARE_1:def 2
,XREAL_1:63;
then sqrt((p/.i)^2)<=sqrt((sqrt Sum sqr q)^2) by SQUARE_1:26;
then |.|.p/.i.|.|<=sqrt((sqrt Sum sqr q)^2) by COMPLEX1:72;
then 0<=|.q.| & |.p/.i.|<= |.sqrt Sum sqr q.| by COMPLEX1:72;
then
A15: |.p/.i.|<=sqrt Sum sqr q by ABSVALUE:def 1;
A16: p/.i<=|.p/.i.| by ABSVALUE:4;
|.q.|^2=Sum sqr q by A5,SQUARE_1:def 2;
hence thesis by A7,A3,A15,A16,RVSUM_1:82,XXREAL_0:2;
end;
begin :: 2. CONTINUITY OF PROJECTIONS
theorem Th12:
for s1,P,i st P = { p: s1>p/.i } & i in Seg n holds P is open
proof
let s1,P,i such that
A1: P= { p:s1>p/.i } & i in Seg n;
reconsider s1 as Real;
A2: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider PP=P as Subset of TopSpaceMetr Euclid n;
for pe being Point of Euclid n st pe in P ex r be Real st r>0 &
Ball(pe,r) c= P
proof
let pe be Point of Euclid n;
assume pe in P;
then consider p such that
A3: p=pe and
A4: s1>p/.i by A1;
set r=(s1-p/.i)/2;
A5: s1-p/.i>0 by A4,XREAL_1:50;
Ball(pe,r) c= P
proof
let x be object;
assume x in Ball(pe,r);
then x in {q where q is Element of Euclid n:dist(pe,q)<r} by METRIC_1:17;
then consider q being Element of Euclid n such that
A6: q=x and
A7: dist(pe,q)<r;
reconsider ppe=pe, pq=q as Point of TOP-REAL n by TOPREAL3:8;
reconsider pen=ppe, pqn=pq as Element of REAL n;
(Pitag_dist n).(q,pe)=dist(q,pe) by METRIC_1:def 1;
then
A8: |.pqn-pen.|<r by A7,EUCLID:def 6;
reconsider q = pq-ppe as Element of REAL n by EUCLID:22;
(pq-ppe)/.i <= |.q.| by A1,Th11;
then (pq-ppe)/.i <= |.pqn-pen.|;
then (pq-ppe)/.i <r by A8,XXREAL_0:2;
then pq/.i-ppe/.i < r by A1,Th6;
then
A9: p/.i+(s1-p/.i)/2 > pq/.i by A3,XREAL_1:19;
p/.i+(s1-p/.i)/2 =s1-r;
then s1> p/.i+(s1-p/.i)/2 by A5,XREAL_1:44,139;
then s1>pq/.i by A9,XXREAL_0:2;
hence thesis by A1,A6;
end;
hence thesis by A5,XREAL_1:139;
end;
then PP is open by TOPMETR:15;
hence thesis by A2,PRE_TOPC:30;
end;
theorem Th13:
for s1,P,i st P = { p: s1<p/.i } & i in Seg n holds P is open
proof
let s1,P,i such that
A1: P= { p:s1<p/.i } & i in Seg n;
reconsider s1 as Real;
A2: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider PP=P as Subset of TopSpaceMetr Euclid n;
for pe being Point of Euclid n st pe in P ex r be Real st r>0 &
Ball(pe,r) c= P
proof
let pe be Point of Euclid n;
assume pe in P;
then consider p such that
A3: p=pe and
A4: s1<p/.i by A1;
set r=(p/.i-s1)/2;
A5: p/.i-s1>0 by A4,XREAL_1:50;
Ball(pe,r) c= P
proof
let x be object;
assume x in Ball(pe,r);
then x in {q where q is Element of Euclid n:dist(pe,q)<r} by METRIC_1:17;
then consider q being Element of Euclid n such that
A6: q=x and
A7: dist(pe,q)<r;
reconsider ppe=pe, pq=q as Point of TOP-REAL n by TOPREAL3:8;
reconsider pen=ppe, pqn=pq as Element of REAL n;
(Pitag_dist n).(pe,q)=dist(pe,q) by METRIC_1:def 1;
then
A8: |.pen-pqn.|<r by A7,EUCLID:def 6;
reconsider qq = ppe-pq as Element of REAL n by EUCLID:22;
(ppe-pq)/.i <= |.qq.| by A1,Th11;
then (ppe-pq)/.i <= |.pen-pqn.|;
then (ppe-pq)/.i <r by A8,XXREAL_0:2;
then ppe/.i-pq/.i < r by A1,Th6;
then ppe/.i-pq/.i+pq/.i < r+pq/.i by XREAL_1:6;
then
A9: ppe/.i-r < pq/.i+r-r by XREAL_1:9;
p/.i-(p/.i-s1)/2 =s1+r;
then s1< p/.i-(p/.i-s1)/2 by A5,XREAL_1:29,139;
then s1<pq/.i by A3,A9,XXREAL_0:2;
hence thesis by A1,A6;
end;
hence thesis by A5,XREAL_1:139;
end;
then PP is open by TOPMETR:15;
hence thesis by A2,PRE_TOPC:30;
end;
theorem Th14:
for P being Subset of TOP-REAL n,a,b being Real, i st P =
{ p where p is Element of TOP-REAL n: a<p/.i & p/.i<b } & i in Seg n
holds P is open
proof
let P be Subset of TOP-REAL n,a,b be Real,i;
assume that
A1: P = { p where p is Element of TOP-REAL n: a<p/.i & p/.i<b } and
A2: i in Seg n;
A3: P = { p1 :a<p1/.i} /\ {p2:p2/.i<b }
proof
A4: { p1 :a<p1/.i} /\ {p2:p2/.i<b } c= P
proof
let x be object;
assume
A5: x in { p1 :a<p1/.i} /\ {p2:p2/.i<b };
then x in {p2:p2/.i<b } by XBOOLE_0:def 4;
then
A6: ex p2 st x=p2 & p2/.i<b;
x in { p1 :a<p1/.i} by A5,XBOOLE_0:def 4;
then ex p1 st x=p1 & a<p1/.i;
hence thesis by A1,A6;
end;
P c= { p1 :a<p1/.i} /\ {p2:p2/.i<b }
proof
let x be object;
assume x in P;
then
A7: ex p3 st p3=x & a<p3/.i & p3/.i<b by A1;
then
A8: x in {p2:p2/.i<b };
x in { p1 :a<p1/.i} by A7;
hence thesis by A8,XBOOLE_0:def 4;
end;
hence thesis by A4,XBOOLE_0:def 10;
end;
{ p:p/.i<b} c= the carrier of TOP-REAL n
proof
let x be object;
assume x in { p:p/.i<b};
then ex p st x= p & p/.i<b;
hence thesis;
end;
then reconsider P2={ p:p/.i<b} as Subset of TOP-REAL n;
{ p:a<p/.i} c= the carrier of TOP-REAL n
proof
let x be object;
assume x in { p:a<p/.i};
then ex p st x= p & a<p/.i;
hence thesis;
end;
then reconsider P1={ p:a<p/.i} as Subset of TOP-REAL n;
P1 is open & P2 is open by A2,Th12,Th13;
hence thesis by A3,TOPS_1:11;
end;
theorem Th15:
for a,b being Real,f being Function of TOP-REAL n,R^1,i
st (for p being Element of TOP-REAL n holds f.p=p/.i) holds f"({s:a<s & s<
b})={p where p is Element of TOP-REAL n: a<p/.i & p/.i<b}
proof
let a,b be Real, f be Function of TOP-REAL n,R^1,i;
assume
A1: for p being Element of TOP-REAL n holds f.p=p/.i;
thus f"({s:a<s & s<b})={p where p is Element of TOP-REAL n: a<p/.i & p/.i<b}
proof
A2: f"({s:a<s & s<b}) c= {p where p is Element of TOP-REAL n: a<p/.i & p/.i<b}
proof
let x be object;
assume
A3: x in f"({s:a<s & s<b});
then reconsider px=x as Element of (TOP-REAL n);
f.x in {s:a<s & s<b} by A3,FUNCT_1:def 7;
then
A4: ex s st s=f.x & a<s & s<b;
f.px=px/.i by A1;
hence thesis by A4;
end;
A5: dom f =the carrier of (TOP-REAL n) by FUNCT_2:def 1;
{p where p is Element of TOP-REAL n: a<p/.i & p/.i<b} c= f"( {s:a<s & s<b})
proof
let x be object;
assume x in {p where p is Element of TOP-REAL n: a<p/.i & p/.i<b};
then consider p being Element of TOP-REAL n such that
A6: x=p and
A7: a<p/.i & p/.i<b;
f.x=p/.i by A1,A6;
then f.x in {s:a<s & s<b} by A7;
hence thesis by A5,A6,FUNCT_1:def 7;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
end;
theorem Th16:
for M being non empty MetrSpace,f being Function of X,
TopSpaceMetr(M) holds (for r being Real,u being Element
of M,P being Subset of TopSpaceMetr(M) st r>0 & P=Ball(u,r) holds f"P is open)
implies f is continuous
proof
let M be non empty MetrSpace,f be Function of X,TopSpaceMetr(M);
assume
A1: for r being Real, u being Element of M, P being Subset of
TopSpaceMetr(M) st r>0 & P=Ball(u,r) holds f"P is open;
A2: for P1 being Subset of TopSpaceMetr(M) st P1 is open holds f"P1 is open
proof
let P1 be Subset of TopSpaceMetr(M);
assume
A3: P1 is open;
for x holds x in f"P1 iff ex Q being Subset of X st Q is open & Q c= f
"P1 & x in Q
proof
let x;
now
assume
A4: x in f"P1;
then
A5: x in dom f by FUNCT_1:def 7;
A6: f.x in P1 by A4,FUNCT_1:def 7;
then reconsider u=f.x as Element of M by TOPMETR:12;
consider r be Real such that
A7: r>0 and
A8: Ball(u,r) c= P1 by A3,A6,TOPMETR:15;
reconsider r as Real;
reconsider PB=Ball(u,r) as Subset of TopSpaceMetr(M) by TOPMETR:12;
A9: f"PB c= f"P1 by A8,RELAT_1:143;
f.x in Ball(u,r) by A7,TBSP_1:11;
then x in f"(Ball(u,r)) by A5,FUNCT_1:def 7;
hence ex Q being Subset of X st Q is open & Q c= f"P1 & x in Q by A1,A7
,A9;
end;
hence thesis;
end;
hence thesis by TOPS_1:25;
end;
[#]TopSpaceMetr M <> {};
hence thesis by A2,TOPS_2:43;
end;
theorem Th17:
for u being Point of RealSpace,r,u1 being Real st u1=u
holds Ball(u,r)={s:u1-r<s & s<u1+r}
proof
let u be Point of RealSpace,r,u1 be Real;
assume
A1: u1=u;
{s:u1-r<s & s<u1+r}={q where q is Element of RealSpace: dist(u,q)<r}
proof
A2: {q where q is Element of RealSpace: dist(u,q)<r} c= {s:u1-r<s & s<u1+ r}
proof
let x be object;
assume x in {q where q is Element of RealSpace: dist(u,q)<r};
then consider q being Element of RealSpace such that
A3: x=q and
A4: dist(u,q)<r;
reconsider s1=q as Real;
A5: |.u1-s1.| < r by A1,A4,TOPMETR:11;
then u1-s1 < r by SEQ_2:1;
then u1-s1+s1<r+s1 by XREAL_1:6;
then
A6: u1-r<r+s1-r by XREAL_1:9;
-r < u1-s1 by A5,SEQ_2:1;
then -r+s1 < u1-s1+s1 by XREAL_1:6;
then s1-r+r < u1+r by XREAL_1:6;
hence thesis by A3,A6;
end;
{s:u1-r<s & s<u1+r} c= {q where q is Element of RealSpace:dist(u,q)<r}
proof
let x be object;
assume x in {s:u1-r<s & s<u1+r};
then consider s such that
A7: x=s and
A8: u1-r<s and
A9: s<u1+r;
s in REAL by XREAL_0:def 1;
then reconsider q1=s as Point of RealSpace by METRIC_1:def 13;
s-r<u1+r-r by A9,XREAL_1:9;
then
A10: s+-r-s<u1-s by XREAL_1:9;
u1-r+r<s+r by A8,XREAL_1:6;
then u1-s<s+r-s by XREAL_1:9;
then |.u1-s.| < r by A10,SEQ_2:1;
then dist(u,q1)<r by A1,TOPMETR:11;
hence thesis by A7;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
hence thesis by METRIC_1:17;
end;
theorem Th18:
for f being Function of TOP-REAL n,R^1,i st i in Seg n & (for p
being Element of TOP-REAL n holds f.p=p/.i) holds f is continuous
proof
let f be Function of TOP-REAL n,R^1,i;
assume that
A1: i in Seg n and
A2: for p being Element of TOP-REAL n holds f.p=p/.i;
reconsider f1=f as Function of TOP-REAL n,TopSpaceMetr(RealSpace) by
TOPMETR:def 6;
for r being Real,u being Element of RealSpace,P
being Subset of TopSpaceMetr(RealSpace) st r>0 & P=Ball(u,r) holds f1"P is open
proof
let r be Real, u be Element of RealSpace, P be
Subset of TopSpaceMetr RealSpace;
assume that
r>0 and
A3: P=Ball(u,r);
reconsider u1=u as Real;
Ball(u,r)={s:u1-r<s & s<u1+r} by Th17;
then f"(Ball(u,r))={p where p is Element of TOP-REAL n: u1-r<p/.i &
p/.i<u1+r} by A2,Th15;
hence thesis by A1,A3,Th14;
end;
hence thesis by Th16,TOPMETR:def 6;
end;
begin ::3. 1-DIMENSIONAL AND 2-DIMENSIONAL CASES
theorem
for s being Real holds abs <*s*>=<*|.s.|*>
proof
let s be Real;
reconsider s as Element of REAL by XREAL_0:def 1;
rng <*s*> c= dom absreal
proof
let x be object;
assume x in rng <*s*>;
then x in {s} by FINSEQ_1:38;
then
A1: x=s by TARSKI:def 1;
dom absreal =REAL by FUNCT_2:def 1;
hence thesis by A1;
end;
then dom <*s*>=dom (absreal*<*s*>) by RELAT_1:27;
then Seg 1=dom (abs <*s*>) by FINSEQ_1:def 8;
then
A2: len (abs <*s*>)=1 by FINSEQ_1:def 3;
A3: len <*|.s.|*>=1 by FINSEQ_1:39;
for j be Nat st 1<=j & j<=len <*|.s.|*> holds <*|.s.|*>.j=(abs <*s*>) .j
proof
let j be Nat;
A4: <*s*>.1=s & <*s*> is Element of REAL 1 by FINSEQ_2:98;
assume 1<=j & j<=len <*|.s.|*>;
then
A5: j=1 by A3,XXREAL_0:1;
thus thesis by A5,A4,VALUED_1:18;
end;
hence thesis by A2,A3,FINSEQ_1:14;
end;
theorem Th20:
for p being Element of TOP-REAL 1 ex r being Real st p=<*r*>
proof
let p be Element of TOP-REAL 1;
1-tuples_on REAL = REAL 1;
then reconsider p9=p as Element of 1-tuples_on REAL by EUCLID:22;
ex r be Element of REAL st p9=<*r*> by FINSEQ_2:97;
hence thesis;
end;
notation
let r be Real;
synonym |[ r ]| for <*r*>;
end;
definition
let r be Real;
redefine func |[ r ]| -> Point of TOP-REAL 1; :: redefines |[ (JORDAN2B, synonym) → <* (FINSEQ_1, definition)
coherence
proof
reconsider r as Element of REAL by XREAL_0:def 1;
<*r*> in REAL 1 by FINSEQ_2:98;
hence thesis by EUCLID:22;
end;
end;
theorem
s*|[ r ]|=|[ s*r ]| by RVSUM_1:47;
theorem
|[ r1+r2 ]|=|[ r1 ]|+|[ r2 ]| by RVSUM_1:13;
theorem
|[r1]|=|[r2]| implies r1=r2 by FINSEQ_1:76;
theorem Th24:
for P being Subset of R^1,b being Real st P = { s: s<b }
holds P is open
proof
let P be Subset of R^1,b be Real;
assume
A1: P = { s: s<b };
for c being Point of RealSpace st c in P ex r being Real st r > 0
& Ball(c,r) c= P
proof
let c be Point of RealSpace;
reconsider n = c as Element of REAL by METRIC_1:def 13;
reconsider r = b-n as Element of REAL by XREAL_0:def 1;
assume c in P;
then
A2: ex s st s=n & s<b by A1;
take r;
now
let x be object;
assume
A3: x in Ball(c,r);
then reconsider t = x as Element of REAL by METRIC_1:def 13;
reconsider u = x as Point of RealSpace by A3;
Ball(c,r) = {q where q is Element of RealSpace :dist(c,q)<r} by
METRIC_1:17;
then ex v being Element of RealSpace st v = u & dist(c,v)<r by A3;
then (real_dist).(t,n) < r by METRIC_1:def 1,def 13;
then
A4: |. t - n .| < r by METRIC_1:def 12;
t - n <= |. t - n .| by ABSVALUE:4;
then t - n < b - n by A4,XXREAL_0:2;
then t < b by XREAL_1:9;
hence x in P by A1;
end;
hence thesis by A2,XREAL_1:50;
end;
hence thesis by TOPMETR:15,def 6;
end;
theorem Th25:
for P being Subset of R^1,a being Real st P = { s: a<s }
holds P is open
proof
let P be Subset of R^1,a be Real;
assume
A1: P = { s: a<s };
for c being Point of RealSpace st c in P ex r being Real st r > 0
& Ball(c,r) c= P
proof
let c be Point of RealSpace;
reconsider n = c as Element of REAL by METRIC_1:def 13;
reconsider r = n-a as Real;
assume c in P;
then
A2: ex s st s=n & a<s by A1;
take r;
now
let x be object;
assume
A3: x in Ball(c,r);
then reconsider t = x as Element of REAL by METRIC_1:def 13;
reconsider u = x as Point of RealSpace by A3;
Ball(c,r) = {q where q is Element of RealSpace :dist(c,q)<r} by
METRIC_1:17;
then ex v being Element of RealSpace st v = u & dist(c,v)<r by A3;
then (real_dist).(n,t) < r by METRIC_1:def 1,def 13;
then
A4: |. n - t .| < r by METRIC_1:def 12;
n - t <= |. n - t .| by ABSVALUE:4;
then n - t < n - a by A4,XXREAL_0:2;
then a<t by XREAL_1:10;
hence x in P by A1;
end;
hence thesis by A2,XREAL_1:50;
end;
hence thesis by TOPMETR:15,def 6;
end;
theorem Th26:
for P being Subset of R^1,a,b being Real st P = { s: a<s
& s<b } holds P is open
proof
let P be Subset of R^1,a,b be Real;
{ w1:a<w1} c= the carrier of R^1
proof
let x be object;
assume x in { w1:a<w1};
then consider r1 be Real such that
A1: x= r1 & a<r1;
r1 in REAL by XREAL_0:def 1;
hence thesis by TOPMETR:17,A1;
end;
then reconsider P1={w1:a<w1} as Subset of R^1;
{w2:w2<b} c= the carrier of R^1
proof
let x be object;
assume x in {w2:w2<b};
then consider r2 be Real such that
A2: x= r2 & r2<b;
r2 in REAL by XREAL_0:def 1;
hence thesis by TOPMETR:17,A2;
end;
then reconsider P2={w2:w2<b} as Subset of R^1;
assume
A3: P = { s: a<s & s<b };
A4: P = { w1: a<w1} /\ {w2: w2<b}
proof
A5: { w1 :a<w1} /\ {w2:w2<b } c= P
proof
let x be object;
assume
A6: x in { w1 :a<w1} /\ {w2:w2<b };
then x in {w2:w2<b } by XBOOLE_0:def 4;
then
A7: ex r2 be Real st x=r2 & r2<b;
x in { w1 :a<w1} by A6,XBOOLE_0:def 4;
then ex r1 be Real st x=r1 & a<r1;
hence thesis by A3,A7;
end;
P c= {w1: a<w1} /\ {w2: w2<b }
proof
let x be object;
assume x in P;
then
A8: ex s st s=x & a<s & s<b by A3;
then
A9: x in {w2:w2<b };
x in { w1 :a<w1} by A8;
hence thesis by A9,XBOOLE_0:def 4;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
P1 is open & P2 is open by Th24,Th25;
hence thesis by A4,TOPS_1:11;
end;
theorem Th27:
for u being Point of Euclid 1,r,u1 being Real st <*u1*>=u
holds Ball(u,r)={<*s*>:u1-r<s & s<u1+r}
proof
let u be Point of Euclid 1,r,u1 be Real;
assume
A1: <*u1*>=u;
reconsider u1 as Element of REAL by XREAL_0:def 1;
{<*s*>:u1-r<s & s<u1+r} ={q where q is Element of Euclid 1: dist(u,q)<r}
proof
A2: {q where q is Element of Euclid 1: dist(u,q)<r} c= {<*s*>:u1-r<s & s< u1+r}
proof
let x be object;
assume x in {q where q is Element of Euclid 1: dist(u,q)<r};
then consider q being Element of Euclid 1 such that
A3: x=q and
A4: dist(u,q)<r;
reconsider eu=u, eq=q as Element of REAL 1;
q is Tuple of 1,REAL by FINSEQ_2:131;
then consider s1 be Element of REAL such that
A5: q=<*s1*> by FINSEQ_2:97;
reconsider us = (u1-s1)^2 as Element of REAL by XREAL_0:def 1;
<*u1*>-<*s1*> =<*u1-s1*> by RVSUM_1:29;
then sqr (<*u1*>-<*s1*>)=<*us*> by RVSUM_1:55;
then Sum sqr (<*u1*>-<*s1*>)=(u1-s1)^2 by FINSOP_1:11;
then
A6: sqrt Sum sqr (<*u1*>-<*s1*>)=|.u1-s1.| by COMPLEX1:72;
(Pitag_dist 1).(eu,eq)<r by A4,METRIC_1:def 1;
then
A7: |.<*u1*>-<*s1*>.| < r by A1,A5,EUCLID:def 6;
then u1-s1 < r by A6,SEQ_2:1;
then u1-s1+s1<r+s1 by XREAL_1:6;
then
A8: u1-r<r+s1-r by XREAL_1:9;
-r < u1-s1 by A7,A6,SEQ_2:1;
then -r+s1 < u1-s1+s1 by XREAL_1:6;
then s1-r+r < u1+r by XREAL_1:6;
hence thesis by A3,A5,A8;
end;
{<*s*>:u1-r<s & s<u1+r} c= {q where q is Element of Euclid 1: dist(u,q )<r}
proof
reconsider eu1=<*u1*> as Element of REAL 1 by FINSEQ_2:98;
let x be object;
assume x in {<*s*>:u1-r<s & s<u1+r};
then consider s such that
A9: x=<*s*> and
A10: u1-r<s and
A11: s<u1+r;
s-r<u1+r-r by A11,XREAL_1:9;
then
A12: s+-r-s<u1-s by XREAL_1:9;
reconsider ss=s as Element of REAL by XREAL_0:def 1;
reconsider es=<*ss*> as Element of REAL 1 by FINSEQ_2:98;
reconsider q1=<*ss*> as Element of Euclid 1 by FINSEQ_2:98;
reconsider uss = (u1-ss)^2 as Element of REAL by XREAL_0:def 1;
<*u1*>-<*ss*> =<*u1-ss*> by RVSUM_1:29;
then sqr (<*u1*>-<*ss*>) =<*uss*> by RVSUM_1:55;
then
A13: Sum sqr (<*u1*>-<*ss*>)=(u1-s)^2 by FINSOP_1:11;
u1-r+r<s+r by A10,XREAL_1:6;
then u1-s<s+r-s by XREAL_1:9;
then |.u1-s.| < r by A12,SEQ_2:1;
then |.<*u1*>-<*ss*>.| < r by A13,COMPLEX1:72;
then
(the distance of Euclid 1).(u,q1)=dist(u,q1) & (Pitag_dist 1).(eu1,
es)<r by EUCLID:def 6,METRIC_1:def 1;
hence thesis by A1,A9;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
hence thesis by METRIC_1:17;
end;
theorem
for f being Function of TOP-REAL 1,R^1 st (for p being Element of
TOP-REAL 1 holds f.p=p/.1) holds f is being_homeomorphism
proof
let f be Function of TOP-REAL 1,R^1;
assume
A1: for p being Element of TOP-REAL 1 holds f.p=p/.1;
A2: dom f=the carrier of TOP-REAL 1 by FUNCT_2:def 1;
REAL c= rng f
proof
let x be object;
assume x in REAL;
then reconsider r=x as Element of REAL;
A3: 1<=len <*r*> by FINSEQ_1:40;
f.(|[r]|)=|[r]|/.1 by A1
.=<*r*>.1 by A3,FINSEQ_4:15
.=x;
hence thesis by A2,FUNCT_1:def 3;
end;
then
A4: [#](TOP-REAL 1) = the carrier of TOP-REAL 1 & rng f=[#](R^1) by TOPMETR:17
,XBOOLE_0:def 10;
A5: the TopStruct of TOP-REAL 1 =TopSpaceMetr Euclid 1 by EUCLID:def 8;
then reconsider ff = f/" as Function of R^1,TopSpaceMetr Euclid 1;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be object;
assume that
A6: x1 in dom f & x2 in dom f and
A7: f.x1 = f.x2;
reconsider p1=x1, p2=x2 as Element of TOP-REAL 1 by A6;
consider r1 be Real such that
A8: p1=<*r1*> by Th20;
A9: 1<=len <*r1*> by FINSEQ_1:40;
reconsider r1 as Element of REAL by XREAL_0:def 1;
consider r2 being Real such that
A10: p2=<*r2*> by Th20;
A11: 1<=len <*r2*> by FINSEQ_1:40;
reconsider r2 as Element of REAL by XREAL_0:def 1;
A12: f.p2=p2/.1 by A1
.=<*r2*>.1 by A10,A11,FINSEQ_4:15
.=r2;
f.(p1)=p1/.1 by A1
.=<*r1*>.1 by A8,A9,FINSEQ_4:15
.=r1;
hence thesis by A7,A8,A10,A12;
end;
then
A13: f is one-to-one by FUNCT_1:def 4;
A14: f/" is continuous
proof
the TopStruct of TOP-REAL 1 =TopSpaceMetr(Euclid 1) by EUCLID:def 8;
then reconsider g=f/" as Function of R^1,TopSpaceMetr(Euclid 1);
reconsider g1=g as Function of the carrier of R^1, the carrier of TOP-REAL
1;
the carrier of R^1 c= rng f
proof
let z1 be object;
assume z1 in the carrier of R^1;
then reconsider r1=z1 as Element of REAL by TOPMETR:17;
<*r1*> in REAL 1 by FINSEQ_2:98;
then reconsider q=<*r1*> as Element of TOP-REAL 1 by EUCLID:22;
f.q=q/.1 by A1
.=z1 by FINSEQ_4:16;
hence thesis by A2,FUNCT_1:def 3;
end;
then
A15: rng f= the carrier of R^1 by XBOOLE_0:def 10;
for r being Real,u being Element of Euclid 1,P
being Subset of the carrier of TopSpaceMetr(Euclid 1) st r>0 & P=Ball(u,r)
holds g"P is open
proof
reconsider f1=f as Function of the carrier of TOP-REAL 1,the carrier of
R^1;
let r be Real,u be Element of Euclid 1,P be Subset
of the carrier of TopSpaceMetr(Euclid 1);
assume that
r>0 and
A16: P=Ball(u,r);
u is Tuple of 1,REAL by FINSEQ_2:131;
then consider s1 be Element of REAL such that
A17: u=<*s1*> by FINSEQ_2:97;
dom f1=the carrier of TOP-REAL 1 by FUNCT_2:def 1;
then
A18: dom f1=REAL 1 by EUCLID:22;
A19: Ball(u,r)={<*s*>:s1-r<s & s<s1+r} by A17,Th27;
A20: f1.:(Ball(u,r))={w1:s1-r<w1 & w1<s1+r}
proof
A21: f1.:(Ball(u,r))c={w1:s1-r<w1 & w1<s1+r}
proof
let z be object;
assume z in f1.:(Ball(u,r));
then consider x1 being object such that
x1 in dom f1 and
A22: x1 in Ball(u,r) and
A23: z=f1.x1 by FUNCT_1:def 6;
consider s such that
A24: <*s*>=x1 and
A25: s1-r<s & s<s1+r by A19,A22;
reconsider ss=s as Element of REAL by XREAL_0:def 1;
<*ss*> in REAL 1 by FINSEQ_2:98;
then reconsider q=<*s*> as Element of TOP-REAL 1 by EUCLID:22;
A26: len <*s*>=1 by FINSEQ_1:40;
z=q/.1 by A1,A23,A24
.=<*ss*>.1 by A26,FINSEQ_4:15
.=s;
hence thesis by A25;
end;
{w1:s1-r<w1 & w1<s1+r} c= f1.:(Ball(u,r))
proof
let z be object;
assume z in {w1:s1-r<w1 & w1<s1+r};
then consider r1 be Real such that
A27: z=r1 and
A28: s1-r<r1 & r1<s1+r;
reconsider rr=r1 as Element of REAL by XREAL_0:def 1;
<*rr*> in REAL 1 by FINSEQ_2:98;
then reconsider q=<*rr*> as Element of TOP-REAL 1 by EUCLID:22;
Ball(u,r)={<*s*>:s1-r<s & s<s1+r} by A17,Th27;
then
A29: <*r1*> in Ball(u,r) by A28;
z = q/.1 by A27,FINSEQ_4:16
.=f1.<*r1*> by A1;
hence thesis by A18,A29,FUNCT_1:def 6;
end;
hence thesis by A21,XBOOLE_0:def 10;
end;
f1 is onto by A15,FUNCT_2:def 3;
then g1=(f1 qua Function)" by A13,TOPS_2:def 4;
then g1"(Ball(u,r))={w1:s1-r<w1 & w1<s1+r} by A13,A20,FUNCT_1:84;
hence thesis by A16,Th26;
end;
then ff is continuous by Th16;
hence f/" is continuous by A5,PRE_TOPC:33;
end;
1 in Seg 1 by FINSEQ_1:1;
then f is continuous by A1,Th18;
hence thesis by A2,A4,A13,A14,TOPS_2:def 5;
end;
theorem Th29:
for p being Element of TOP-REAL 2 holds p/.1=p`1 & p/.2=p`2
proof
let p be Element of TOP-REAL 2;
reconsider r1=p`1,r2=p`2 as Element of REAL by XREAL_0:def 1;
reconsider g=<*r1,r2*> as FinSequence of REAL by FINSEQ_2:13;
A1: p/.2 = g/.2 by EUCLID:53
.=p`2 by FINSEQ_4:17;
p/.1 = g/.1 by EUCLID:53
.=p`1 by FINSEQ_4:17;
hence thesis by A1;
end;
theorem
for p being Element of TOP-REAL 2 holds p/.1=proj1.p & p/.2= proj2.p
proof
let p be Element of TOP-REAL 2;
A1: proj2.p=p`2 by PSCOMP_1:def 6
.=p/.2 by Th29;
proj1.p=p`1 by PSCOMP_1:def 5
.=p/.1 by Th29;
hence thesis by A1;
end;