:: Continuity of Barycentric Coordinates in Euclidean Topological Spaces
:: by Karol P\kak
::
:: Received December 21, 2010
:: Copyright (c) 2010-2011 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 ALGSTR_0, AOFA_I00, ARYTM_1, ARYTM_3, CARD_1, CARD_3, CLASSES1,
COMPLEX1, CONVEX1, EUCLID, EUCLID_9, FINSEQ_1, FINSEQ_2, FINSEQ_4,
FINSET_1, FUNCOP_1, FUNCSDOM, FUNCT_1, FUNCT_2, LMOD_7, MATRIX_1,
MATRIX_3, MATRIX13, MATRLIN, MATRLIN2, MESFUNC1, METRIC_1, MONOID_0,
NAT_1, NUMBERS, ORDINAL1, ORDINAL2, ORDINAL4, PARTFUN1, PCOMPS_1,
PRE_TOPC, PROB_1, PRVECT_1, QC_LANG1, RCOMP_1, REAL_1, RELAT_1, RFINSEQ,
RLAFFIN1, RLSUB_1, RLTOPSP1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5,
RUSUB_4, SEMI_AF1, SETFAM_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI,
TOPMETR, TOPS_1, TOPS_2, VALUED_0, VALUED_1, VECTSP_1, XBOOLE_0,
XCMPLX_0, XREAL_0, XXREAL_0, XXREAL_1, ZFMISC_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, NAT_1,
XXREAL_0, CARD_1, XREAL_0, REAL_1, FINSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, FUNCOP_1, STRUCT_0, FINSEQ_2,
FINSEQOP, RVSUM_1, RLVECT_1, RLVECT_2, RUSUB_4, CONVEX1, RLAFFIN1,
COMPLEX1, VALUED_0, METRIC_1, BINOP_2, PRE_TOPC, PCOMPS_1, ALGSTR_0,
FUNCSDOM, TOPS_2, RLTOPSP1, EUCLID, VFUNCT_1, FVSUM_1, RLSUB_1, RLVECT_3,
RLVECT_5, CARD_3, RCOMP_1, EUCLID_9, VECTSP_1, MATRIX_1, NAT_D, MATRIX_3,
MATRIX_6, VECTSP_6, VECTSP_7, MATRIX13, MATRLIN, RLSUB_2, RFINSEQ,
TOPMETR, RLAFFIN2, SETFAM_1, PRVECT_1, TOPREAL9, MATRTOP1;
constructors BINOP_2, CONVEX1, EUCLID_9, FUNCSDOM, FVSUM_1, MATRIX_6,
MATRIX13, MATRTOP1, MONOID_0, NAT_D, RANKNULL, RCOMP_1, REAL_1, REALSET1,
RFINSEQ, RLAFFIN1, RLAFFIN2, RLSUB_2, RLVECT_3, RLVECT_5, RUSUB_5, SEQ_1,
TDLAT_3, TOPMETR, TOPREAL9, TOPS_2, VECTSP_7, VFUNCT_1, WELLORD2, SEQ_4;
registrations CARD_1, EUCLID, EUCLID_7, EUCLID_9, FINSEQ_1, FINSEQ_2,
FINSET_1, FUNCT_1, JORDAN2B, MATRIX13, MATRTOP1, MEMBERED, MONOID_0,
NAT_1, NUMBERS, PRE_TOPC, PRVECT_1, REAL_1, REALSET1, RELAT_1, RELSET_1,
RLAFFIN1, RLTOPSP1, RLVECT_5, RVSUM_1, STRUCT_0, SUBSET_1, TEX_1,
TOPGEN_1, TOPMETR, TOPREAL1, TOPREALC, TOPS_1, VALUED_0, VECTSP_1,
VECTSP_9, XBOOLE_0, XREAL_0, XXREAL_0, ZFMISC_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions FINSEQ_1, MATRIX13, MATRTOP1, RLTOPSP1, STRUCT_0, SUBSET_1,
TARSKI, XBOOLE_0;
theorems BORSUK_5, CARD_1, CARD_2, CARD_3, CARD_FIN, COMPLEX1, CONVEX1,
EUCLID, EUCLID_7, EUCLID_9, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4,
FUNCOP_1, FUNCT_1, FUNCT_2, FVSUM_1, GOBOARD6, JORDAN2B, JORDAN2C,
JORDAN6, LAPLACE, MATRIX_6, MATRIX13, MATRLIN, MATRLIN2, MATRTOP1,
MATRTOP2, METRIC_1, METRIZTS, NAT_1, ORDINAL1, PARTFUN1, PCOMPS_1,
PRALG_3, PRE_TOPC, REALSET1, RELAT_1, RFINSEQ, RLAFFIN1, RLAFFIN2,
RLSUB_1, RLSUB_2, RLTOPSP1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5,
RUSUB_4, RVSUM_1, SETFAM_1, SPPOL_1, STIRL2_1, STRUCT_0, TARSKI,
TOPGRP_1, TOPMETR, TOPREAL7, TOPREAL9, TOPS_1, TOPS_2, TREAL_1, TSEP_1,
URYSOHN1, VECTSP_1, VECTSP_4, VECTSP_7, VECTSP_9, VFUNCT_1, XBOOLE_0,
XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_0, XREAL_1, XXREAL_0, XXREAL_1,
ZFMISC_1;
schemes FINSEQ_1, FUNCT_2, TREES_2;
begin :: Preliminaries
reserve x for set,
n,m,k for Nat,
r for Real,
V for RealLinearSpace,
v,u,w,t for VECTOR of V,
Av for finite Subset of V,
Affv for finite affinely-independent Subset of V;
Lm1: for f be n-element real-valued FinSequence holds f is Point of TOP-REAL n
proof
let f be n-element real-valued FinSequence;
len f=n & @@f=f by CARD_1:def 13;
hence thesis by TOPREAL7:18;
end;
theorem Th1:
for f1,f2 be real-valued FinSequence, r be real number
holds Intervals(f1,r)^Intervals(f2,r) = Intervals(f1^f2,r)
proof
let f1,f2 be real-valued FinSequence;
let r be real number;
set I1=Intervals(f1,r),I2=Intervals(f2,r),f12=f1^f2;
set I12=Intervals(f12,r);
A1: dom I12=dom f12 by EUCLID_9:def 3;
A2: len f12=len f1+len f2 & len(I1^I2)=len I1+len I2 by FINSEQ_1:35;
A3: dom I1=dom f1 by EUCLID_9:def 3;
then A4: len I1=len f1 by FINSEQ_3:31;
A5: dom I2=dom f2 by EUCLID_9:def 3;
then len I2=len f2 by FINSEQ_3:31;
then A6: dom(I1^I2)=dom I12 by A1,A4,A2,FINSEQ_3:31;
now let i be Nat;
assume A7: i in dom(I1^I2);
then A8: I12.i=].f12.i-r,f12.i+r.[ by A1,A6,EUCLID_9:def 3;
per cases by A7,FINSEQ_1:38;
suppose A9: i in dom I1;
then (I1^I2).i=I1.i & f12.i=f1.i by A3,FINSEQ_1:def 7;
hence (I1^I2).i=I12.i by A3,A8,A9,EUCLID_9:def 3;
end;
suppose ex j be Nat st j in dom I2 & i=len I1+j;
then consider j be Nat such that
A10: j in dom I2 and
A11: i=len I1+j;
(I1^I2).i=I2.j & f12.i=f2.j by A5,A4,A10,A11,FINSEQ_1:def 7;
hence (I1^I2).i=I12.i by A5,A8,A10,EUCLID_9:def 3;
end;
end;
hence thesis by A6,FINSEQ_1:17;
end;
theorem Th2:
for f1,f2 be FinSequence holds
x in product(f1^f2)
iff
ex p1,p2 be FinSequence st x = p1^p2 & p1 in product f1 & p2 in product f2
proof
let f1,f2 be FinSequence;
set f12=f1^f2;
A1: len f12=len f1+len f2 by FINSEQ_1:35;
dom f1=Seg(len f1) by FINSEQ_1:def 3;
then A2: f12|Seg(len f1)=f1 by FINSEQ_1:33;
hereby assume A3: x in product f12;
then consider g be Function such that
A4: x=g and
A5: dom g=dom f12 and
A6: for y be set st y in dom f12 holds g.y in f12.y by CARD_3:def 5;
dom f12=Seg len f12 by FINSEQ_1:def 3;
then reconsider g as FinSequence by A5,FINSEQ_1:def 2;
set p1=g|(len f1);
consider p2 be FinSequence such that
A7: g=p1^p2 by FINSEQ_1:101;
take p1,p2;
thus x=p1^p2 & p1 in product f1 by A2,A3,A4,A7,PRALG_3:1;
A8: len f12=len g by A5,FINSEQ_3:31;
then A9: len f1=len p1 by A1,FINSEQ_1:80,NAT_1:11;
len g=len p1+len p2 by A7,FINSEQ_1:35;
then A10: dom f2=dom p2 by A1,A8,A9,FINSEQ_3:31;
now let y be set;
assume A11: y in dom f2;
then reconsider i=y as Nat;
i+len f1 in dom f12 by A11,FINSEQ_1:41;
then
g.(i+len f1) in f12.(i+len f1) & f12.(i+len f1)=f2.i
by A6,A11,FINSEQ_1:def 7;
hence p2.y in f2.y by A7,A9,A10,A11,FINSEQ_1:def 7;
end;
hence p2 in product f2 by A10,CARD_3:def 5;
end;
given p1,p2 be FinSequence such that
A12: x=p1^p2 and
A13: p1 in product f1 and
A14: p2 in product f2;
A15: ex g be Function st p2=g & dom g=dom f2 & for y be set st y in dom f2
holds g.y in f2.y by A14,CARD_3:def 5;
A16: ex g be Function st p1=g & dom g=dom f1 & for y be set st y in dom f1
holds g.y in f1.y by A13,CARD_3:def 5;
then A17: len p1=len f1 by FINSEQ_3:31;
A18: now let y be set;
assume A19: y in dom f12;
then reconsider i=y as Nat;
per cases by A19,FINSEQ_1:38;
suppose A20: i in dom f1;
then f12.y=f1.i & (p1^p2).y=p1.i by A16,FINSEQ_1:def 7;
hence (p1^p2).y in f12.y by A16,A20;
end;
suppose ex j be Nat st j in dom f2 & i=len f1+j;
then consider j be Nat such that
A21: j in dom f2 and
A22: i=len f1+j;
f12.y=f2.j & (p1^p2).y=p2.j by A15,A17,A21,A22,FINSEQ_1:def 7;
hence (p1^p2).y in f12.y by A15,A21;
end;
end;
len(p1^p2)=len p1+len p2 & len p2=len f2 by A15,FINSEQ_1:35,FINSEQ_3:31;
then dom(p1^p2)=dom f12 by A1,A17,FINSEQ_3:31;
hence thesis by A12,A18,CARD_3:def 5;
end;
Lm2: for A be Subset of V holds Lin A=Lin(A\{0.V})
proof
let A be Subset of V;
per cases;
suppose not 0.V in A;
hence thesis by ZFMISC_1:65;
end;
suppose A1: 0.V in A;
{0.V}=the carrier of(0).V by RLSUB_1:def 3;
then A2: Lin{0.V}=(0).V by RLVECT_3:21;
A=(A\{0.V})\/{0.V} by A1,ZFMISC_1:140;
hence Lin A=(Lin(A\{0.V}))+(0).V by A2,RLVECT_3:25
.=Lin(A\{0.V}) by RLSUB_2:13;
end;
end;
theorem Th3:
V is finite-dimensional iff (Omega).V is finite-dimensional
proof
set O=(Omega).V;
thus V is finite-dimensional implies O is finite-dimensional;
assume O is finite-dimensional;
then consider A be finite Subset of O such that
A1: A is Basis of O by RLVECT_5:def 1;
A2: the RLSStruct of V=O by RLSUB_1:def 4;
then reconsider a=A as finite Subset of V;
Lin(A)=O by A1,RLVECT_3:def 3;
then A3: Lin(a)=O by RLVECT_5:21;
A is linearly-independent by A1,RLVECT_3:def 3;
then a is linearly-independent by RLVECT_5:15;
then a is Basis of V by A2,A3,RLVECT_3:def 3;
hence thesis by RLVECT_5:def 1;
end;
registration
let V be finite-dimensional RealLinearSpace;
cluster -> finite (affinely-independent Subset of V);
coherence
proof
let A be affinely-independent Subset of V;
per cases;
suppose A is empty;
hence thesis;
end;
suppose A is non empty;
then consider v be VECTOR of V such that
v in A and
A1: -v+A\{0.V} is linearly-independent by RLAFFIN1:def 4;
set vA=-v+A;
vA\{0.V}\/{0.V}=vA\/{0.V} by XBOOLE_1:39;
then A2: card vA=card A & vA c=vA\{0.V}\/{0.V} by RLAFFIN1:7,XBOOLE_1:7;
vA\{0.V} is finite by A1,RLVECT_5:25;
hence thesis by A2;
end;
end;
end;
registration
let n;
cluster TOP-REAL n -> add-continuous Mult-continuous;
coherence
proof
set T=TOP-REAL n,E=Euclid n,TE=TopSpaceMetr E;
A1: the TopStruct of T=TE by EUCLID:def 8;
A2: n in NAT by ORDINAL1:def 13;
thus T is add-continuous
proof
let x1,x2 be Point of T,V be Subset of T such that
A3: V is open and
A4: x1+x2 in V;
reconsider X1=x1,X2=x2,X12=x1+x2 as Point of E by A1,TOPMETR:16;
reconsider v=V as Subset of TE by A1;
V in the topology of T by A3,PRE_TOPC:def 5;
then v is open by A1,PRE_TOPC:def 5;
then consider r be real number such that
A5: r>0 and
A6: Ball(X12,r)c=v by A4,TOPMETR:22;
set r2=r/2;
reconsider B1=Ball(X1,r2),B2=Ball(X2,r2) as Subset of T by A1,TOPMETR:16;
take B1,B2;
thus B1 is open & B2 is open & x1 in B1 & x2 in B2
by A2,A5,GOBOARD6:4,6,XREAL_1:217;
let x be set;
assume x in B1+B2;
then x in {b1+b2 where b1,b2 is Element of T:b1 in B1 & b2 in B2}
by RUSUB_4:def 10;
then consider b1,b2 be Element of T such that
A7: x=b1+b2 and
A8: b1 in B1 and
A9: b2 in B2;
reconsider e1=b1,e2=b2,e12=b1+b2 as Point of E by A1,TOPMETR:16;
reconsider y1=x1,y2=x2,c1=b1,c2=b2 as Element of REAL n by EUCLID:25;
dist(X2,e2)0 and
A17: Ball(AX,r)c=v by A15,TOPMETR:22;
set r2=r/2;
A18: r2>0 by A16,XREAL_1:217;
then A19: r2/2>0 by XREAL_1:217;
ex m be positive Real st abs(a)*m0;
then reconsider m=r2/2/abs(a) as positive Real by A19,XREAL_1:141;
take m;
r2/20) by RVSUM_1:53
.=C-(Y-Y) by RVSUM_1:58
.=C-Y+Y by RVSUM_1:62;
then A25: |.c.|<=|.c-y.|+|.y.| by EUCLID:15;
A26: dist(X,e)=0 & |.y-c.|=dist(X,e) by A2,COMPLEX1:132,SPPOL_1:20;
then |.a*y+-a*c.|<=abs(a)*m by A26,A28,XREAL_1:66;
then A29: |.a*y+-a*c.|0)-s*C by RVSUM_1:53
.=a*y-(a*C-a*C)-s*c by RVSUM_1:58
.=a*y-a*C+a*C-s*c by RVSUM_1:62
.=a*y-a*C+a*C+-s*c by RVSUM_1:52
.=a*y-a*C+(a*c+-s*c) by RVSUM_1:32
.=a*y+-a*c+(a*c+-s*c) by RVSUM_1:52;
then dist(AX,se)=|.a*y+-a*c+(a*c+-s*c).| by A2,A31,SPPOL_1:20;
then dist(AX,se) finite-dimensional;
coherence
proof
the RLSStruct of TOP-REAL n=RealVectSpace Seg n by EUCLID:def 8;
then (Omega).(TOP-REAL n)=RealVectSpace Seg n by RLSUB_1:def 4;
hence thesis by Th3;
end;
end;
reserve pn for Point of TOP-REAL n,
An for Subset of TOP-REAL n,
Affn for affinely-independent Subset of TOP-REAL n,
Ak for Subset of TOP-REAL k;
theorem Th4:
dim TOP-REAL n = n
proof
the RLSStruct of TOP-REAL n=RealVectSpace Seg n by EUCLID:def 8;
then (Omega).(TOP-REAL n)=RealVectSpace Seg n by RLSUB_1:def 4;
then dim(Omega).(TOP-REAL n)=n by EUCLID_7:49;
hence thesis by RLVECT_5:31;
end;
theorem Th5:
for V be finite-dimensional RealLinearSpace
for A be affinely-independent Subset of V holds card A <= 1+dim V
proof
let V be finite-dimensional RealLinearSpace;
let A be affinely-independent Subset of V;
per cases;
suppose A is empty;
hence thesis;
end;
suppose A is non empty;
then consider v be VECTOR of V such that
v in A and
A1: -v+A\{0.V} is linearly-independent by RLAFFIN1:def 4;
set vA=-v+A;
vA\{0.V} misses {0.V} by XBOOLE_1:79;
then
A2: card{0.V}=1 & card(vA\{0.V}\/{0.V})=card(vA\{0.V})+card{0.V}
by CARD_2:53,60;
A3: card vA=card A by RLAFFIN1:7;
reconsider vA as finite set;
card(vA\{0.V})=dim Lin(-v+A\{0.V}) by A1,RLVECT_5:30;
then card(vA\{0.V})<=dim V by RLVECT_5:29;
then A4: card(vA\{0.V}\/{0.V})<=1+dim V by A2,XREAL_1:9;
vA\{0.V}\/{0.V}=vA\/{0.V} by XBOOLE_1:39;
then card A<=card(vA\{0.V}\/{0.V}) by A3,NAT_1:44,XBOOLE_1:7;
hence thesis by A4,XXREAL_0:2;
end;
end;
theorem Th6:
for V be finite-dimensional RealLinearSpace,
A be affinely-independent Subset of V
holds
card A = dim V + 1
iff
Affin A = [#]V
proof
let V be finite-dimensional RealLinearSpace;
let A be affinely-independent Subset of V;
A1: 0.V in [#]V;
A2: A c=Affin A by RLAFFIN1:49;
hereby assume A3: card A=dim V+1;
then A is non empty;
then consider v be VECTOR of V such that
A4: v in A and
A5: -v+A\{0.V} is linearly-independent by RLAFFIN1:def 4;
set vA=-v+A;
reconsider vA as finite Subset of V;
-v+v in {-v+w where w is Element of V:w in A} by A4;
then A6: -v+v in vA by RUSUB_4:def 9;
A7: card vA=card A & card{0.V}=1 by CARD_2:60,RLAFFIN1:7;
-v+v=0.V by RLVECT_1:16;
then vA=vA\{0.V}\/{0.V} by A6,ZFMISC_1:140;
then A8: card A=card(vA\{0.V})+1 by A7,CARD_2:53,XBOOLE_1:79;
dim Lin(vA\{0.V})=card(vA\{0.V}) by A5,RLVECT_5:30;
then (Omega).V=(Omega).Lin(vA\{0.V}) by A3,A8,RLVECT_5:32
.=Lin(vA\{0.V}) by RLSUB_1:def 4;
then the RLSStruct of V=Lin(vA\{0.V}) by RLSUB_1:def 4;
then A9: [#]V =the carrier of Lin vA by Lm2;
then v in Lin vA by STRUCT_0:def 5;
hence [#]V=v+Lin vA by A9,RLSUB_1:64
.=v+Up Lin vA by RUSUB_4:32
.=Affin A by A2,A4,RLAFFIN1:57;
end;
assume A10: Affin A=[#]V;
then A is non empty;
then consider v be VECTOR of V such that
A11: v in A and
A12: -v+A\{0.V} is linearly-independent by RLAFFIN1:def 4;
set vA=-v+A;
reconsider vA as finite Subset of V;
[#]V=v+Up Lin vA by A10,RLAFFIN1:57
.=v+Lin vA by RUSUB_4:32;
then [#]Lin vA=the carrier of the RLSStruct of V by A1,RLSUB_1:63
.=the carrier of(Omega).V by RLSUB_1:def 4;
then Lin vA=(Omega).V by RLSUB_1:38
.=the RLSStruct of V by RLSUB_1:def 4;
then the RLSStruct of V=Lin(vA\{0.V}) by Lm2;
then A13: vA\{0.V} is Basis of V by A12,RLVECT_3:def 3;
-v+v in {-v+w where w is Element of V:w in A} by A11;
then A14: -v+v in vA by RUSUB_4:def 9;
-v+v=0.V by RLVECT_1:16;
then A15: vA=vA\{0.V}\/{0.V} by A14,ZFMISC_1:140;
card vA=card A & card{0.V}=1 by CARD_2:60,RLAFFIN1:7;
hence card A=card(vA\{0.V})+1 by A15,CARD_2:53,XBOOLE_1:79
.=dim V+1 by A13,RLVECT_5:def 3;
end;
begin :: Open and Closed Subsets of a Subspace of the Euclidean Topological
:: Space
theorem Th7:
k <= n & An = {v where v is Element of TOP-REAL n : v|k in Ak}
implies
(An is open iff Ak is open)
proof
assume k<=n;
then reconsider nk=n-k as Element of NAT by NAT_1:21;
A1: the TopStruct of TOP-REAL n=TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider an=An as Subset of TopSpaceMetr Euclid n;
A2: the TopStruct of TOP-REAL k=TopSpaceMetr Euclid k by EUCLID:def 8;
then reconsider ak=Ak as Subset of TopSpaceMetr Euclid k;
assume A3: An={v where v is Element of TOP-REAL n:v|k in Ak};
hereby assume An is open;
then an in the topology of TOP-REAL n by PRE_TOPC:def 5;
then A4: an is open by A1,PRE_TOPC:def 5;
for e being Point of Euclid k st e in ak ex r being real number st r>0
& OpenHypercube(e,r)c=ak
proof
len(nk|->0)=nk & @@(nk|->0)=nk|->0 by CARD_1:def 13;
then reconsider nk0=nk|->0 as Point of Euclid nk by TOPREAL7:17;
let e be Point of Euclid k;
A5: @@(e^(nk|->0))=e^(nk|->0) & len(e^nk0)=n by CARD_1:def 13;
then reconsider en=e^nk0 as Point of Euclid n by TOPREAL7:17;
reconsider En=e^nk0 as Point of TOP-REAL n by A5,TOPREAL7:18;
len e=k by CARD_1:def 13;
then dom e=Seg k by FINSEQ_1:def 3;
then A6: e =En|k by FINSEQ_1:33;
assume e in ak;
then en in an by A3,A6;
then consider m be non zero Element of NAT such that
A7: OpenHypercube(en,1/m)c=an by A4,EUCLID_9:23;
take r=1/m;
thus r>0 by XREAL_1:141;
let y be set;
assume A8: y in OpenHypercube(e,r);
then reconsider p=y as Point of TopSpaceMetr Euclid k;
A9: p in product Intervals(e,r) by A8,EUCLID_9:def 4;
reconsider P=p as Point of TOP-REAL k by A2;
nk0 in OpenHypercube(nk0,r) by EUCLID_9:11,XREAL_1:141;
then A10: nk0 in product Intervals(nk0,r) by EUCLID_9:def 4;
Intervals(e,r)^Intervals(nk0,r)=Intervals(en,r) by Th1;
then P^nk0 in product Intervals(en,r) by A10,A9,Th2;
then P^nk0 in OpenHypercube(en,r) by EUCLID_9:def 4;
then P^nk0 in an by A7;
then consider v be Element of TOP-REAL n such that
A11: v=P^nk0 & v|k in Ak by A3;
len P=k by CARD_1:def 13;
then dom P=Seg k by FINSEQ_1:def 3;
hence y in ak by A11,FINSEQ_1:33;
end;
then ak is open by EUCLID_9:24;
then ak in the topology of TOP-REAL k by A2,PRE_TOPC:def 5;
hence Ak is open by PRE_TOPC:def 5;
end;
assume Ak is open;
then ak in the topology of TOP-REAL k by PRE_TOPC:def 5;
then A12: ak is open by A2,PRE_TOPC:def 5;
for e being Point of Euclid n st e in an ex r being real number st r>0
& OpenHypercube(e,r)c=an
proof
let e be Point of Euclid n;
assume e in an;
then consider v be Element of TOP-REAL n such that
A13: e=v and
A14: v|k in Ak by A3;
reconsider vk=v|k as Point of TOP-REAL k by A14;
A15: len vk=k by CARD_1:def 13;
@@vk=vk;
then reconsider Vk=vk as Point of Euclid k by A15,TOPREAL7:17;
consider m be non zero Element of NAT such that
A16: OpenHypercube(Vk,1/m)c=ak by A12,A14,EUCLID_9:23;
take r=1/m;
thus r>0 by XREAL_1:141;
let y be set;
assume A17: y in OpenHypercube(e,r);
then A18: y in product Intervals(e,r) by EUCLID_9:def 4;
reconsider Y=y as Point of TOP-REAL n by A1,A17;
A19: len v=n by CARD_1:def 13;
consider q be FinSequence such that
A20: @@v=vk^q by FINSEQ_1:101;
reconsider q as FinSequence of REAL by A20,FINSEQ_1:50;
len v=len vk+len q by A20,FINSEQ_1:35;
then reconsider Q=q as Point of Euclid nk by A15,A19,TOPREAL7:17;
Intervals(Vk,r)^Intervals(Q,r)=Intervals(e,r) by A13,A20,Th1;
then consider p1,p2 be FinSequence such that
A21: y=p1^p2 and
A22: p1 in product Intervals(Vk,r) and
p2 in product Intervals(Q,r) by A18,Th2;
A23: p1 in OpenHypercube(Vk,1/m) by A22,EUCLID_9:def 4;
then len p1=k by A2,CARD_1:def 13;
then Y|k=Y|dom p1 by FINSEQ_1:def 3
.=p1 by A21,FINSEQ_1:33;
hence thesis by A3,A16,A23;
end;
then an is open by EUCLID_9:24;
then an in the topology of TOP-REAL n by A1,PRE_TOPC:def 5;
hence thesis by PRE_TOPC:def 5;
end;
Lm3: the carrier of n-VectSp_over F_Real=the carrier of TOP-REAL n
proof
thus the carrier of n-VectSp_over F_Real=n-tuples_on the carrier of F_Real
by MATRIX13:102
.=REAL n by EUCLID:def 1,VECTSP_1:def 15
.=the carrier of TOP-REAL n by EUCLID:25;
end;
theorem Th8:
for A be Subset of TOP-REAL(k+n) st
A = {v^(n|->0) where v is Element of TOP-REAL k: not contradiction}
for B be Subset of (TOP-REAL(k+n))|A st
B = {v where v is Point of TOP-REAL(k+n): v|k in Ak & v in A}
holds Ak is open iff B is open
proof
set kn=k+n;
set TRn=TOP-REAL kn;
set TRk=TOP-REAL k;
let A be Subset of TRn such that
A1: A={v^(n|->0) where v is Element of TRk:not contradiction};
A2: the TopStruct of TRk=TopSpaceMetr Euclid k by EUCLID:def 8;
then reconsider p=Ak as Subset of TopSpaceMetr Euclid k;
set TRA=TRn|A;
let B be Subset of TRn|A such that
A3: B={v where v is Element of TRn:v|k in Ak & v in A};
A4: [#]TRA=A by PRE_TOPC:def 10;
A5: kn>=k by NAT_1:11;
hereby set PP={v where v is Element of TRn:v|k in Ak};
PP c=[#]TRn
proof
let x be set;
assume x in PP;
then ex v be Element of TRn st x=v & v|k in Ak;
hence thesis;
end;
then reconsider PP as Subset of TRn;
A6: PP/\A c=B
proof
let x be set;
assume A7: x in PP/\A;
then x in PP by XBOOLE_0:def 4;
then consider v be Element of TRn such that
A8: x=v & v|k in Ak;
x in A by A7,XBOOLE_0:def 4;
hence thesis by A3,A8;
end;
assume Ak is open;
then PP is open by A5,Th7;
then PP in the topology of TRn by PRE_TOPC:def 5;
then A9: PP/\[#]TRA in the topology of TRA by PRE_TOPC:def 9;
B c=PP/\A
proof
let x be set;
assume x in B;
then consider v be Element of TRn such that
A10: x=v and
A11: v|k in Ak and
A12: v in A by A3;
v in PP by A11;
hence thesis by A10,A12,XBOOLE_0:def 4;
end;
then B=PP/\A by A6,XBOOLE_0:def 10;
hence B is open by A4,A9,PRE_TOPC:def 5;
end;
assume B is open;
then B in the topology of TRA by PRE_TOPC:def 5;
then consider Q be Subset of TRn such that
A13: Q in the topology of TRn and
A14: Q/\[#]TRA=B by PRE_TOPC:def 9;
A15: the TopStruct of TRn=TopSpaceMetr Euclid kn by EUCLID:def 8;
then reconsider q=Q as Subset of TopSpaceMetr Euclid kn;
A16: q is open by A13,A15,PRE_TOPC:def 5;
for e being Point of Euclid k st e in p ex r being real number st r>0 &
OpenHypercube(e,r)c=p
proof
let e be Point of Euclid k;
A17: len(n|->0)=n by CARD_1:def 13;
A18: @@(e^(n|->0))=e^(n|->0);
A19: len e=k by CARD_1:def 13;
then len(e^(n|->0))=kn by A17,FINSEQ_1:35;
then reconsider e0=e^(n|->0) as Point of Euclid kn by A18,TOPREAL7:17;
dom e=Seg k by A19,FINSEQ_1:def 3;
then A20: e =e0|k by FINSEQ_1:33;
n|->0=@@(n|->0);
then reconsider N=n|->0 as Element of Euclid n by A17,TOPREAL7:17;
e is Element of TRk by Lm1;
then A21: e0 in A by A1;
assume e in p;
then e0 in B by A3,A21,A20;
then e0 in q by A14,XBOOLE_0:def 4;
then consider m be non zero Element of NAT such that
A22: OpenHypercube(e0,1/m)c=q by A16,EUCLID_9:23;
set r=1/m;
take r;
thus r>0 by XREAL_1:141;
let x be set;
N in OpenHypercube(N,r) by EUCLID_9:11,XREAL_1:141;
then A23: N in product Intervals(N,r) by EUCLID_9:def 4;
assume A24: x in OpenHypercube(e,r);
then reconsider w=x as Point of TRk by A2;
A25: Intervals(e,r)^Intervals(N,r)=Intervals(e^N,r) by Th1;
w in product Intervals(e,r) by A24,EUCLID_9:def 4;
then w^N in product Intervals(e0,r) by A23,A25,Th2;
then A26: w^N in OpenHypercube(e0,r) by EUCLID_9:def 4;
w^N in A by A1;
then w^N in B by A4,A14,A22,A26,XBOOLE_0:def 4;
then A27: ex v be Element of TRn st w^N=v & v|k in Ak & v in A by A3;
len w=k by CARD_1:def 13;
then (w^N)|k=(w^N)|dom w by FINSEQ_1:def 3
.=w by FINSEQ_1:33;
hence thesis by A27;
end;
then p is open by EUCLID_9:24;
then Ak in the topology of TOP-REAL k by A2,PRE_TOPC:def 5;
hence thesis by PRE_TOPC:def 5;
end;
theorem Th9:
for A be affinely-independent Subset of V, B be Subset of V st B c= A
holds conv A/\Affin B = conv B
proof
let A be affinely-independent Subset of V;
let B be Subset of V;
A1: conv B c=Affin B by RLAFFIN1:65;
assume A2: B c=A;
thus conv A/\Affin B c=conv B
proof
let x be set;
assume A3: x in conv A/\Affin B;
then A4: x in Affin B by XBOOLE_0:def 4;
A5: x in conv A by A3,XBOOLE_0:def 4;
A6: now let v be Element of V;
x|--B=x|--A by A2,A4,RLAFFIN1:77;
hence v in B implies 0<=(x|--B).v by A5,RLAFFIN1:71;
end;
B is affinely-independent by A2,RLAFFIN1:43;
hence thesis by A4,A6,RLAFFIN1:73;
end;
conv B c=conv A by A2,RLAFFIN1:3;
hence thesis by A1,XBOOLE_1:19;
end;
theorem Th10:
for V be non empty RLSStruct, A be non empty set
for f be PartFunc of A,the carrier of V
for X be set holds (r(#)f).:X = r*(f.:X)
proof
let V be non empty RLSStruct;
let A be non empty set;
let f be PartFunc of A,the carrier of V;
let X be set;
set rf=r(#)f;
A1: dom rf=dom f by VFUNCT_1:def 4;
hereby let y be set;
assume y in rf.:X;
then consider x be set such that
A2: x in dom rf and
A3: x in X and
A4: y=rf.x by FUNCT_1:def 12;
rf.x=rf/.x by A2,PARTFUN1:def 8;
then A5: y=r*(f/.x) by A2,A4,VFUNCT_1:def 4;
f.x=f/.x by A1,A2,PARTFUN1:def 8;
then f/.x in f.:X by A1,A2,A3,FUNCT_1:def 12;
then y in {r*v where v is Element of V:v in f.:X} by A5;
hence y in r*(f.:X) by CONVEX1:def 1;
end;
let y be set;
assume y in r*(f.:X);
then y in {r*v where v is Element of V:v in f.:X} by CONVEX1:def 1;
then consider v be Element of V such that
A6: y=r*v and
A7: v in f.:X;
consider x be set such that
A8: x in dom f and
A9: x in X and
A10: v=f.x by A7,FUNCT_1:def 12;
v=f/.x by A8,A10,PARTFUN1:def 8;
then y=rf/.x by A1,A6,A8,VFUNCT_1:def 4
.=rf.x by A1,A8,PARTFUN1:def 8;
hence thesis by A1,A8,A9,FUNCT_1:def 12;
end;
theorem Th11:
0*n in An implies Affin An = [#]Lin An
proof
set TR=TOP-REAL n;
set A=An;
A1: 0*n=0.TR & A c=Affin A by EUCLID:70,RLAFFIN1:49;
assume 0*n in A;
hence Affin A=0.TR+Up Lin(-0.TR+A) by A1,RLAFFIN1:57
.=Up Lin(-0.TR+A) by RLAFFIN1:6
.=Up Lin(0.TR+A) by RLVECT_1:25
.=Up Lin A by RLAFFIN1:6
.=[#]Lin A by RUSUB_4:def 6;
end;
registration
let V be non empty addLoopStr;
let A be finite Subset of V;
let v be Element of V;
cluster v+A -> finite;
coherence
proof
deffunc F(Element of V)=v+$1;
card{F(w) where w is Element of V:w in A}c=card A from TREES_2:sch 2;
then card(v+A) is finite by RUSUB_4:def 9;
hence thesis;
end;
end;
Lm4: for V be non empty RLSStruct,A be Subset of V,r be Real holds card(r*A)c=
card A
proof
let V be non empty RLSStruct;
let A be Subset of V;
let r be real number;
deffunc F(Element of V)=r*$1;
card{F(w) where w is Element of V:w in A}c=card A from TREES_2:sch 2;
hence thesis by CONVEX1:def 1;
end;
registration
let V be non empty RLSStruct;
let A be finite Subset of V;
let r;
cluster r*A -> finite;
coherence
proof
card(r*A)c=card A by Lm4;
hence thesis;
end;
end;
theorem Th12:
for A be Subset of V holds
card A = card(r*A)
iff
r<>0 or A is trivial
proof
let A be Subset of V;
A1: card{0.V}=1 by CARD_2:60;
hereby assume A2: card A=card(r*A);
assume A3: r=0;
then A4: r*A c={0.V} by RLAFFIN1:12;
then reconsider a=A as finite set by A2;
reconsider rA=r*A as finite set by A4;
card(rA)<=card{0.V} by A3,NAT_1:44,RLAFFIN1:12;
then card a<1+1 by A1,A2,NAT_1:13;
hence A is trivial by REALSET1:13;
end;
assume A5: r<>0 or A is trivial;
per cases by A5;
suppose A6: r<>0;
A7: 1*A=A & (1/r)*r*A=(1/r)*(r*A) by RLAFFIN1:10,11;
A8: card(r*A)c=card A by Lm4;
(1/r)*r=1 by A6,XCMPLX_1:88;
then card A c=card(r*A) by A7,Lm4;
hence thesis by A8,XBOOLE_0:def 10;
end;
suppose A9: A is empty;
r*A is empty
proof
assume r*A is non empty;
then consider x be set such that
A10: x in r*A by XBOOLE_0:def 1;
x in {r*v where v is Element of V:v in A} by A10,CONVEX1:def 1;
then ex v be Element of V st x=r*v & v in A;
hence contradiction by A9;
end;
hence thesis by A9;
end;
suppose A11: r=0 & A is non empty trivial;
then consider x being set such that
A12: A={x} by REALSET1:def 4;
r*A={0.V} by A11,CONVEX1:34;
hence thesis by A1,A12,CARD_2:60;
end;
end;
registration
let V be non empty RLSStruct;
let f be FinSequence of V;
let r;
cluster r(#)f -> FinSequence-like;
coherence
proof
dom(r(#)f)=dom f by VFUNCT_1:def 4
.=Seg len f by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
end;
begin :: The Vector of Barycentric Coordinates
definition
let X be finite set;
mode Enumeration of X -> one-to-one FinSequence means :Def1:
rng it = X;
existence
proof
ex p be FinSequence st rng p=X & p is one-to-one by FINSEQ_4:73;
hence thesis;
end;
end;
definition
let X be 1-sorted;
let A be finite Subset of X;
redefine mode Enumeration of A -> one-to-one FinSequence of X;
coherence
proof
let E be Enumeration of A;
rng E=A by Def1;
hence thesis by FINSEQ_1:def 4;
end;
end;
reserve EV for Enumeration of Affv,
EN for Enumeration of Affn;
theorem Th13:
for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr
for A be finite Subset of V, E be Enumeration of A, v be Element of V
holds E+(card A|->v) is Enumeration of (v+A)
proof
let V be Abelian add-associative right_zeroed right_complementable non empty
addLoopStr;
let A be finite Subset of V;
let E be Enumeration of A;
let v be Element of V;
A1: rng E=A by Def1;
then A2: len E=card A by FINSEQ_4:77;
then reconsider e=E,cAv=card A|->v as Element of card A-tuples_on the carrier
of V by FINSEQ_2:110;
A3: len(e+cAv)=card A by CARD_1:def 13;
then A4: dom(e+cAv)=Seg card A by FINSEQ_1:def 3;
A5: dom e=Seg card A by A2,FINSEQ_1:def 3;
A6: rng(e+cAv)c=v+A
proof
let y be set;
assume y in rng(e+cAv);
then consider x be set such that
A7: x in dom(e+cAv) and
A8: (e+cAv).x=y by FUNCT_1:def 5;
reconsider x as Element of NAT by A7;
A9: e.x in rng e by A5,A4,A7,FUNCT_1:def 5;
then reconsider Ex=e.x as Element of V;
cAv.x=v by A4,A7,FINSEQ_2:71;
then y=Ex+v by A7,A8,FVSUM_1:21;
then y=v+Ex by RLVECT_1:def 5;
then y in {v+w where w is Element of V:w in A} by A1,A9;
hence thesis by RUSUB_4:def 9;
end;
v+A c=rng(e+cAv)
proof
let vA be set;
assume vA in v+A;
then vA in {v+a where a is Element of V:a in A} by RUSUB_4:def 9;
then consider a be Element of V such that
A10: vA=v+a and
A11: a in A;
consider x be set such that
A12: x in dom E and
A13: E.x=a by A1,A11,FUNCT_1:def 5;
reconsider x as Element of NAT by A12;
cAv.x=v by A5,A12,FINSEQ_2:71;
then (e+cAv).x=a+v by A5,A4,A12,A13,FVSUM_1:21
.=vA by A10,RLVECT_1:def 5;
hence thesis by A5,A4,A12,FUNCT_1:def 5;
end;
then A14: v+A=rng(e+cAv) by A6,XBOOLE_0:def 10;
card A=card(v+A) by RLAFFIN1:7;
then e+cAv is one-to-one by A3,A14,FINSEQ_4:77;
hence thesis by A14,Def1;
end;
theorem
for E be Enumeration of Av holds
r(#)E is Enumeration of r*Av
iff
r<>0 or Av is trivial
proof
let EV be Enumeration of Av;
set rE=r(#)EV;
A1: dom rE=dom EV by VFUNCT_1:def 4;
then A2: len rE=len EV by FINSEQ_3:31;
A3: rng EV=Av by Def1;
then A4: card Av=len EV by FINSEQ_4:77;
A5: rng rE=rE.:dom EV by A1,RELAT_1:146
.=r*(EV.:dom EV) by Th10
.=r*Av by A3,RELAT_1:146;
A6: card{0.V}=1 by CARD_2:60;
hereby reconsider rA=r*Av as finite set;
assume rE is Enumeration of r*Av;
then A7: card(r*Av)=card Av by A4,A2,A5,FINSEQ_4:77;
assume r=0;
then card Av<=1 by A6,A7,NAT_1:44,RLAFFIN1:12;
then card Av<1+1 by NAT_1:13;
hence Av is trivial by REALSET1:13;
end;
assume r<>0 or Av is trivial;
then card Av=card(r*Av) by Th12;
then rE is one-to-one by A4,A2,A5,FINSEQ_4:77;
hence thesis by A5,Def1;
end;
theorem Th15:
for M be Matrix of n,m,F_Real st the_rank_of M = n
for A be finite Subset of TOP-REAL n, E be Enumeration of A
holds (Mx2Tran M)*E is Enumeration of(Mx2Tran M).:A
proof
let M be Matrix of n,m,F_Real such that
A2: the_rank_of M=n;
set MT=Mx2Tran M;
A3: MT is one-to-one by A2,MATRTOP1:39;
set TRn=TOP-REAL n;
let A be finite Subset of TOP-REAL n;
let E be Enumeration of A;
A4: rng E=A by Def1;
dom MT=[#]TRn by FUNCT_2:def 1;
then len(MT*E)=len E by A4,FINSEQ_2:33;
then A5: dom(MT*E)=dom E by FINSEQ_3:31;
rng(MT*E)=(MT*E).:dom(MT*E) by RELAT_1:146
.=MT.:(E.:dom E) by A5,RELAT_1:159
.=MT.:A by A4,RELAT_1:146;
hence thesis by A3,Def1;
end;
definition
let V,Av;
let E be Enumeration of Av;
let x;
func x|--E -> FinSequence of REAL equals
(x|--Av)*E;
coherence;
end;
theorem Th16:
for E be Enumeration of Av holds len (x|--E) = card Av
proof
let E be Enumeration of Av;
rng E=Av by Def1;
then len E=card Av by FINSEQ_4:77;
hence thesis by FINSEQ_2:37;
end;
theorem Th17:
for E be Enumeration of v+Affv st w in Affin Affv & E = EV+(card Affv|->v)
holds w|--EV=(v+w)|--E
proof
set E=EV;
let Ev be Enumeration of v+Affv such that
A1: w in Affin Affv and
A2: Ev=E+(card Affv|->v);
set wA=w|--Affv;
A3: sum wA=1 by A1,RLAFFIN1:def 7;
v+w in {v+u:u in Affin Affv} by A1;
then A4: v+w in v+Affin Affv by RUSUB_4:def 9;
rng E=Affv by Def1;
then A5: len E=card Affv by FINSEQ_4:77;
then reconsider e=E,cAv=card Affv|->v as Element of card Affv-tuples_on the
carrier of V by FINSEQ_2:110;
A6: Affin(v+Affv)=v+Affin Affv & 1*v=v by RLAFFIN1:53,RLVECT_1:def 11;
Carrier(v+wA)=v+Carrier wA & Carrier wA c=Affv by RLAFFIN1:16,RLVECT_2:def 8;
then Carrier(v+wA)c=v+Affv by RLTOPSP1:8;
then reconsider vwA=v+wA as Linear_Combination of v+Affv by RLVECT_2:def 8;
Sum wA=w by A1,RLAFFIN1:def 7;
then A7: Sum vwA=1*v+w by A3,RLAFFIN1:39;
A8: len(w|--E)=card Affv by Th16;
A9: card Affv=card(v+Affv) by RLAFFIN1:7;
then len((v+w)|--Ev)=card Affv by Th16;
then A10: dom(w|--E)=dom((v+w)|--Ev) by A8,FINSEQ_3:31;
rng Ev=v+Affv by Def1;
then A11: len Ev=card Affv by A9,FINSEQ_4:77;
sum vwA=1 by A3,RLAFFIN1:37;
then A12: vwA=(v+w)|--(v+Affv) by A4,A7,A6,RLAFFIN1:def 7;
now let i be Nat;
assume A13: i in dom(w|--E);
then A14: (w|--E).i=(w|--Affv).(E.i) by FUNCT_1:22;
dom E=dom(w|--E) by A8,A5,FINSEQ_3:31;
then A15: E.i=E/.i by A13,PARTFUN1:def 8;
i in Seg card Affv by A8,A13,FINSEQ_1:def 3;
then A16: cAv.i=v by FINSEQ_2:71;
A17: ((v+w)|--Ev).i=((v+w)|--(v+Affv)).(Ev.i) by A10,A13,FUNCT_1:22;
dom Ev=dom(w|--E) by A8,A11,FINSEQ_3:31;
then Ev.i=E/.i+v by A2,A13,A16,A15,FVSUM_1:21;
hence ((v+w)|--Ev).i=(w|--Affv).(E/.i+v-v) by A12,A17,RLAFFIN1:def 1
.=(w|--Affv).(E/.i+(v-v)) by RLVECT_1:42
.=(w|--Affv).(E/.i+0.V) by RLVECT_1:28
.=(w|--E).i by A14,A15,RLVECT_1:def 7;
end;
hence thesis by A10,FINSEQ_1:17;
end;
theorem
for rE be Enumeration of r*Affv st v in Affin Affv & rE = r(#)EV & r<>0
holds v|--EV = (r*v)|--rE
proof
set E=EV;
let rE be Enumeration of r*Affv such that
A1: v in Affin Affv and
A2: rE=r(#)E and
A3: r<>0;
set vA=v|--Affv;
A4: Carrier vA c=Affv by RLVECT_2:def 8;
A5: r*v in {r*u:u in Affin Affv} by A1;
A6: dom rE=dom E by A2,VFUNCT_1:def 4;
Carrier(r(*)vA)=r*Carrier vA by A3,RLAFFIN1:23;
then Carrier(r(*)vA)c=r*Affv by A4,CONVEX1:39;
then reconsider rvA=r(*)vA as Linear_Combination of r*Affv by RLVECT_2:def 8;
sum vA=1 by A1,RLAFFIN1:def 7;
then A7: sum rvA=1 by A3,RLAFFIN1:38;
Sum vA=v by A1,RLAFFIN1:def 7;
then A8: Sum rvA=r*v by RLAFFIN1:40;
A9: len((r*v)|--rE)=card(r*Affv) by Th16;
A10: len(v|--E)=card Affv by Th16;
rng E=Affv by Def1;
then len E=card Affv by FINSEQ_4:77;
then A11: dom(v|--E)=dom E by A10,FINSEQ_3:31;
card Affv=card(r*Affv) by A3,Th12;
then A12: dom(v|--E)=dom((r*v)|--rE) by A10,A9,FINSEQ_3:31;
Affin(r*Affv)=r*Affin Affv by A3,RLAFFIN1:55;
then r*v in Affin(r*Affv) by A5,CONVEX1:def 1;
then A13: rvA=(r*v)|--(r*Affv) by A7,A8,RLAFFIN1:def 7;
now let k be Nat;
assume A14: k in dom(v|--E);
then A15: (v|--E).k=vA.(E.k) & E/.k=E.k by A11,FUNCT_1:22,PARTFUN1:def 8;
A16: rE/.k=r*(E/.k) by A2,A11,A6,A14,VFUNCT_1:def 4;
((r*v)|--rE).k=rvA.(rE.k) & rE/.k=rE.k by A13,A12,A11,A6,A14,FUNCT_1:22
,PARTFUN1:def 8;
hence ((r*v)|--rE).k=vA.(r"*(r*(E/.k))) by A3,A16,RLAFFIN1:def 2
.=vA.(r"*r*(E/.k)) by RLVECT_1:def 10
.=vA.(1*(E/.k)) by A3,XCMPLX_0:def 7
.=(v|--E).k by A15,RLVECT_1:def 11;
end;
hence thesis by A12,FINSEQ_1:17;
end;
theorem Th19:
for M be Matrix of n,m,F_Real st the_rank_of M = n
for ME be Enumeration of (Mx2Tran M).:Affn st ME = (Mx2Tran M)*EN
for pn st pn in Affin Affn holds pn |-- EN = ((Mx2Tran M).pn) |-- ME
proof
set TRn=TOP-REAL n;
let M be Matrix of n,m,F_Real such that
A2: the_rank_of M=n;
set MT=Mx2Tran M;
A3: MT is one-to-one by A2,MATRTOP1:39;
set E=EN;
set A=Affn;
let ME be Enumeration of(Mx2Tran M).:A such that
A4: ME=(Mx2Tran M)*E;
dom MT=the carrier of TRn by FUNCT_2:def 1;
then A,MT.:A are_equipotent by A3,CARD_1:60;
then A5: card A=card(MT.:A) by CARD_1:21;
let v be Element of TOP-REAL n such that
A6: v in Affin A;
set MTv=MT.v;
A7: len(v|--E)=card A by Th16;
A8: len(MTv|--ME)=card(MT.:A) by Th16;
now let i be Nat;
assume A9: 1<=i & i<=card A;
then A10: i in dom(MTv|--ME) by A5,A8,FINSEQ_3:27;
then A11: i in dom ME by FUNCT_1:21;
A12: i in dom(v|--E) by A7,A9,FINSEQ_3:27;
then i in dom E by FUNCT_1:21;
then E.i in rng E by FUNCT_1:def 5;
then reconsider Ei=E.i as Element of TRn;
thus(v|--E).i=(v|--A).Ei by A12,FUNCT_1:22
.=(MTv|--MT.:A).(MT.Ei) by A2,A6,MATRTOP2:25
.=(MTv|--MT.:A).(ME.i) by A4,A11,FUNCT_1:22
.=(MTv|--ME).i by A10,FUNCT_1:22;
end;
hence thesis by A5,A8,A7,FINSEQ_1:18;
end;
theorem Th20:
for A be Subset of V st A c= Affv & x in Affin Affv holds
x in Affin A
iff
for y be set st y in dom(x|--EV) & not EV.y in A holds (x|--EV).y = 0
proof
let B be Subset of V such that
A1: B c=Affv;
set xA=x|--Affv;
set xB=x|--B;
set cA=card Affv;
set E=EV;
assume A2: x in Affin Affv;
set xE=x|--E;
A3: len xE=cA by Th16;
A4: rng E=Affv by Def1;
then len E=cA by FINSEQ_4:77;
then A5: dom xE=dom E by A3,FINSEQ_3:31;
A6: Carrier xB c=B by RLVECT_2:def 8;
hereby assume x in Affin B;
then A7: xB=xA by A1,RLAFFIN1:77;
let y be set;
assume that
A8: y in dom xE and
A9: not E.y in B;
y in dom E by A8,FUNCT_1:21;
then E.y in Affv by A4,FUNCT_1:def 5;
then reconsider Ey=E.y as Element of V;
xE.y=(x|--Affv).(E.y) & not Ey in Carrier xB by A6,A8,A9,FUNCT_1:22;
hence xE.y=0 by A7,RLVECT_2:28;
end;
assume A10: for y be set st y in dom xE & not E.y in B holds xE.y=0;
A11: now let y be set;
assume A12: y in Affv\B;
then y in Affv by XBOOLE_0:def 5;
then consider z be set such that
A13: z in dom E & E.z=y by A4,FUNCT_1:def 5;
not y in B by A12,XBOOLE_0:def 5;
then xE.z=0 by A5,A10,A13;
hence xA.y=0 by A5,A13,FUNCT_1:22;
end;
Affv\(Affv\B)=Affv/\B by XBOOLE_1:48
.=B by A1,XBOOLE_1:28;
hence thesis by A2,A11,RLAFFIN1:75;
end;
theorem
for EV st x in Affin Affv holds
x in Affin(EV.:Seg k)
iff
x|--EV = ((x|--EV)|k)^((card Affv-' k)|->0)
proof
let E be Enumeration of Affv;
set B=E.:Seg k;
set cA=card Affv;
set cAk=cA-' k;
set xE=x|--E;
set xEk=xE|k;
set cAk0=cAk|->0;
A1: B c=rng E by RELAT_1:144;
assume A2: x in Affin Affv;
then reconsider v=x as Element of V;
A3: len xE=cA by Th16;
A4: rng E=Affv by Def1;
then A5: len E=cA by FINSEQ_4:77;
per cases;
suppose A6: k>cA;
then Seg cA c=Seg k by FINSEQ_1:7;
then dom E c=Seg k by A5,FINSEQ_1:def 3;
then dom E/\Seg k=dom E by XBOOLE_1:28;
then A7: B=E.:dom E by RELAT_1:145;
cA-k<0 by A6,XREAL_1:51;
then cAk=0 by XREAL_0:def 2;
then A8: cAk0 is empty;
xEk=xE by A3,A6,FINSEQ_1:79;
hence thesis by A2,A4,A8,A7,FINSEQ_1:47,RELAT_1:146;
end;
suppose A9: k<=cA;
A10: len cAk0=cAk by CARD_1:def 13;
A11: len xEk=k by A3,A9,FINSEQ_1:80;
cAk=cA-k by A9,XREAL_1:235;
then A12: len(xEk^cAk0)=k+(cA-k) by A11,A10,FINSEQ_1:35;
hereby assume A13: x in Affin B;
now let i be Nat;
assume A14: 1<=i & i<=len xE;
then A15: i in dom xE by FINSEQ_3:27;
A16: i in dom E by A3,A5,A14,FINSEQ_3:27;
A17: i in dom(xEk^cAk0) by A3,A12,A14,FINSEQ_3:27;
per cases by A11,A17,FINSEQ_1:38;
suppose A18: i in dom xEk;
hence (xEk^cAk0).i=xEk.i by FINSEQ_1:def 7
.=xE.i by A18,FUNCT_1:70;
end;
suppose ex n be Nat st n in dom cAk0 & i=k+n;
then consider n be Nat such that
A19: n in dom cAk0 and
A20: i=k+n;
A21: not E.i in B
proof
assume E.i in B;
then consider t be set such that
A22: t in dom E & t in Seg k & E.t=E.i by FUNCT_1:def 12;
i in Seg k by A16,A22,FUNCT_1:def 8;
then A23: i<=k by FINSEQ_1:3;
i>=k by A20,NAT_1:11;
then i=k by A23,XXREAL_0:1;
hence contradiction by A19,A20,FINSEQ_3:27;
end;
cAk0.n=0;
then (xEk^cAk0).i=0 by A11,A19,A20,FINSEQ_1:def 7;
hence xE.i=(xEk^cAk0).i by A2,A1,A4,A13,A15,A21,Th20;
end;
end;
hence xE=xEk^cAk0 by A12,Th16,FINSEQ_1:18;
end;
assume A24: xE=xEk^cAk0;
A25: dom(xEk^cAk0)=dom xE by A3,A12,FINSEQ_3:31;
now let y be set;
assume that
A26: y in dom xE and
A27: not E.y in B;
reconsider i=y as Nat by A26;
i in dom E by A3,A5,A26,FINSEQ_3:31;
then not i in Seg k by A27,FUNCT_1:def 12;
then not i in dom xEk by A11,FINSEQ_1:def 3;
then consider n be Nat such that
A28: n in dom cAk0 & i=k+n by A11,A25,A26,FINSEQ_1:38;
cAk0.n=0;
hence xE.y=0 by A11,A24,A28,FINSEQ_1:def 7;
end;
hence x in Affin B by A2,A1,A4,Th20;
end;
end;
theorem Th22:
for EV st k <= card Affv & x in Affin Affv holds
x in Affin(Affv\(EV.:Seg k))
iff
x|--EV = (k|->0)^((x|--EV)/^k)
proof
let E be Enumeration of Affv;
set cA=card Affv;
set B=E.:Seg k;
set AB=Affv\B;
set xE=x|--E;
set xEk=xE|k;
set xA=x|--Affv;
set k0=k|->0;
A1: AB c=Affv by XBOOLE_1:36;
A2: xE=(xE|k)^(xE/^k) by RFINSEQ:21;
assume A3: k<=card Affv;
then A4: Seg k c=Seg cA by FINSEQ_1:7;
A5: len xE=cA by Th16;
then A6: Seg cA=dom xE by FINSEQ_1:def 3;
A7: rng E=Affv by Def1;
then len E=cA by FINSEQ_4:77;
then A8: dom E=dom xE by A5,FINSEQ_3:31;
assume A9: x in Affin Affv;
A10: len k0=k & len xEk=k by A3,A5,CARD_1:def 13,FINSEQ_1:80;
hereby assume A11: x in Affin AB;
now let i be Nat;
assume 1<=i & i<=k;
then A12: i in Seg k by FINSEQ_1:3;
then E.i in B by A8,A4,A6,FUNCT_1:def 12;
then not E.i in AB by XBOOLE_0:def 5;
then xE.i=0 by A9,A1,A4,A6,A11,A12,Th20;
hence xEk.i=k0.i by A12,FUNCT_1:72;
end;
hence xE=k0^(xE/^k) by A10,A2,FINSEQ_1:18;
end;
assume xE=k0^(xE/^k);
then A13: xEk=k0 by A2,FINSEQ_1:46;
now let y be set;
assume that
A14: y in dom xE and
A15: not E.y in AB;
E.y in Affv by A7,A8,A14,FUNCT_1:def 5;
then E.y in E.:Seg k by A15,XBOOLE_0:def 5;
then consider z be set such that
A16: z in dom E and
A17: z in Seg k and
A18: E.z=E.y by FUNCT_1:def 12;
z=y by A8,A14,A16,A18,FUNCT_1:def 8;
then xEk.y=xE.y by A17,FUNCT_1:72;
hence xE.y=0 by A13;
end;
hence thesis by A9,A1,Th20;
end;
theorem Th23:
0*n in Affn & EN.len EN=0*n implies
rng(EN|(card Affn-' 1)) = Affn\{0*n} &
for A be Subset of n-VectSp_over F_Real st Affn = A holds
EN|(card Affn-' 1) is OrdBasis of Lin A
proof
set A=Affn;
set E=EN;
assume that
A1: 0*n in A and
A2: E.len E=0*n;
A3: card A>=1 by A1,NAT_1:14;
set cA=card A-' 1;
A4: rng E=A by Def1;
cA=card A-1 by A1,NAT_1:14,XREAL_1:235;
then A5: len E=cA+1 by A4,FINSEQ_4:77;
A6: len E=card A by A4,FINSEQ_4:77;
A7: not 0*n in rng(E|cA)
proof
A8: len E in dom E by A6,A3,FINSEQ_3:27;
assume 0*n in rng(E|cA);
then consider x be set such that
A9: x in dom(E|cA) and
A10: (E|cA).x=0*n by FUNCT_1:def 5;
A11: x in Seg cA by A9,RELAT_1:86;
x in dom E & (E|cA).x=E.x by A9,FUNCT_1:70,RELAT_1:86;
then x=cA+1 by A2,A5,A10,A8,FUNCT_1:def 8;
then cA+1<=cA by A11,FINSEQ_1:3;
hence thesis by NAT_1:13;
end;
E=(E|cA)^<*E.len E*> by A5,FINSEQ_3:61;
then A12:A=rng(E|cA)\/rng<*E.len E*> by A4,FINSEQ_1:44
.=rng(E|cA)\/{0*n} by A2,FINSEQ_1:55;
hence A13:A\{0*n} =rng(E|cA) by A7,ZFMISC_1:141;
let A1 be Subset of n-VectSp_over F_Real such that
A14: A=A1;
A1 c=[#]Lin A1
proof
let x be set;
assume x in A1;
then x in Lin A1 by VECTSP_7:13;
hence thesis by STRUCT_0:def 5;
end;
then reconsider e=E as FinSequence of Lin A1 by A4,A14,FINSEQ_1:def 4;
0*n=0.TOP-REAL n by EUCLID:70;
then A\{0*n} is linearly-independent by A1,RLAFFIN1:46;
then A1\{0*n} is linearly-independent by A14,MATRTOP2:7;
then A15: rng(e|cA) is linearly-independent
by A14,A13,VECTSP_9:16;
[#]Lin A1=[#]Lin A by A14,MATRTOP2:6
.=[#]Lin(A\{0.TOP-REAL n}) by Lm2
.=[#]Lin(A\{0*n}) by EUCLID:70
.=[#]Lin(A1\{0*n}) by A14,MATRTOP2:6;
then Lin A1=Lin(A1\{0*n}) by VECTSP_4:37
.=Lin rng(e|cA) by A12,A7,A14,VECTSP_9:21,ZFMISC_1:141;
then (e|cA is one-to-one) & rng(e|cA) is Basis of Lin A1 by A15,FUNCT_1:84
,VECTSP_7:def 3;
hence thesis by MATRLIN:def 4;
end;
X: 0 in REAL by XREAL_0:def 1;
theorem Th24:
for A be Subset of n-VectSp_over F_Real st
Affn = A & 0*n in Affn & EN.len EN = 0*n
for B be OrdBasis of Lin A st B = EN|(card Affn-' 1)
for v be Element of Lin A holds v|--B = (v|--EN)|(card Affn-' 1)
proof
reconsider Z=0 as Element of REAL by X;
set TR=TOP-REAL n;
set A=Affn;
set V=n-VectSp_over F_Real;
set E=EN;
let A1 be Subset of V such that
A1: A=A1 and
A2: 0*n in A and
A3: E.len E=0*n;
deffunc F(set)=Z;
A4: Affin A=[#]Lin A by A2,Th11;
set cA=card A-' 1;
let B be OrdBasis of Lin A1 such that
A5: B=E|cA;
A6: rng B=A\{0*n} by A2,A3,A5,Th23;
then reconsider rB=rng B as Subset of TR;
let v be Element of Lin A1;
set vB=v|--B;
consider KV be Linear_Combination of Lin A1 such that
A7: v=Sum(KV) and
A8: Carrier KV c=rng B and
A9: for k be Nat st 1<=k & k<=len vB holds vB/.k=KV.(B/.k)
by MATRLIN:def 9;
A10: (v|--E)|cA =(v|--A)*(E|cA) by RELAT_1:112;
dom(v|--A)=[#]TR by FUNCT_2:def 1;
then rB c=dom(v|--A);
then A11: len((v|--E)|cA)=len B by A5,A10,FINSEQ_2:33;
A12: [#]Lin A1=[#]Lin A by A1,MATRTOP2:6;
then reconsider RB=rB as Subset of Lin A;
reconsider KR=KV as Linear_Combination of Lin A by A12,MATRTOP2:11;
A13: Carrier KR=Carrier KV by MATRTOP2:12;
consider KR1 be Linear_Combination of TR such that
A14: Carrier KR1=Carrier KR and
A15: Sum KR1=Sum KR by RLVECT_5:12;
rng B c=A by A6,XBOOLE_1:36;
then A16: Carrier KR1 c=A by A8,A13,A14,XBOOLE_1:1;
reconsider KR2=KR1| [#]Lin A as Linear_Combination of Lin A by MATRTOP2:10;
A17: Carrier KR2=Carrier KR1 & Sum KR2=Sum KR1 by A14,RLVECT_5:11;
reconsider KR1 as Linear_Combination of A by A16,RLVECT_2:def 8;
consider KR0 being Function of the carrier of TR,REAL such that
A18: KR0.0.TR=1-sum KR1 and
A19: for u being Element of TR st u<>0.TR holds KR0.u=F(u) from FUNCT_2:sch
6;
reconsider KR0 as Element of Funcs(the carrier of TR,REAL) by FUNCT_2:11;
now let u be VECTOR of TR;
assume not u in {0.TR};
then u<>0.TR by TARSKI:def 1;
hence KR0.u=0 by A19;
end;
then reconsider KR0 as Linear_Combination of TR by RLVECT_2:def 5;
Carrier KR0 c={0.TR}
proof
let x;
assume that
A20: x in Carrier KR0 and
A21: not x in {0.TR};
KR0.x<>0 & x<>0.TR by A20,A21,RLVECT_2:28,TARSKI:def 1;
hence thesis by A19,A20;
end;
then reconsider KR0 as Linear_Combination of{0.TR} by RLVECT_2:def 8;
A22: Carrier KR0 c={0.TR} by RLVECT_2:def 8;
rng B is Basis of Lin A1 by MATRLIN:def 4;
then rng B is linearly-independent by VECTSP_7:def 3;
then rng B is linearly-independent Subset of V by VECTSP_9:15;
then rB is linearly-independent by MATRTOP2:7;
then A23: RB is linearly-independent by RLVECT_5:16;
A24: len vB=len B by MATRLIN:def 9;
A25: Sum KR0=KR0.(0.TR)*0.TR by RLVECT_2:50
.=0.TR by RLVECT_1:23;
A26: 0.TR=0*n by EUCLID:70;
then {0.TR}c=A by A2,ZFMISC_1:37;
then reconsider KR0 as Linear_Combination of A by RLVECT_2:33;
reconsider K=KR1+KR0 as Linear_Combination of A by RLVECT_2:59;
A27: sum K=sum KR1+sum KR0 by RLAFFIN1:34
.=sum KR1+(1-sum KR1) by A18,A22,RLAFFIN1:32
.=1;
Sum K=Sum KR1+Sum KR0 by RLVECT_3:1
.=Sum KR1 by A25,RLVECT_1:def 7
.=v by A7,A15,MATRTOP2:12;
then A28: v|--A=K by A12,A4,A27,RLAFFIN1:def 7;
now let k be Nat;
reconsider Bk=B/.k as Element of TR by A12,RLSUB_1:18;
assume A29: 1<=k & k<=len B;
then A30: vB/.k=KV.Bk & k in dom((v|--E)|cA) by A24,A9,A11,FINSEQ_3:27;
A31: k in dom B by A29,FINSEQ_3:27;
then A32: Bk=B.k by PARTFUN1:def 8;
then Bk in rng B by A31,FUNCT_1:def 5;
then Bk<>0.TR by A6,A26,ZFMISC_1:64;
then not Bk in Carrier KR0 by A22,TARSKI:def 1;
then A33: KR0.Bk=0 by RLVECT_2:28;
k in dom vB by A24,A29,FINSEQ_3:27;
then A34: vB.k=vB/.k by PARTFUN1:def 8;
K.Bk=KR1.Bk+KR0.Bk by RLVECT_2:def 12;
then K.Bk =KR2.Bk by A12,A33,FUNCT_1:72
.=KV.Bk by A23,A8,A13,A14,A15,A17,RLVECT_5:1;
hence ((v|--E)|cA).k=vB.k by A5,A28,A10,A30,A34,A32,FUNCT_1:22;
end;
hence thesis by A24,A11,FINSEQ_1:18;
end;
Lm5: for V be non empty LinearTopSpace for A be finite affinely-independent
Subset of V for E be Enumeration of A for v be Point of V for Ev be Enumeration
of v+A st Ev=E+(card A|->v)for X be set holds transl(v,V).:{u where u is Point
of V:u in Affin A & (u|--E)|k in X}={w where w is Point of V:w in Affin(v+A) &
(w|--Ev)|k in X}
proof
let V be non empty LinearTopSpace;
let A be finite affinely-independent Subset of V;
let E be Enumeration of A;
let v be Point of V;
let Ev be Enumeration of v+A such that
A1: Ev=E+(card A|->v);
set T=transl(v,V);
let X be set;
set U={u where u is Point of V:u in Affin A & (u|--E)|k in X};
set W={w where w is Point of V:w in Affin(v+A) & (w|--Ev)|k in X};
A2: Affin(v+A)=v+Affin A by RLAFFIN1:53;
hereby let y be set;
assume y in T.:U;
then consider x be set such that
x in dom T and
A3: x in U and
A4: T.x=y by FUNCT_1:def 12;
consider u be Point of V such that
A5: x=u and
A6: u in Affin A and
A7: (u|--E)|k in X by A3;
v+u in {v+t where t is Point of V:t in Affin A} by A6;
then A8: v+u in Affin(v+A) by A2,RUSUB_4:def 9;
u|--E=(v+u)|--Ev by A1,A6,Th17;
then v+u in W by A7,A8;
hence y in W by A4,A5,RLTOPSP1:def 10;
end;
let y be set;
assume y in W;
then consider w be Point of V such that
A9: y=w and
A10: w in Affin(v+A) and
A11: (w|--Ev)|k in X;
w in {v+t where t is Point of V:t in Affin A} by A2,A10,RUSUB_4:def 9;
then consider u be Point of V such that
A12: w=v+u and
A13: u in Affin A;
w|--Ev=u|--E by A1,A12,A13,Th17;
then dom T=the carrier of V & u in U by A11,A13,FUNCT_2:67;
then T.u in T.:U by FUNCT_1:def 12;
hence thesis by A9,A12,RLTOPSP1:def 10;
end;
Lm6: for n,k st k<=n for A be non empty finite affinely-independent Subset of
TOP-REAL n st card A=n+1 for E be Enumeration of A st E.len E=0*n for P be
Subset of TOP-REAL k,B be Subset of TOP-REAL n st B={pn:(pn|--E)|k in P} holds
P is open iff B is open
proof
let n,k be Nat such that
A1: k<=n;
set V=n-VectSp_over F_Real;
set TRn=TOP-REAL n;
let A be non empty finite affinely-independent Subset of TRn;
reconsider A1=A as Subset of V by Lm3;
set TRk=TOP-REAL k;
set cA=(card A-' 1);
assume A2: card A=n+1;
dim TRn=n by Th4;
then A3: Affin A=[#]TRn by A2,Th6;
0*n=0.TRn by EUCLID:70;
then A4: Lin(A\{0*n})=Lin A by Lm2;
let E be Enumeration of A;
reconsider e=E as FinSequence of V by Lm3;
A5: rng E=A by Def1;
then A6: len E=card A by FINSEQ_4:77;
n=1 by NAT_1:14;
then len E in dom E by A6,FINSEQ_3:27;
then A10: 0*n in A by A8,A5,FUNCT_1:def 5;
then A11: [#]Lin(A\{0*n})=[#]Lin(A1\{0*n}) & rng(E|cA)=A\{0*n} by A8,Th23,
MATRTOP2:6;
[#]Lin A=[#]Lin A1 by MATRTOP2:6;
then A12: Lin lines M=Lin A1 by A2,A7,A4,A11,VECTSP_4:37;
then reconsider BE=E|cA as OrdBasis of Lin lines M by A8,A10,Th23;
rng BE is Basis of Lin lines M by MATRLIN:def 4;
then rng BE is linearly-independent by VECTSP_7:def 3;
then A13: lines M is linearly-independent by A2,A7,VECTSP_9:15;
BE=M by A2,A7;
then M is one-to-one by MATRLIN:def 4;
then A14: the_rank_of M=n by A13,MATRIX13:121;
then Det M<>0.F_Real by MATRIX13:83;
then A15: M is invertible by LAPLACE:34;
MT is onto by A14,MATRTOP1:41;
then A16: rng MT=the carrier of TRn by FUNCT_2:def 3;
A17: B c=MT.:PP
proof
let x be set;
assume x in B;
then consider v be Element of TRn such that
A18: x=v and
A19: (v|--E)|k in P by A9;
consider f be set such that
A20: f in dom MT & MT.f=v by A16,FUNCT_1:def 5;
len(v|--E)=n+1 by A2,Th16;
then len((v|--E)|n)=n by FINSEQ_1:80,NAT_1:11;
then (v|--E)|n is Element of n-tuples_on REAL by FINSEQ_2:110;
then (v|--E)|n in n-tuples_on REAL;
then (v|--E)|n in REAL n by EUCLID:def 1;
then A21: (v|--E)|n is Element of TRn by EUCLID:25;
reconsider w=v as Element of Lin lines M by A2,A7,A3,A10,A4,A11,Th11;
A22: (v|--E)|n|k=(v|--E)|k by A1,FINSEQ_1:103;
f=w|--BE by A2,A7,A20,MATRTOP2:17
.=(w|--E)|cA by A8,A10,A12,Th24;
then f in PP by A2,A7,A19,A21,A22;
hence thesis by A18,A20,FUNCT_1:def 12;
end;
MT.:PP c=B
proof
let y be set;
assume y in MT.:PP;
then consider x be set such that
x in dom MT and
A23: x in PP and
A24: MT.x=y by FUNCT_1:def 12;
consider f be Element of TRn such that
A25: x=f & f|k in P by A23;
reconsider MTf=MT.f as Element of Lin lines M by A2,A7,A3,A10,A4,A11,Th11;
f=MTf|--BE by A2,A7,MATRTOP2:17
.=(MTf|--E)|cA by A8,A10,A12,Th24;
then f|k =(MTf|--E)|k by A1,A2,A7,FINSEQ_1:103;
hence thesis by A9,A24,A25;
end;
then A26: MT.:PP=B by A17,XBOOLE_0:def 10;
P is open iff PP is open by A1,Th7;
hence thesis by A15,A26,TOPGRP_1:25;
end;
Lm7: for n,k for A be non empty finite affinely-independent Subset of TOP-REAL
n st k=1 by NAT_1:14;
then A6: len E in dom E by FINSEQ_3:27;
then A7: 0*n in rng E by A2,FUNCT_1:def 5;
A8: 0.TRn=0*n by EUCLID:70;
then A9: 0.TRn in A by A2,A3,A6,FUNCT_1:def 5;
then A10: A\{0.TRn} is linearly-independent by RLAFFIN1:46;
card A<=1+dim TRn by Th5;
then c1+1<=1+n by Th4;
then A11: c1<=n by XREAL_1:8;
set nc=n-' c1;
let P be Subset of TOP-REAL k;
let B be Subset of TRn|AA such that
A12: B={v where v is Element of TRn|AA:(v|--E)|k in P};
A13: [#](TRn|AA)=AA by PRE_TOPC:def 10;
consider F be FinSequence such that
A14: rng F=A\{0.TRn} and
A15: F is one-to-one by FINSEQ_4:73;
set V=n-VectSp_over F_Real;
reconsider Bn=MX2FinS 1.(F_Real,n) as OrdBasis of V by MATRLIN2:45;
len Bn=n by MATRTOP1:19;
then reconsider BnC=FinS2MX(Bn|c1) as Matrix of c1,n,F_Real by A11,
FINSEQ_1:80;
reconsider MBC=Mx2Tran BnC as Function;
A20: c1+1=card A;
A21: len F=card(A\{0.TRn}) by A14,A15,FINSEQ_4:77
.=c1 by A9,A20,STIRL2_1:65;
set MBc=Mx2Tran BnC;
set TRc=TOP-REAL c1;
A22: dom MBc=[#]TRc & MBc.0.TRc=0.TRn by FUNCT_2:def 1,MATRTOP1:29;
rng Bn is Basis of V by MATRLIN:def 4;
then rng Bn is linearly-independent by VECTSP_7:def 3;
then A23: rng(Bn|c1) is linearly-independent by RELAT_1:99,VECTSP_7:2;
reconsider F as FinSequence of TRn by A14,FINSEQ_1:def 4;
[#]Lin rng(Bn|len F)c=the carrier of V by VECTSP_4:def 2;
then reconsider BF=[#]Lin rng(Bn|len F) as Subset of TRn by Lm3;
A24: rng MBC=BF by A21,MATRTOP2:18;
consider M be Matrix of n,F_Real such that
A25: M is invertible and
A26: M|len F=F by A10,A14,A15,MATRTOP2:19;
set MTI=Mx2Tran(M~);
A27: [#](TRn|BF)=BF by PRE_TOPC:def 10;
M~ is invertible by A25,MATRIX_6:16;
then A28: Det(M~)<>0.F_Real by LAPLACE:34;
then A29: the_rank_of(M~)=n by MATRIX13:83;
then reconsider MTe=MTI*E as Enumeration of MTI.:A by Th15;
A30: rng MTe=MTI.:A by Def1;
dom MTI=[#]TRn & MTI is one-to-one by A28,FUNCT_2:def 1,MATRTOP1:40;
then A,MTI.:A are_equipotent by CARD_1:60;
then A31: card A=card(MTI.:A) by CARD_1:21;
then len MTe=len E by A4,A30,FINSEQ_4:77;
then len E in dom MTe by A5,FINSEQ_3:27;
then A32: MTe.len E=MTI.(0.TRn) by A2,A8,FUNCT_1:22
.=0.TRn by MATRTOP1:29;
set MT=Mx2Tran M;
Affin A=[#]Lin A by A3,A7,Th11
.=[#]Lin rng F by A14,Lm2;
then A33: MT.:BF=AA by A10,A14,A15,A25,A26,MATRTOP2:21;
then A34: rng(MT|BF)=AA by RELAT_1:148;
A35: dom MT=[#]TRn by FUNCT_2:def 1;
then dom(MT|BF)=BF by RELAT_1:91;
then reconsider MT1=MT|BF as Function of TRn|BF,TRn|AA by A13,A27,A34,
FUNCT_2:3;
reconsider MT as Function;
A36: Det M<>0.F_Real by A25,LAPLACE:34;
then A37: MT"=MTI by MATRTOP1:43;
MT1 is being_homeomorphism by A25,A33,METRIZTS:2;
then A38: MT1"B is open iff B is open by TOPGRP_1:26;
set nc0=nc|->0;
set Vc1={v^nc0 where v is Element of TRc:not contradiction};
A39: nc=n-c1 by A11,XREAL_1:235;
then A40: n=c1+nc;
A41: MT is one-to-one by A36,MATRTOP1:40;
then A42: MT"AA=BF by A33,A35,FUNCT_1:164;
A43: MT"A c=MT"AA by RELAT_1:178,RLAFFIN1:49;
then A44: MTI.:A c=BF by A37,A41,A42,FUNCT_1:155;
Bn is one-to-one by MATRLIN:def 4;
then Bn|c1 is one-to-one by FUNCT_1:84;
then A45: the_rank_of BnC=c1 by A23,MATRIX13:121;
then A46: MBC is one-to-one by MATRTOP1:39;
then A47: dom(MBC")=rng MBC by FUNCT_1:55;
then reconsider MBCe=MBC"*MTe as FinSequence by A24,A30,A44,FINSEQ_1:20;
A48: rng MBCe=MBC".:(MTI.:A) by A30,RELAT_1:160;
MTI.:A is affinely-independent by A29,MATRTOP2:24;
then MBc"(MTI.:A) is affinely-independent by A45,MATRTOP2:27;
then reconsider R=rng MBCe as finite affinely-independent Subset of TRc by
A46,A48,FUNCT_1:155;
reconsider MBCe as Enumeration of R by A46,Def1;
reconsider MBCeE=MBc*MBCe as Enumeration of(Mx2Tran BnC).:R by A45,Th15;
MBC*MBC"=id rng MBC by A46,FUNCT_1:61;
then A49: MBCeE=(id rng MBC)*MTe by RELAT_1:55
.=MTe by A24,A30,A44,RELAT_1:79;
set PPP={v where v is Element of TRc:(v|--MBCe)|k in P};
A50: PPP c=[#]TRc
proof
let x be set;
assume x in PPP;
then ex v be Element of TRc st x=v & (v|--MBCe)|k in P;
hence thesis;
end;
A51: MTI.:A=MT"A by A37,A41,FUNCT_1:155;
A52: MT"B c=MT"AA by A13,RELAT_1:178;
A53: (MTI.:A),R are_equipotent by A24,A46,A47,A44,A48,CARD_1:60;
then A54: c1+1=card R by A31,CARD_1:21;
then A55: k<=c1 & R is non empty by A1,NAT_1:13;
reconsider PPP as Subset of TRc by A50;
set nPP={v where v is Element of TRn:v|c1 in PPP & v in BF};
dim TRc=c1 by Th4;
then A56: Affin R=[#]TRc by A54,Th6;
A57: (Mx2Tran BnC).:R=MBC.:(MBC".:(MTI.:A)) by A30,RELAT_1:160
.=(MBC*MBC").:(MTI.:A) by RELAT_1:159
.=(id rng MBC).:(MTI.:A) by A46,FUNCT_1:61
.=MTI.:A by A51,A42,A43,A24,FUNCT_1:162;
A58: MT"B c=nPP
proof
let x be set;
assume A59: x in MT"B;
then reconsider w=x as Element of TRn|BF
by A33,A27,A35,A41,A52,FUNCT_1:164;
MT.x in B by A59,FUNCT_1:def 13;
then consider v be Element of TRn|AA such that
A60: MT.x=v and
A61: (v|--E)|k in P by A12;
x in dom MT by A59,FUNCT_1:def 13;
then A62: MTI.v=x by A37,A41,A60,FUNCT_1:56;
x in BF by A42,A52,A59;
then reconsider W=x as Element of TRn;
A63: v in AA by A13;
consider u be set such that
A64: u in dom MBc and
A65: MBc.u=w by A42,A52,A24,A59,FUNCT_1:def 5;
A66: W|c1=u by A64,A65,MATRTOP1:38;
reconsider u as Element of TRc by A64;
u|--MBCe =w|--MTe by A65,A57,A49,A45,A56,Th19
.=v|--E by A29,A62,A63,Th19;
then u in PPP by A61;
hence thesis by A42,A52,A59,A66;
end;
A67: BF c=Vc1
proof
let x be set;
assume A68: x in BF;
then reconsider f=x as Element of TRn;
len f=n by CARD_1:def 13;
then len(f|c1)=c1 by A11,FINSEQ_1:80;
then f|c1 is c1-element by CARD_1:def 13;
then A69: f|c1 is Element of TRc by Lm1;
f in Lin rng(Bn|c1) by A21,A68,STRUCT_0:def 5;
then f=(f|c1)^nc0 by MATRTOP2:20;
hence thesis by A69;
end;
Vc1 c=BF
proof
let x be set;
assume x in Vc1;
then consider v be Element of TRc such that
A70: x=v^nc0 and
not contradiction;
len v=c1 by CARD_1:def 13;
then (v^(nc|->0))|c1=(v^(nc|->0))|dom v by FINSEQ_1:def 3
.=v by FINSEQ_1:33;
then v^(nc|->0) in Lin rng(Bn|c1) by A39,MATRTOP2:20;
hence thesis by A21,A70,STRUCT_0:def 5;
end;
then A71: BF=Vc1 by A67,XBOOLE_0:def 10;
A72: nPP c=MT"B
proof
let x be set;
assume x in nPP;
then consider v be Element of TRn such that
A73: x=v and
A74: v|c1 in PPP and
A75: v in BF;
consider v1 be Element of TRc such that
A76: v=v1^nc0 by A71,A75;
consider u be Element of TRc such that
A77: u=v|c1 and
A78: (u|--MBCe)|k in P by A74;
set w=MBc.u;
A79: w=MTI.(MT.w) by A35,A37,A41,FUNCT_1:56;
dom MBc=[#]TRc by FUNCT_2:def 1;
then A80: w in BF by A24,FUNCT_1:def 5;
then A81: MT.w in AA by A33,A35,FUNCT_1:def 12;
u|--MBCe=w|--MBCeE by A45,A56,Th19
.=MT.w|--E by A29,A79,A81,Th19,A57,A49;
then A82: MT.w in B by A12,A13,A78,A81;
consider w1 be Element of TRc such that
A83: w=w1^nc0 by A71,A80;
w1=w|dom w1 by A83,FINSEQ_1:33
.=w|Seg len w1 by FINSEQ_1:def 3
.=w|c1 by CARD_1:def 13
.=v|c1 by A77,MATRTOP1:38
.=v|Seg len v1 by CARD_1:def 13
.=v|dom v1 by FINSEQ_1:def 3
.=v1 by A76,FINSEQ_1:33;
hence thesis by A35,A73,A83,A76,A82,FUNCT_1:def 13;
end;
A84: len MBCe=len E by A4,A54,FINSEQ_4:77;
then len E in dom MBCe by A5,FINSEQ_3:27;
then MBCe.len E=(MBC").(0.TRn) by A32,FUNCT_1:22
.=0.TRc by A46,A22,FUNCT_1:56;
then A85: MBCe.len MBCe=0*c1 by A84,EUCLID:74;
MT1"B=BF/\(MT"B) by FUNCT_1:139
.=MT"B by A13,A42,RELAT_1:178,XBOOLE_1:28;
then MT1"B=nPP by A58,A72,XBOOLE_0:def 10;
then A86: PPP is open iff B is open by A38,A71,A40,Th8;
card R=c1+1 by A31,A53,CARD_1:21;
hence thesis by A85,A86,A55,Lm6;
end;
theorem Th25:
for EN,An st k <= n & card Affn = n+1 & An = {pn:(pn|--EN)|k in Ak}
holds Ak is open iff An is open
proof
set A=Affn;
set AA=Affin A;
set TRn=TOP-REAL n;
let EN,An such that
A1: k<=n and
A2: card A=n+1 and
A3: An={v where v is Element of TRn:(v|--EN)|k in Ak};
set E=EN;
A4: rng E=A by Def1;
then A5: len E=card A by FINSEQ_4:77;
then A6: len E>=1 by A2,NAT_1:14;
then A7: len E in dom E by FINSEQ_3:27;
then E.(len E) in A by A4,FUNCT_1:def 5;
then reconsider EL=E.(len E) as Element of TRn;
A8: card(-EL+A)=n+1 by A2,RLAFFIN1:7;
set BB={u where u is Element of TRn:u in AA & (u|--E)|k in Ak};
A9: BB c=An
proof
let x be set;
assume x in BB;
then ex u be Element of TRn st x=u & u in AA & (u|--E)|k in Ak;
hence thesis by A3;
end;
reconsider Ev=E+(card A|->-EL) as Enumeration of-EL+A by Th13;
set TB={w where w is Element of TRn:(w|--Ev)|k in Ak};
set T=transl(-EL,TRn);
A10: dim TRn=n by Th4;
then A11: [#]TRn=AA by A2,Th6;
An c=BB
proof
let x be set;
assume x in An;
then consider v be Element of TRn such that
A12: x=v & (v|--E)|k in Ak by A3;
thus thesis by A11,A12;
end;
then BB=An by A9,XBOOLE_0:def 10;
then A13: T.:An={w where w is Element of TRn:w in Affin(-EL+A) & (w|--Ev)|k
in Ak} by Lm5;
A14: T.:An c=TB
proof
let x be set;
assume x in T.:An;
then ex w be Element of TRn st x=w & w in Affin(-EL+A) & (w|--Ev)|k in Ak
by A13;
hence thesis;
end;
A15: card(-EL+A)=card A by RLAFFIN1:7;
then A16: Affin(-EL+A)=[#]TRn by A2,A10,Th6;
TB c=T.:An
proof
let x be set;
assume x in TB;
then consider w be Element of TRn such that
A17: x=w & (w|--Ev)|k in Ak;
thus thesis by A16,A13,A17;
end;
then A18: T.:An=TB by A14,XBOOLE_0:def 10;
len E in Seg card A by A5,A6;
then A19: (card A|->-EL).len E=-EL by FINSEQ_2:71;
A20: rng Ev=-EL+A by Def1;
then len Ev=card A by A15,FINSEQ_4:77;
then dom E=dom Ev by A5,FINSEQ_3:31;
then Ev.len E=EL+(-EL) by A7,A19,FVSUM_1:21
.=0.TRn by RLVECT_1:16
.=0*n by EUCLID:74;
then A21: Ev.len Ev=0*n by A5,A15,A20,FINSEQ_4:77;
-EL+A is non empty by A2,A15;
then T.:An is open iff Ak is open by A1,A21,A8,A18,Lm6;
hence thesis by TOPGRP_1:25;
set TAA=T.:AA;
A22: rng(T|AA)=T.:AA by RELAT_1:148;
dom T=[#]TRn by FUNCT_2:67;
then A23: dom(T|AA)=AA by RELAT_1:91;
[#](TRn|AA)=AA & [#](TRn|TAA)=TAA by PRE_TOPC:def 10;
then reconsider TA=T|AA as Function of TRn|AA,TRn|TAA by A23,A22,FUNCT_2:3;
reconsider TAB=TA.:An as Subset of TRn|TAA;
reconsider TAB=TA.:An as Subset of TRn|TAA;
end;
theorem Th26:
for EN st k <=n & card Affn = n+1 & An = {pn:(pn|--EN)|k in Ak}
holds Ak is closed iff An is closed
proof
set TRn=TOP-REAL n;
set TRk=TOP-REAL k;
set A=Affn;
let E be Enumeration of A such that
A1: k<=n & card A=n+1 and
A2: An={v where v is Element of TRn:(v|--E)|k in Ak};
set B1={v where v is Element of TRn:(v|--E)|k in Ak`};
A3: k closed Subset of TOP-REAL n;
coherence
proof
set TRn=TOP-REAL n;
let A be Subset of TRn;
assume A is Affine;
then A1: Affin A=A by RLAFFIN1:50;
per cases;
suppose A is empty;
hence thesis;
end;
suppose A2: A is non empty;
{}TRn c=A by XBOOLE_1:2;
then consider Ia be affinely-independent Subset of TRn such that
{}c=Ia and
Ia c=A and
A3: Affin Ia=A by A1,RLAFFIN1:60;
consider IA be affinely-independent Subset of TRn such that
A4: Ia c=IA and
IA c=[#]TRn and
A5: Affin IA=Affin[#]TRn by RLAFFIN1:60;
reconsider IB=IA\Ia as affinely-independent Subset of TRn by RLAFFIN1:43
,XBOOLE_1:36;
set cIB=card IB;
A6: dim TRn=n by Th4;
then A7: cIB<=n+1 by Th5;
[#]TRn is Affine by RUSUB_4:22;
then A8: Affin[#]TRn=[#]TRn by RLAFFIN1:50;
then A9: card IA=n+1 by A5,A6,Th6;
Ia is non empty by A2,A3;
then IA meets Ia by A4,XBOOLE_1:67;
then IA<>IB by XBOOLE_1:83;
then cIB<>n+1 by A9,CARD_FIN:1,XBOOLE_1:36;
then A10: cIB0 is Element of TRc by EUCLID:def 4;
then reconsider P={cIB|->0} as Subset of TRc by ZFMISC_1:37;
0*cIB=cIB|->0 by EUCLID:def 4;
then A13: P is closed by A12,PCOMPS_1:10;
set P1=the Enumeration of Ia;
A14: rng P1=Ia by Def1;
set P2=the Enumeration of IB;
set P12=P2^P1;
A15: rng P2=IB by Def1;
Ia misses IB by XBOOLE_1:79;
then A16: P12 is one-to-one by A14,A15,FINSEQ_3:98;
Ia\/IB=Ia\/IA by XBOOLE_1:39
.=IA by A4,XBOOLE_1:12;
then rng P12=IA by A14,A15,FINSEQ_1:44;
then reconsider P12 as Enumeration of IA by A16,Def1;
len P2=card IB by A15,FINSEQ_4:77;
then A17: P12.:(Seg cIB)=P12.:dom P2 by FINSEQ_1:def 3
.=rng(P12|dom P2) by RELAT_1:148
.=rng P2 by FINSEQ_1:33
.=IB by Def1;
set B={v where v is Element of TRn:(v|--P12)|cIB in P};
A18: IA\IB=IA/\Ia by XBOOLE_1:48
.=Ia by A4,XBOOLE_1:28;
A19: Affin A c=B
proof
let x be set;
assume A20: x in Affin A;
then reconsider v=x as Element of TRn;
set vP=v|--P12;
A21: vP=(vP|cIB)^(vP/^cIB) by RFINSEQ:21;
vP=(cIB|->0)^(vP/^cIB) by A1,A3,A5,A8,A18,A17,A11,A20,Th22;
then vP|cIB=cIB|->0 by A21,FINSEQ_1:46;
then vP|cIB in P by TARSKI:def 1;
hence thesis;
end;
A22: cIB<=n by A10,NAT_1:13;
B c=Affin A
proof
let x be set;
assume x in B;
then consider v be Element of TRn such that
A23: x=v and
A24: (v|--P12)|cIB in P;
set vP=v|--P12;
vP|cIB=cIB|->0 by A24,TARSKI:def 1;
then vP=(cIB|->0)^(vP/^cIB) by RFINSEQ:21;
hence thesis by A1,A3,A5,A8,A18,A17,A11,A23,Th22;
end;
then B=Affin A by A19,XBOOLE_0:def 10;
hence thesis by A1,A9,A22,A13,Th26;
end;
end;
end;
reserve pnA for Element of(TOP-REAL n)|Affin Affn;
theorem Th27:
for EN for B be Subset of (TOP-REAL n)|Affin Affn st
k < card Affn & B = {pnA: (pnA|--EN) |k in Ak}
holds Ak is open iff B is open
proof
let EN;
set E=EN;
set Tn=TOP-REAL n,Tk=TOP-REAL k;
set A=Affn;
set cA=card A-' 1;
set TcA=TOP-REAL cA;
set AA=Affin A;
let B be Subset of Tn|AA such that
A1: k=1 by A1,NAT_1:14;
then A12: len E in dom E by FINSEQ_3:27;
then E.(len E) in A by A9,FUNCT_1:def 5;
then reconsider EL=E.(len E) as Element of Tn;
len E in Seg card A by A10,A11;
then A13: (card A|->-EL).len E=-EL by FINSEQ_2:71;
A14: k-EL) as Enumeration of-EL+A by Th13;
A19: card(-EL+A)=card A by RLAFFIN1:7;
then A20: (-EL+A) is non empty by A1;
A21: rng Ev=-EL+A by Def1;
then len Ev=card A by A19,FINSEQ_4:77;
then dom E=dom Ev by A10,FINSEQ_3:31;
then Ev.len E=EL+(-EL) by A12,A13,FVSUM_1:21
.=0.Tn by RLVECT_1:16
.=0*n by EUCLID:74;
then A22: Ev.len Ev=0*n by A10,A19,A21,FINSEQ_4:77;
set Tab={w where w is Element of Tn|TAA:(w|--Ev)|k in Ak};
A23: -EL+AA=Affin(-EL+A) by RLAFFIN1:53;
then A24: T.:AA=Affin(-EL+A) by RLTOPSP1:34;
TA.:B=T.:B by A3,RELAT_1:162;
then A25: TAB={w where w is Element of Tn:w in Affin(-EL+A) & (w|--Ev)|k in
Ak} by A8,Lm5;
A26: TAB c=Tab
proof
let x be set;
assume x in TAB;
then consider w be Element of Tn such that
A27: x=w and
A28: w in Affin(-EL+A) and
A29: (w|--Ev)|k in Ak by A25;
w in TAA by A23,A28,RLTOPSP1:34;
hence thesis by A15,A27,A29;
end;
A30: T.:AA is non empty by A6,A17,RELAT_1:152;
Tab c=TAB
proof
let x be set;
assume x in Tab;
then consider w be Element of Tn|TAA such that
A31: x=w & (w|--Ev)|k in Ak;
w in TAA by A15,A30;
hence thesis by A24,A25,A31;
end;
then TAB=Tab by A26,XBOOLE_0:def 10;
then TAB is open iff Ak is open by A24,A22,A14,A20,Lm7;
hence thesis by A6,A18,A30,TOPGRP_1:25;
end;
theorem Th28:
for EN for B be Subset of (TOP-REAL n)|Affin Affn st
k < card Affn & B = {pnA: (pnA|--EN)|k in Ak}
holds Ak is closed iff B is closed
proof
let E be Enumeration of Affn;
set TRn=TOP-REAL n;
set A=Affn;
set AA=Affin A;
let B be Subset of TRn|AA such that
A1: k closed;
coherence
proof
set pq={p,q};
A1: n in NAT by ORDINAL1:def 13;
per cases;
suppose A2: p=q;
{p} is closed by URYSOHN1:27;
hence thesis by A1,A2,TOPREAL9:29;
end;
suppose A3: p<>q;
A4: rng<*p,q*>=pq by FINSEQ_2:147;
<*p,q*> is one-to-one by A3,FINSEQ_3:103;
then reconsider E=<*p,q*> as Enumeration of pq by A4,Def1;
set Apq=Affin pq;
set TRn=TOP-REAL n,TR1=TOP-REAL 1;
set L=].-infty,1 .];
A5: E.1=p by FINSEQ_1:61;
reconsider L as Subset of R^1 by TOPMETR:24;
consider h be Function of TR1,R^1 such that
A6: for p be Point of TR1 holds h.p=p/.1 by JORDAN2B:1;
set B={w where w is Element of TRn|Apq:(w|--E)|1 in h"L};
B c=[#](TRn|Apq)
proof
let x be set;
assume x in B;
then ex w be Element of TRn|Apq st x=w & (w|--E)|1 in h"L;
hence thesis;
end;
then reconsider B as Subset of TRn|Apq;
A7: [#](TRn|Apq)=Apq by PRE_TOPC:def 10;
A8: card pq=2 by A3,CARD_2:76;
A9: h is being_homeomorphism by A6,JORDAN2B:34;
then A10: dom h=[#]TR1 by TOPGRP_1:24;
A11: halfline(p,q)c=B
proof
Carrier(q|--{q})c={q} by RLVECT_2:def 8;
then not p in Carrier(q|--{q}) by A3,TARSKI:def 1;
then A12: (q|--{q}).p=0 by RLVECT_2:28;
{q} is Affine by RUSUB_4:23;
then A13: Affin{q}={q} by RLAFFIN1:50;
let x;
set W=x|--pq,wE=x|--E;
A14: p in pq by TARSKI:def 2;
assume x in halfline(p,q);
then consider a be real number such that
A15: x=(1-a)*p+a*q and
A16: 0<=a by A1,TOPREAL9:26;
reconsider a as Real by XREAL_0:def 1;
q in {q} & {q}c=pq by TARSKI:def 1,ZFMISC_1:42;
then 0=(q|--pq).p by A12,A13,RLAFFIN1:77;
then A17: (a*(q|--pq)).p=a*0 by RLVECT_2:def 13
.=0;
pq c=conv pq by CONVEX1:41;
then A18: (p|--pq).p=1 by A14,RLAFFIN1:72;
A19: q in pq & pq c=Affin pq by RLAFFIN1:49,TARSKI:def 2;
then W=(1-a)*(p|--pq)+a*(q|--pq) by A15,A14,RLAFFIN1:70;
then W.p=((1-a)*(p|--pq)).p+(a*(q|--pq)).p by RLVECT_2:def 12
.=(1-a)*((p|--pq).p)+0 by A17,RLVECT_2:def 13
.=1-a by A18;
then W.p<=1-0 by A16,XREAL_1:12;
then A20: W.p in L by XXREAL_1:234;
(1-a)+a=1;
then reconsider w=x as Element of TRn|Apq by A7,A15,A14,A19,RLAFFIN1:78;
len wE=2 by A8,Th16;
then A21: len(wE|1)=1 by FINSEQ_1:80;
then reconsider wE1=wE|1 as Point of TOP-REAL 1 by TOPREAL7:18;
A22: 1 in dom wE1 by A21,FINSEQ_3:27;
then A23: wE1/.1=wE1.1 & wE1.1=wE.1 by FUNCT_1:70,PARTFUN1:def 8;
A24: 1 in dom wE by A22,RELAT_1:86;
h.wE1=wE1/.1 by A6;
then h.wE1 in L by A5,A20,A23,A24,FUNCT_1:22;
then wE1 in h"L by A10,FUNCT_1:def 13;
then w in B;
hence thesis;
end;
L is closed by BORSUK_5:65;
then h"L is closed by A9,TOPGRP_1:24;
then A25: B is closed by A8,Th28;
B c=halfline(p,q)
proof
let x;
assume x in B;
then consider w be Element of TRn|Apq such that
A26: x=w and
A27: (w|--E)|1 in h"L;
set W=w|--pq,wE=w|--E;
reconsider wE1=wE|1 as Point of TR1 by A27;
A28: h.wE1=wE1/.1 by A6;
len wE1=1 by CARD_1:def 13;
then A29: 1 in dom wE1 by FINSEQ_3:27;
then A30: wE1/.1=wE1.1 & wE1.1=wE.1 by FUNCT_1:70,PARTFUN1:def 8;
A31: 1 in dom wE by A29,RELAT_1:86;
h.(wE|1) in L by A27,FUNCT_1:def 13;
then W.p in L by A5,A28,A30,A31,FUNCT_1:22;
then W.p<=1 by XXREAL_1:234;
then A32: W.p-W.p<=1-W.p by XREAL_1:11;
A33: sum W=1 by A7,RLAFFIN1:def 7;
Carrier W c=pq by RLVECT_2:def 8;
then A34: sum W=W.p+W.q by A3,RLAFFIN1:33;
Sum W=w by A7,RLAFFIN1:def 7;
then w=(1-W.q)*p+W.q*q by A3,A34,A33,RLVECT_2:51;
hence thesis by A1,A26,A34,A33,A32,TOPREAL9:26;
end;
then halfline(p,q)=B by A11,XBOOLE_0:def 10;
hence thesis by A7,A25,TSEP_1:8;
end;
end;
end;
begin :: Continuity of Barycentric Coordinates
definition
let V;
let A be Subset of V,x;
func |--(A,x) -> Function of V,R^1 means :Def3:
it.v = (v|--A).x;
existence
proof
deffunc F(set)=($1|--A).x;
A1: for v be set st v in the carrier of V holds F(v) in the carrier of R^1
proof
let v be set such that
v in the carrier of V;
set vA=v|--A;
per cases;
suppose x in dom vA;
then vA.x in rng vA by FUNCT_1:def 5;
hence thesis by TOPMETR:24;
end;
suppose not x in dom vA;
then vA.x=0 by FUNCT_1:def 4;
hence thesis by X,TOPMETR:24;
end;
end;
consider f being Function of V,R^1 such that
A2: for v be set st v in the carrier of V holds f.v=F(v) from FUNCT_2:sch 2
(A1);
take f;
let v be Element of V;
thus thesis by A2;
end;
uniqueness
proof
let F1,F2 be Function of V,R^1 such that
A3: for v be Element of V holds F1.v=(v|--A).x and
A4: for v be Element of V holds F2.v=(v|--A).x;
now let v be set;
assume A5: v in the carrier of V;
hence F1.v=(v|--A).x by A3
.=F2.v by A4,A5;
end;
hence thesis by FUNCT_2:18;
end;
end;
theorem Th29:
for A be Subset of V st not x in A holds |--(A,x) = [#]V-->0
proof
let A be Subset of V;
set Ax=|--(A,x);
assume A1: not x in A;
A2: now let y be set;
assume y in dom Ax;
then A3: Ax.y=(y|--A).x by Def3;
Carrier(y|--A)c=A by RLVECT_2:def 8;
then A4: not x in Carrier(y|--A) by A1;
per cases;
suppose x in [#]V;
hence Ax.y=0 by A3,A4,RLVECT_2:28;
end;
suppose not x in [#]V;
then not x in dom(y|--A);
hence Ax.y=0 by A3,FUNCT_1:def 4;
end;
end;
dom Ax=[#]V by FUNCT_2:def 1;
hence thesis by A2,FUNCOP_1:17;
end;
theorem
for A be affinely-independent Subset of V st |--(A,x) = [#]V-->0
holds not x in A
proof
let A be affinely-independent Subset of V;
set Ax=|--(A,x);
assume A1: |--(A,x)=[#]V-->0;
A2: A c=conv A by RLAFFIN1:2;
assume A3: x in A;
then 0=Ax.x by A1,FUNCOP_1:13
.=(x|--A).x by A3,Def3
.=1 by A3,A2,RLAFFIN1:72;
hence contradiction;
end;
theorem Th31:
|--(Affn,x)|Affin Affn is continuous Function of (TOP-REAL n)|Affin Affn,R^1
proof
reconsider Z=0 as Element of R^1 by X,TOPMETR:24;
set TRn=TOP-REAL n;
set AA=Affin Affn;
set Ax=|--(Affn,x);
set AxA=Ax|AA;
A1: [#]TRn/\AA=AA by XBOOLE_1:28;
A2: AA=[#](TRn|AA) by PRE_TOPC:def 10;
then reconsider AxA as Function of TRn|AA,R^1 by FUNCT_2:38;
A3: dom AxA=AA by A2,FUNCT_2:def 1;
per cases;
suppose not x in Affn;
then Ax=[#]TRn-->Z by Th29;
then AxA =(TRn|AA)-->Z by A2,A1,FUNCOP_1:18;
hence thesis;
end;
suppose A4: x in Affn & card Affn=1;
A5: rng AxA c=the carrier of R^1 by RELAT_1:def 19;
consider y be set such that
A6: Affn={y} by A4,CARD_2:60;
A7: x=y by A4,A6,TARSKI:def 1;
then Affn is Affine by A4,A6,RUSUB_4:23;
then A8: AA=Affn by RLAFFIN1:50;
then AxA.x in rng AxA by A3,A4,FUNCT_1:def 5;
then reconsider b=AxA.x as Element of R^1 by A5;
rng AxA={AxA.x} by A3,A6,A7,A8,FUNCT_1:14;
then AxA =(TRn|AA)-->b by A2,A3,FUNCOP_1:15;
hence thesis;
end;
suppose A9: x in Affn & card Affn<>1;
set P2=the Enumeration of Affn\{x};
set P1=<*x*>;
set P12=P1^P2;
A10: rng P1={x} & rng P2=Affn\{x} by Def1,FINSEQ_1:56;
(P1 is one-to-one) & {x}misses Affn\{x} by FINSEQ_3:102,XBOOLE_1:79;
then A11: P12 is one-to-one by A10,FINSEQ_3:98;
rng P12=rng P1\/rng P2 by FINSEQ_1:44;
then rng P12=Affn by A9,A10,ZFMISC_1:140;
then reconsider P12 as Enumeration of Affn by A11,Def1;
set TR1=TOP-REAL 1;
consider Pro being Function of TR1,R^1 such that
A12: for p being Element of TR1 holds Pro.p=p/.1 by JORDAN2B:1;
A13: Pro is being_homeomorphism by A12,JORDAN2B:34;
card Affn>=1 by A9,NAT_1:14;
then A14: card Affn>1 by A9,XXREAL_0:1;
now A15: dom P1 c=dom P12 by FINSEQ_1:39;
let P be Subset of R^1;
set B={v where v is Element of TRn|AA:(v|--P12)|1 in Pro"P};
A16: 1 in {1} by FINSEQ_1:4;
assume P is closed;
then A17: Pro"P is closed by A13,TOPGRP_1:24;
A18: dom P1=Seg 1 by FINSEQ_1:55;
then A19: P12.1=P1.1 by A16,FINSEQ_1:4,def 7
.=x by FINSEQ_1:57;
A20: AA is non empty by A9;
A21: B c=AxA"P
proof
let y be set;
assume y in B;
then consider v be Element of TRn|AA such that
A22: y=v and
A23: (v|--P12)|1 in Pro"P;
set vP=v|--P12;
reconsider vP1=vP|1 as Element of TR1 by A23;
A24: v in AA by A2,A20;
len vP1=1 by CARD_1:def 13;
then dom vP1=Seg 1 by FINSEQ_1:def 3;
then A25: 1 in dom vP1;
then A26: 1 in dom vP by RELAT_1:86;
Pro.vP1=vP1/.1 by A12
.=vP1.1 by A25,PARTFUN1:def 8
.=vP.1 by A25,FUNCT_1:70
.=(v|--Affn).x by A19,A26,FUNCT_1:22
.=Ax.v by A24,Def3;
then Ax.v in P by A23,FUNCT_1:def 13;
then AxA.v in P by A2,A3,A9,FUNCT_1:70;
hence thesis by A2,A3,A9,A22,FUNCT_1:def 13;
end;
A27: dom Pro=[#]TR1 by A13,TOPGRP_1:24;
AxA"P c=B
proof
let y be set;
set yP=y|--P12;
len yP=card Affn by Th16;
then A28: len(yP|1)=1 by A9,FINSEQ_1:80,NAT_1:14;
then reconsider yP1=yP|1 as Element of TR1 by TOPREAL7:18;
A29: dom yP1=Seg 1 by A28,FINSEQ_1:def 3;
assume A30: y in AxA"P;
then A31: y in dom AxA by FUNCT_1:def 13;
then AxA.y=Ax.y by FUNCT_1:70
.=(y|--Affn).(P12.1) by A19,A3,A31,Def3
.=yP.1 by A18,A16,A15,FINSEQ_1:4,FUNCT_1:23
.=yP1.1 by A16,A29,FINSEQ_1:4,FUNCT_1:70
.=yP1/.1 by A16,A29,FINSEQ_1:4,PARTFUN1:def 8
.=Pro.yP1 by A12;
then Pro.yP1 in P by A30,FUNCT_1:def 13;
then yP1 in Pro"P by A27,FUNCT_1:def 13;
hence thesis by A30;
end;
then B=AxA"P by A21,XBOOLE_0:def 10;
hence AxA"P is closed by A14,A17,Th28;
end;
hence thesis by PRE_TOPC:def 12;
end;
end;
theorem Th32:
card Affn = n+1 implies |--(Affn,x) is continuous
proof
set TRn=TOP-REAL n;
set AA=Affin Affn;
set Ax=|--(Affn,x);
reconsider AxA=Ax|AA as continuous Function of TRn|AA,R^1 by Th31;
assume A1: card Affn=n+1;
dim TRn=n by Th4;
then A2: AA=[#]TRn by A1,Th6;
then A3: TRn|AA=the TopStruct of TRn by TSEP_1:100;
A4: dom Ax=AA by A2,FUNCT_2:def 1;
now let P be Subset of R^1;
assume P is closed;
then AxA"P is closed by PRE_TOPC:def 12;
then A5: (AxA"P)` in the topology of the TopStruct of TRn by A3,
PRE_TOPC:def 5;
(AxA"P)`=(Ax"P)` by A4,A3,RELAT_1:98;
then (Ax"P)` is open by A5,PRE_TOPC:def 5;
hence Ax"P is closed by TOPS_1:29;
end;
hence thesis by PRE_TOPC:def 12;
end;
Lm8: for A be affinely-independent Subset of TOP-REAL n st card A=n+1 holds
conv A is closed
proof
set L=[.0,1 .];
set TRn=TOP-REAL n;
let A be affinely-independent Subset of TRn;
assume A1: card A=n+1;
reconsider L as Subset of R^1 by TOPMETR:24;
set E=the Enumeration of A;
deffunc F(set)=|--(A,E.$1)"L;
consider f be FinSequence such that
A2: len f=n+1 and
A3: for k be Nat st k in dom f holds f.k=F(k) from FINSEQ_1:sch 2;
A4: dom f=Seg len f by FINSEQ_1:def 3;
then A5: rng f is non empty by A2,RELAT_1:65;
rng f c=bool the carrier of TRn
proof
let y be set;
assume y in rng f;
then consider x be set such that
A6: x in dom f and
A7: f.x=y by FUNCT_1:def 5;
f.x=F(x) by A3,A6;
hence thesis by A7;
end;
then reconsider f as FinSequence of bool the carrier of TRn by FINSEQ_1:def 4
;
A8: rng E=A by Def1;
then A9: len E=card A by FINSEQ_4:77;
A10: meet rng f c=conv A
proof
let x be set;
assume A11: x in meet rng f;
A12: now let v be Element of TRn;
assume v in A;
then consider k be set such that
A13: k in dom E and
A14: E.k=v by A8,FUNCT_1:def 5;
A15: k in dom f by A1,A2,A9,A4,A13,FINSEQ_1:def 3;
then f.k in rng f by FUNCT_1:def 5;
then A16: meet rng f c=f.k by SETFAM_1:4;
A17: (x|--A).v=|--(A,v).x by A11,Def3;
f.k=|--(A,v)"L by A3,A14,A15;
then (x|--A).v in L by A11,A17,A16,FUNCT_1:def 13;
hence (x|--A).v>=0 by XXREAL_1:1;
end;
dim TRn=n by Th4;
then [#]TRn=Affin A by A1,Th6;
hence thesis by A11,A12,RLAFFIN1:73;
end;
A18: dom E=Seg len E by FINSEQ_1:def 3;
A19: conv A c=meet rng f
proof
let x be set;
assume A20: x in conv A;
now let Y be set;
assume Y in rng f;
then consider k be set such that
A21: k in dom f and
A22: f.k=Y by FUNCT_1:def 5;
E.k in A by A1,A2,A8,A9,A4,A18,A21,FUNCT_1:def 5;
then reconsider Ek=E.k as Element of TRn;
A23: dom|--(A,Ek)=[#]TRn by FUNCT_2:def 1;
A24: 0<=(x|--A).Ek & (x|--A).Ek<=1 by A20,RLAFFIN1:71;
(x|--A).Ek=|--(A,Ek).x by A20,Def3;
then A25: |--(A,Ek).x in L by A24,XXREAL_1:1;
Y=|--(A,E.k)"L by A3,A21,A22;
hence x in Y by A20,A25,A23,FUNCT_1:def 13;
end;
hence thesis by A5,SETFAM_1:def 1;
end;
now let B be Subset of TRn;
assume B in rng f;
then consider k be set such that
A26: k in dom f & f.k=B by FUNCT_1:def 5;
(|--(A,E.k) is continuous) & L is closed by A1,Th32,TREAL_1:4;
then |--(A,E.k)"L is closed by PRE_TOPC:def 12;
hence B is closed by A3,A26;
end;
then rng f is closed by TOPS_2:def 2;
then meet rng f is closed by TOPS_2:29;
hence thesis by A19,A10,XBOOLE_0:def 10;
end;
registration
let n,Affn;
cluster conv Affn -> closed;
coherence
proof
set TRn=TOP-REAL n;
consider I be affinely-independent Subset of TRn such that
A1: Affn c=I and
I c=[#]TRn and
A2: Affin I=Affin[#]TRn by RLAFFIN1:60;
A3: dim TRn=n by Th4;
[#]TRn is Affine by RUSUB_4:22;
then Affin I=[#]TRn by A2,RLAFFIN1:50;
then card I=n+1 by A3,Th6;
then conv I is closed by Lm8;
then conv I/\Affin Affn is closed;
hence thesis by A1,Th9;
end;
end;
theorem
card Affn = n+1 implies Int Affn is open
proof
set L=].0,1 .[;
set TRn=TOP-REAL n;
set A=Affn;
assume that
A1: card A=n+1;
per cases;
suppose A2:n<>0;
reconsider L as Subset of R^1 by TOPMETR:24;
set E=the Enumeration of A;
deffunc F(set)=|--(A,E.$1)"L;
consider f be FinSequence such that
A3: len f=n+1 and
A4: for k be Nat st k in dom f holds f.k=F(k) from FINSEQ_1:sch 2;
A5: dom f=Seg len f by FINSEQ_1:def 3;
then A6: rng f is non empty by A3,RELAT_1:65;
rng f c=bool the carrier of TRn
proof
let y be set;
assume y in rng f;
then consider x be set such that
A7: x in dom f and
A8: f.x=y by FUNCT_1:def 5;
f.x=F(x) by A4,A7;
hence thesis by A8;
end;
then reconsider f as FinSequence of bool the carrier of TRn by FINSEQ_1:def 4
;
A9: rng E=A by Def1;
then A10: len E=card A by FINSEQ_4:77;
A11: meet rng f c=Int A
proof
let x be set;
dim TRn=n by Th4;
then A12: [#]TRn=Affin A by A1,Th6;
assume A13: x in meet rng f;
A14: now let v be Element of TRn;
assume v in A;
then consider k be set such that
A15: k in dom E and
A16: E.k=v by A9,FUNCT_1:def 5;
A17: k in dom f by A1,A3,A10,A5,A15,FINSEQ_1:def 3;
then f.k in rng f by FUNCT_1:def 5;
then A18: meet rng f c=f.k by SETFAM_1:4;
A19: (x|--A).v=|--(A,v).x by A13,Def3;
f.k=|--(A,v)"L by A4,A16,A17;
then (x|--A).v in L by A13,A19,A18,FUNCT_1:def 13;
hence (x|--A).v>0 by XXREAL_1:4;
end;
A20: A c=Carrier(x|--A)
proof
let y be set;
assume A21: y in A;
then (x|--A).y>0 by A14;
hence thesis by A21,RLVECT_2:28;
end;
Carrier(x|--A)c=A by RLVECT_2:def 8;
then A22: Carrier(x|--A)=A by A20,XBOOLE_0:def 10;
for v be Element of TRn st v in A holds(x|--A).v>=0 by A14;
then A23: x in conv A by A13,A12,RLAFFIN1:73;
Sum(x|--A)=x by A13,A12,RLAFFIN1:def 7;
hence thesis by A23,A22,RLAFFIN1:71,RLAFFIN2:12;
end;
A24: conv A c=Affin A by RLAFFIN1:65;
A25: Int A c=conv A by RLAFFIN2:5;
A26: dom E=Seg len E by FINSEQ_1:def 3;
A27: Int A c=meet rng f
proof
let x be set;
assume A28: x in Int A;
then consider K be Linear_Combination of A such that
A29: K is convex and
A30: x=Sum K by RLAFFIN2:10;
A31: x in conv A by A25,A28;
sum K=1 by A29,RLAFFIN1:62;
then A32: K=x|--A by A24,A30,A31,RLAFFIN1:def 7;
A33: Carrier K=A by A28,A29,A30,RLAFFIN2:11;
now let Y be set;
assume Y in rng f;
then consider k be set such that
A34: k in dom f and
A35: f.k=Y by FUNCT_1:def 5;
A36: E.k in A by A1,A3,A9,A10,A5,A26,A34,FUNCT_1:def 5;
then reconsider Ek=E.k as Element of TRn;
(x|--A).Ek<>0 by A32,A33,A36,RLVECT_2:28;
then A37: 0<(x|--A).Ek by A29,A32,RLAFFIN1:62;
A38: (x|--A).Ek<1
proof
assume A39: (x|--A).Ek>=1;
(x|--A).Ek<=1 by A29,A32,RLAFFIN1:63;
then A={Ek} by A29,A32,A33,A39,RLAFFIN1:64,XXREAL_0:1;
then card A=1 by CARD_2:60;
hence contradiction by A1,A2;
end;
(x|--A).Ek=|--(A,Ek).x by A30,Def3;
then A40: |--(A,Ek).x in L by A38,A37,XXREAL_1:4;
A41: dom|--(A,Ek)=[#]TRn by FUNCT_2:def 1;
Y=|--(A,E.k)"L by A4,A34,A35;
hence x in Y by A28,A40,A41,FUNCT_1:def 13;
end;
hence thesis by A6,SETFAM_1:def 1;
end;
now let B be Subset of TRn;
A42: [#]R^1 is non empty;
assume B in rng f;
then consider k be set such that
A43: k in dom f & f.k=B by FUNCT_1:def 5;
(|--(A,E.k) is continuous) & L is open by A1,Th32,JORDAN6:46;
then |--(A,E.k)"L is open by A42,TOPS_2:55;
hence B is open by A4,A43;
end;
then rng f is open by TOPS_2:def 1;
then meet rng f is open by TOPS_2:27;
hence thesis by A27,A11,XBOOLE_0:def 10;
end;
suppose A44:n =0;
Affn is non empty by A1;
then A45:Int Affn is non empty by RLAFFIN2:20;
the carrier of TRn = {0.TRn} by A44,EUCLID:25,JORDAN2C:113;
then Int Affn = [#]TRn by A45,ZFMISC_1:39;
hence thesis;
end;
end;