:: Continuity of Barycentric Coordinates in Euclidean Topological Spaces :: by Karol P\kak :: :: Received December 21, 2010 :: Copyright (c) 2010-2012 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, 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, TOPMETR, TOPREAL9, TOPS_2, VECTSP_7, VFUNCT_1, WELLORD2; 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, RELSET_1, RLAFFIN1, RLTOPSP1, RLVECT_5, RVSUM_1, STRUCT_0, SUBSET_1, TOPMETR, TOPREAL1, 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, JORDAN6, LAPLACE, MATRIX_6, MATRIX13, MATRLIN, MATRLIN2, MATRTOP1, MATRTOP2, METRIC_1, METRIZTS, NAT_1, ORDINAL1, PARTFUN1, PCOMPS_1, PRALG_3, PRE_TOPC, 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, 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, NAT_D, TOPREAL3; 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 7; hence thesis by TOPREAL3:46; 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:22; A3: dom I1=dom f1 by EUCLID_9:def 3; then A4: len I1=len f1 by FINSEQ_3:29; A5: dom I2=dom f2 by EUCLID_9:def 3; then len I2=len f2 by FINSEQ_3:29; then A6: dom(I1^I2)=dom I12 by A1,A4,A2,FINSEQ_3:29; 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:25; 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:13; 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:22; dom f1=Seg(len f1) by FINSEQ_1:def 3; then A2: f12|Seg(len f1)=f1 by FINSEQ_1:21; 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:80; 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:29; then A9: len f1=len p1 by A1,FINSEQ_1:59,NAT_1:11; len g=len p1+len p2 by A7,FINSEQ_1:22; then A10: dom f2=dom p2 by A1,A8,A9,FINSEQ_3:29; 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:28; 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:29; A18: now let y be set; assume A19: y in dom f12; then reconsider i=y as Nat; per cases by A19,FINSEQ_1:25; 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:22,FINSEQ_3:29; then dom(p1^p2)=dom f12 by A1,A17,FINSEQ_3:29; 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:57; 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:18; A=(A\{0.V})\/{0.V} by A1,ZFMISC_1:116; hence Lin A=(Lin(A\{0.V}))+(0).V by A2,RLVECT_3:22 .=Lin(A\{0.V}) by RLSUB_2:9; 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:20; A is linearly-independent by A1,RLVECT_3:def 3; then a is linearly-independent by RLVECT_5:14; 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 for 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:24; 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 12; 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:12; reconsider v=V as Subset of TE by A1; V in the topology of T by A3,PRE_TOPC:def 2; then v is open by A1,PRE_TOPC:def 2; then consider r be real number such that A5: r>0 and A6: Ball(X12,r)c=v by A4,TOPMETR:15; set r2=r/2; reconsider B1=Ball(X1,r2),B2=Ball(X2,r2) as Subset of T by A1,TOPMETR:12; take B1,B2; thus B1 is open & B2 is open & x1 in B1 & x2 in B2 by A5,GOBOARD6:1,3,XREAL_1:215; 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 9; 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:12; reconsider y1=x1,y2=x2,c1=b1,c2=b2 as Element of REAL n by EUCLID:22; dist(X2,e2)0 and A17: Ball(AX,r)c=v by A15,TOPMETR:15; set r2=r/2; A18: r2>0 by A16,XREAL_1:215; then A19: r2/2>0 by XREAL_1:215; ex m be positive Real st abs(a)*m0; then reconsider m=r2/2/abs(a) as positive Real by A19,XREAL_1:139; take m; r2/20) by RVSUM_1:32 .=C-(Y-Y) by RVSUM_1:37 .=C-Y+Y by RVSUM_1:41; then A25: |.c.|<=|.c-y.|+|.y.| by EUCLID:12; A26: dist(X,e)=0 & |.y-c.|=dist(X,e) by A2,COMPLEX1:46,SPPOL_1:5; then |.a*y+-a*c.|<=abs(a)*m by A26,A28,XREAL_1:64; then A29: |.a*y+-a*c.|0)-s*C by RVSUM_1:32 .=a*y-(a*C-a*C)-s*c by RVSUM_1:37 .=a*y-a*C+a*C-s*c by RVSUM_1:41 .=a*y-a*C+a*C+-s*c by RVSUM_1:31 .=a*y-a*C+(a*c+-s*c) by RVSUM_1:15 .=a*y+-a*c+(a*c+-s*c) by RVSUM_1:31; then dist(AX,se)=|.a*y+-a*c+(a*c+-s*c).| by A2,SPPOL_1:5; 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:46; hence thesis by RLVECT_5:30; 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:40,42; 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:29; then card(vA\{0.V})<=dim V by RLVECT_5:28; then A4: card(vA\{0.V}\/{0.V})<=1+dim V by A2,XREAL_1:7; 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:43,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 8; A7: card vA=card A & card{0.V}=1 by CARD_2:42,RLAFFIN1:7; -v+v=0.V by RLVECT_1:5; then vA=vA\{0.V}\/{0.V} by A6,ZFMISC_1:116; then A8: card A=card(vA\{0.V})+1 by A7,CARD_2:40,XBOOLE_1:79; dim Lin(vA\{0.V})=card(vA\{0.V}) by A5,RLVECT_5:29; then (Omega).V=(Omega).Lin(vA\{0.V}) by A3,A8,RLVECT_5:31 .=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:48 .=v+Up Lin vA by RUSUB_4:30 .=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:30; then [#]Lin vA=the carrier of the RLSStruct of V by A1,RLSUB_1:47 .=the carrier of(Omega).V by RLSUB_1:def 4; then Lin vA=(Omega).V by RLSUB_1:30 .=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 8; -v+v=0.V by RLVECT_1:5; then A15: vA=vA\{0.V}\/{0.V} by A14,ZFMISC_1:116; card vA=card A & card{0.V}=1 by CARD_2:42,RLAFFIN1:7; hence card A=card(vA\{0.V})+1 by A15,CARD_2:40,XBOOLE_1:79 .=dim V+1 by A13,RLVECT_5:def 2; 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 2; then A4: an is open by A1,PRE_TOPC:def 2; 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 7; then reconsider nk0=nk|->0 as Point of Euclid nk by TOPREAL3:45; let e be Point of Euclid k; A5: @@(e^(nk|->0))=e^(nk|->0) & len(e^nk0)=n by CARD_1:def 7; then reconsider en=e^nk0 as Point of Euclid n by TOPREAL3:45; reconsider En=e^nk0 as Point of TOP-REAL n by A5,TOPREAL3:46; len e=k by CARD_1:def 7; then dom e=Seg k by FINSEQ_1:def 3; then A6: e =En|k by FINSEQ_1:21; 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:139; 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:139; 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 7; then dom P=Seg k by FINSEQ_1:def 3; hence y in ak by A11,FINSEQ_1:21; end; then ak is open by EUCLID_9:24; then ak in the topology of TOP-REAL k by A2,PRE_TOPC:def 2; hence Ak is open by PRE_TOPC:def 2; end; assume Ak is open; then ak in the topology of TOP-REAL k by PRE_TOPC:def 2; then A12: ak is open by A2,PRE_TOPC:def 2; 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 7; @@vk=vk; then reconsider Vk=vk as Point of Euclid k by A15,TOPREAL3:45; 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:139; 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 7; consider q be FinSequence such that A20: @@v=vk^q by FINSEQ_1:80; reconsider q as FinSequence of REAL by A20,FINSEQ_1:36; len v=len vk+len q by A20,FINSEQ_1:22; then reconsider Q=q as Point of Euclid nk by A15,A19,TOPREAL3:45; 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 7; then Y|k=Y|dom p1 by FINSEQ_1:def 3 .=p1 by A21,FINSEQ_1:21; 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 2; hence thesis by PRE_TOPC:def 2; 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 5 .=the carrier of TOP-REAL n by EUCLID:22; 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 5; 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 2; then A9: PP/\[#]TRA in the topology of TRA by PRE_TOPC:def 4; 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 2; end; assume B is open; then B in the topology of TRA by PRE_TOPC:def 2; 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 4; 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 2; 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 7; A18: @@(e^(n|->0))=e^(n|->0); A19: len e=k by CARD_1:def 7; then len(e^(n|->0))=kn by A17,FINSEQ_1:22; then reconsider e0=e^(n|->0) as Point of Euclid kn by A18,TOPREAL3:45; dom e=Seg k by A19,FINSEQ_1:def 3; then A20: e =e0|k by FINSEQ_1:21; n|->0=@@(n|->0); then reconsider N=n|->0 as Element of Euclid n by A17,TOPREAL3:45; 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:139; let x be set; N in OpenHypercube(N,r) by EUCLID_9:11,XREAL_1:139; 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 7; then (w^N)|k=(w^N)|dom w by FINSEQ_1:def 3 .=w by FINSEQ_1:21; 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 2; hence thesis by PRE_TOPC:def 2; 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 6; rf.x=rf/.x by A2,PARTFUN1:def 6; then A5: y=r*(f/.x) by A2,A4,VFUNCT_1:def 4; f.x=f/.x by A1,A2,PARTFUN1:def 6; then f/.x in f.:X by A1,A2,A3,FUNCT_1:def 6; 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 6; v=f/.x by A8,A10,PARTFUN1:def 6; then y=rf/.x by A1,A6,A8,VFUNCT_1:def 4 .=rf.x by A1,A8,PARTFUN1:def 6; hence thesis by A1,A8,A9,FUNCT_1:def 6; 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:66,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:12 .=Up Lin A by RLAFFIN1:6 .=[#]Lin A by RUSUB_4:def 5; 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 8; 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:42; 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:43,RLAFFIN1:12; then card a<1+1 by A1,A2,NAT_1:13; hence A is trivial by NAT_D:60; 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:87; 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 1-element; then consider x being set such that A12: A={x} by ZFMISC_1:131; r*A={0.V} by A11,CONVEX1:34; hence thesis by A1,A12,CARD_2:42; 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:58; 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:62; then reconsider e=E,cAv=card A|->v as Element of card A-tuples_on the carrier of V by FINSEQ_2:92; A3: len(e+cAv)=card A by CARD_1:def 7; 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 3; reconsider x as Element of NAT by A7; A9: e.x in rng e by A5,A4,A7,FUNCT_1:def 3; then reconsider Ex=e.x as Element of V; cAv.x=v by A4,A7,FINSEQ_2:57; then y=Ex+v by A7,A8,FVSUM_1:17; then y=v+Ex by RLVECT_1:def 2; then y in {v+w where w is Element of V:w in A} by A1,A9; hence thesis by RUSUB_4:def 8; 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 8; 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 3; reconsider x as Element of NAT by A12; cAv.x=v by A5,A12,FINSEQ_2:57; then (e+cAv).x=a+v by A5,A4,A12,A13,FVSUM_1:17 .=vA by A10,RLVECT_1:def 2; hence thesis by A5,A4,A12,FUNCT_1:def 3; 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:62; 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:29; A3: rng EV=Av by Def1; then A4: card Av=len EV by FINSEQ_4:62; A5: rng rE=rE.:dom EV by A1,RELAT_1:113 .=r*(EV.:dom EV) by Th10 .=r*Av by A3,RELAT_1:113; A6: card{0.V}=1 by CARD_2:42; 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:62; assume r=0; then card Av<=1 by A6,A7,NAT_1:43,RLAFFIN1:12; then card Av<1+1 by NAT_1:13; hence Av is trivial by NAT_D:60; 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:62; 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 A1: the_rank_of M=n; set MT=Mx2Tran M; A2: MT is one-to-one by A1,MATRTOP1:39; set TRn=TOP-REAL n; let A be finite Subset of TOP-REAL n; let E be Enumeration of A; A3: rng E=A by Def1; dom MT=[#]TRn by FUNCT_2:def 1; then len(MT*E)=len E by A3,FINSEQ_2:29; then A4: dom(MT*E)=dom E by FINSEQ_3:29; rng(MT*E)=(MT*E).:dom(MT*E) by RELAT_1:113 .=MT.:(E.:dom E) by A4,RELAT_1:126 .=MT.:A by A3,RELAT_1:113; hence thesis by A2,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:62; hence thesis by FINSEQ_2:33; 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 8; rng E=Affv by Def1; then A5: len E=card Affv by FINSEQ_4:62; then reconsider e=E,cAv=card Affv|->v as Element of card Affv-tuples_on the carrier of V by FINSEQ_2:92; A6: Affin(v+Affv)=v+Affin Affv & 1*v=v by RLAFFIN1:53,RLVECT_1:def 8; Carrier(v+wA)=v+Carrier wA & Carrier wA c=Affv by RLAFFIN1:16,RLVECT_2:def 6; 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 6; 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:29; rng Ev=v+Affv by Def1; then A11: len Ev=card Affv by A9,FINSEQ_4:62; 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:12; dom E=dom(w|--E) by A8,A5,FINSEQ_3:29; then A15: E.i=E/.i by A13,PARTFUN1:def 6; i in Seg card Affv by A8,A13,FINSEQ_1:def 3; then A16: cAv.i=v by FINSEQ_2:57; A17: ((v+w)|--Ev).i=((v+w)|--(v+Affv)).(Ev.i) by A10,A13,FUNCT_1:12; dom Ev=dom(w|--E) by A8,A11,FINSEQ_3:29; then Ev.i=E/.i+v by A2,A13,A16,A15,FVSUM_1:17; 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:28 .=(w|--Affv).(E/.i+0.V) by RLVECT_1:15 .=(w|--E).i by A14,A15,RLVECT_1:def 4; end; hence thesis by A10,FINSEQ_1:13; 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 6; 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 6; 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:62; then A11: dom(v|--E)=dom E by A10,FINSEQ_3:29; card Affv=card(r*Affv) by A3,Th12; then A12: dom(v|--E)=dom((r*v)|--rE) by A10,A9,FINSEQ_3:29; 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:12,PARTFUN1:def 6; 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:12 ,PARTFUN1:def 6; 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 7 .=vA.(1*(E/.k)) by A3,XCMPLX_0:def 7 .=(v|--E).k by A15,RLVECT_1:def 8; end; hence thesis by A12,FINSEQ_1:13; 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 A1: the_rank_of M=n; set MT=Mx2Tran M; A2: MT is one-to-one by A1,MATRTOP1:39; set E=EN; set A=Affn; let ME be Enumeration of(Mx2Tran M).:A such that A3: ME=(Mx2Tran M)*E; dom MT=the carrier of TRn by FUNCT_2:def 1; then A,MT.:A are_equipotent by A2,CARD_1:33; then A4: card A=card(MT.:A) by CARD_1:5; let v be Element of TOP-REAL n such that A5: v in Affin A; set MTv=MT.v; A6: len(v|--E)=card A by Th16; A7: len(MTv|--ME)=card(MT.:A) by Th16; now let i be Nat; assume A8: 1<=i & i<=card A; then A9: i in dom(MTv|--ME) by A4,A7,FINSEQ_3:25; then A10: i in dom ME by FUNCT_1:11; A11: i in dom(v|--E) by A6,A8,FINSEQ_3:25; then i in dom E by FUNCT_1:11; then E.i in rng E by FUNCT_1:def 3; then reconsider Ei=E.i as Element of TRn; thus(v|--E).i=(v|--A).Ei by A11,FUNCT_1:12 .=(MTv|--MT.:A).(MT.Ei) by A1,A5,MATRTOP2:25 .=(MTv|--MT.:A).(ME.i) by A3,A10,FUNCT_1:12 .=(MTv|--ME).i by A9,FUNCT_1:12; end; hence thesis by A4,A7,A6,FINSEQ_1:14; 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:62; then A5: dom xE=dom E by A3,FINSEQ_3:29; A6: Carrier xB c=B by RLVECT_2:def 6; 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:11; then E.y in Affv by A4,FUNCT_1:def 3; 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:12; hence xE.y=0 by A7,RLVECT_2:19; 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 3; 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:12; 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:111; 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:62; per cases; suppose A6: k>cA; then Seg cA c=Seg k by FINSEQ_1:5; 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:112; cA-k<0 by A6,XREAL_1:49; then cAk=0 by XREAL_0:def 2; then A8: cAk0 is empty; xEk=xE by A3,A6,FINSEQ_1:58; hence thesis by A2,A4,A8,A7,FINSEQ_1:34,RELAT_1:113; end; suppose A9: k<=cA; A10: len cAk0=cAk by CARD_1:def 7; A11: len xEk=k by A3,A9,FINSEQ_1:59; cAk=cA-k by A9,XREAL_1:233; then A12: len(xEk^cAk0)=k+(cA-k) by A11,A10,FINSEQ_1:22; 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:25; A16: i in dom E by A3,A5,A14,FINSEQ_3:25; A17: i in dom(xEk^cAk0) by A3,A12,A14,FINSEQ_3:25; per cases by A11,A17,FINSEQ_1:25; suppose A18: i in dom xEk; hence (xEk^cAk0).i=xEk.i by FINSEQ_1:def 7 .=xE.i by A18,FUNCT_1:47; 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 6; i in Seg k by A16,A22,FUNCT_1:def 4; then A23: i<=k by FINSEQ_1:1; i>=k by A20,NAT_1:11; then i=k by A23,XXREAL_0:1; hence contradiction by A19,A20,FINSEQ_3:25; 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:14; end; assume A24: xE=xEk^cAk0; A25: dom(xEk^cAk0)=dom xE by A3,A12,FINSEQ_3:29; 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:29; then not i in Seg k by A27,FUNCT_1:def 6; 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:25; 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:8; assume A3: k<=card Affv; then A4: Seg k c=Seg cA by FINSEQ_1:5; 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:62; then A8: dom E=dom xE by A5,FINSEQ_3:29; assume A9: x in Affin Affv; A10: len k0=k & len xEk=k by A3,A5,CARD_1:def 7,FINSEQ_1:59; 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:1; then E.i in B by A8,A4,A6,FUNCT_1:def 6; 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:49; end; hence xE=k0^(xE/^k) by A10,A2,FINSEQ_1:14; end; assume xE=k0^(xE/^k); then A13: xEk=k0 by A2,FINSEQ_1:33; 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 3; 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 6; z=y by A8,A14,A16,A18,FUNCT_1:def 4; then xEk.y=xE.y by A17,FUNCT_1:49; 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:233; then A5: len E=cA+1 by A4,FINSEQ_4:62; A6: len E=card A by A4,FINSEQ_4:62; A7: not 0*n in rng(E|cA) proof A8: len E in dom E by A6,A3,FINSEQ_3:25; 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 3; A11: x in Seg cA by A9,RELAT_1:57; x in dom E & (E|cA).x=E.x by A9,FUNCT_1:47,RELAT_1:57; then x=cA+1 by A2,A5,A10,A8,FUNCT_1:def 4; then cA+1<=cA by A11,FINSEQ_1:1; hence thesis by NAT_1:13; end; E=(E|cA)^<*E.len E*> by A5,FINSEQ_3:55; then A12:A=rng(E|cA)\/rng<*E.len E*> by A4,FINSEQ_1:31 .=rng(E|cA)\/{0*n} by A2,FINSEQ_1:38; hence A13:A\{0*n} =rng(E|cA) by A7,ZFMISC_1:117; 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:8; 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:66; 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:12; [#]Lin A1=[#]Lin A by A14,MATRTOP2:6 .=[#]Lin(A\{0.TOP-REAL n}) by Lm2 .=[#]Lin(A\{0*n}) by EUCLID:66 .=[#]Lin(A1\{0*n}) by A14,MATRTOP2:6; then Lin A1=Lin(A1\{0*n}) by VECTSP_4:29 .=Lin rng(e|cA) by A12,A7,A14,VECTSP_9:17,ZFMISC_1:117; then (e|cA is one-to-one) & rng(e|cA) is Basis of Lin A1 by A15,FUNCT_1:52 ,VECTSP_7:def 3; hence thesis by MATRLIN:def 2; end; Lm5: 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 Lm5; 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 7; A10: (v|--E)|cA =(v|--A)*(E|cA) by RELAT_1:83; 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:29; 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:11; 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:10; reconsider KR1 as Linear_Combination of A by A16,RLVECT_2:def 6; 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:8; 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 3; 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:19,TARSKI:def 1; hence thesis by A19,A20; end; then reconsider KR0 as Linear_Combination of{0.TR} by RLVECT_2:def 6; A22: Carrier KR0 c={0.TR} by RLVECT_2:def 6; rng B is Basis of Lin A1 by MATRLIN:def 2; then rng B is linearly-independent by VECTSP_7:def 3; then rng B is linearly-independent Subset of V by VECTSP_9:11; then rB is linearly-independent by MATRTOP2:7; then A23: RB is linearly-independent by RLVECT_5:15; A24: len vB=len B by MATRLIN:def 7; A25: Sum KR0=KR0.(0.TR)*0.TR by RLVECT_2:32 .=0.TR by RLVECT_1:10; A26: 0.TR=0*n by EUCLID:66; then {0.TR}c=A by A2,ZFMISC_1:31; then reconsider KR0 as Linear_Combination of A by RLVECT_2:21; reconsider K=KR1+KR0 as Linear_Combination of A by RLVECT_2:38; 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 4 .=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:10; 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:25; A31: k in dom B by A29,FINSEQ_3:25; then A32: Bk=B.k by PARTFUN1:def 6; then Bk in rng B by A31,FUNCT_1:def 3; then Bk<>0.TR by A6,A26,ZFMISC_1:56; then not Bk in Carrier KR0 by A22,TARSKI:def 1; then A33: KR0.Bk=0 by RLVECT_2:19; k in dom vB by A24,A29,FINSEQ_3:25; then A34: vB.k=vB/.k by PARTFUN1:def 6; K.Bk=KR1.Bk+KR0.Bk by RLVECT_2:def 10; then K.Bk =KR2.Bk by A12,A33,FUNCT_1:49 .=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:12; end; hence thesis by A24,A11,FINSEQ_1:14; end; Lm6: 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 6; 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 8; 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 8; 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:52; then T.u in T.:U by FUNCT_1:def 6; hence thesis by A9,A12,RLTOPSP1:def 10; end; Lm7: 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:66; 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:62; n=1 by NAT_1:14; then len E in dom E by A6,FINSEQ_3:25; then A10: 0*n in A by A8,A5,FUNCT_1:def 3; 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:29; 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 2; then rng BE is linearly-independent by VECTSP_7:def 3; then A13: lines M is linearly-independent by A2,A7,VECTSP_9:11; BE=M by A2,A7; then M is one-to-one by MATRLIN:def 2; 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 3; len(v|--E)=n+1 by A2,Th16; then len((v|--E)|n)=n by FINSEQ_1:59,NAT_1:11; then (v|--E)|n is Element of n-tuples_on REAL by FINSEQ_2:92; 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:22; 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:82; 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 6; 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 6; 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:82; 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; Lm8: 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:25; then A7: 0*n in rng E by A2,FUNCT_1:def 3; A8: 0.TRn=0*n by EUCLID:66; then A9: 0.TRn in A by A2,A3,A6,FUNCT_1:def 3; 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:6; 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 5; consider F be FinSequence such that A14: rng F=A\{0.TRn} and A15: F is one-to-one by FINSEQ_4:58; 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:59; reconsider MBC=Mx2Tran BnC as Function; A16: c1+1=card A; A17: len F=card(A\{0.TRn}) by A14,A15,FINSEQ_4:62 .=c1 by A9,A16,STIRL2_1:55; set MBc=Mx2Tran BnC; set TRc=TOP-REAL c1; A18: dom MBc=[#]TRc & MBc.0.TRc=0.TRn by FUNCT_2:def 1,MATRTOP1:29; rng Bn is Basis of V by MATRLIN:def 2; then rng Bn is linearly-independent by VECTSP_7:def 3; then A19: rng(Bn|c1) is linearly-independent by RELAT_1:70,VECTSP_7:1; 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; A20: rng MBC=BF by A17,MATRTOP2:18; consider M be Matrix of n,F_Real such that A21: M is invertible and A22: M|len F=F by A10,A14,A15,MATRTOP2:19; set MTI=Mx2Tran(M~); A23: [#](TRn|BF)=BF by PRE_TOPC:def 5; M~ is invertible by A21,MATRIX_6:16; then A24: Det(M~)<>0.F_Real by LAPLACE:34; then A25: the_rank_of(M~)=n by MATRIX13:83; then reconsider MTe=MTI*E as Enumeration of MTI.:A by Th15; A26: rng MTe=MTI.:A by Def1; dom MTI=[#]TRn & MTI is one-to-one by A24,FUNCT_2:def 1,MATRTOP1:40; then A,MTI.:A are_equipotent by CARD_1:33; then A27: card A=card(MTI.:A) by CARD_1:5; then len MTe=len E by A4,A26,FINSEQ_4:62; then len E in dom MTe by A5,FINSEQ_3:25; then A28: MTe.len E=MTI.(0.TRn) by A2,A8,FUNCT_1:12 .=0.TRn by MATRTOP1:29; set MT=Mx2Tran M; Affin A=[#]Lin A by A3,A7,Th11 .=[#]Lin rng F by A14,Lm2; then A29: MT.:BF=AA by A10,A14,A15,A21,A22,MATRTOP2:21; then A30: rng(MT|BF)=AA by RELAT_1:115; A31: dom MT=[#]TRn by FUNCT_2:def 1; then dom(MT|BF)=BF by RELAT_1:62; then reconsider MT1=MT|BF as Function of TRn|BF,TRn|AA by A13,A23,A30, FUNCT_2:1; reconsider MT as Function; A32: Det M<>0.F_Real by A21,LAPLACE:34; then A33: MT"=MTI by MATRTOP1:43; MT1 is being_homeomorphism by A21,A29,METRIZTS:2; then A34: 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}; A35: nc=n-c1 by A11,XREAL_1:233; then A36: n=c1+nc; A37: MT is one-to-one by A32,MATRTOP1:40; then A38: MT"AA=BF by A29,A31,FUNCT_1:94; A39: MT"A c=MT"AA by RELAT_1:143,RLAFFIN1:49; then A40: MTI.:A c=BF by A33,A37,A38,FUNCT_1:85; Bn is one-to-one by MATRLIN:def 2; then Bn|c1 is one-to-one by FUNCT_1:52; then A41: the_rank_of BnC=c1 by A19,MATRIX13:121; then A42: MBC is one-to-one by MATRTOP1:39; then A43: dom(MBC")=rng MBC by FUNCT_1:33; then reconsider MBCe=MBC"*MTe as FinSequence by A20,A26,A40,FINSEQ_1:16; A44: rng MBCe=MBC".:(MTI.:A) by A26,RELAT_1:127; MTI.:A is affinely-independent by A25,MATRTOP2:24; then MBc"(MTI.:A) is affinely-independent by A41,MATRTOP2:27; then reconsider R=rng MBCe as finite affinely-independent Subset of TRc by A42,A44,FUNCT_1:85; reconsider MBCe as Enumeration of R by A42,Def1; reconsider MBCeE=MBc*MBCe as Enumeration of(Mx2Tran BnC).:R by A41,Th15; MBC*MBC"=id rng MBC by A42,FUNCT_1:39; then A45: MBCeE=(id rng MBC)*MTe by RELAT_1:36 .=MTe by A20,A26,A40,RELAT_1:53; set PPP={v where v is Element of TRc:(v|--MBCe)|k in P}; A46: 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; A47: MTI.:A=MT"A by A33,A37,FUNCT_1:85; A48: MT"B c=MT"AA by A13,RELAT_1:143; A49: (MTI.:A),R are_equipotent by A20,A42,A43,A40,A44,CARD_1:33; then A50: c1+1=card R by A27,CARD_1:5; then A51: k<=c1 & R is non empty by A1,NAT_1:13; reconsider PPP as Subset of TRc by A46; set nPP={v where v is Element of TRn:v|c1 in PPP & v in BF}; dim TRc=c1 by Th4; then A52: Affin R=[#]TRc by A50,Th6; A53: (Mx2Tran BnC).:R=MBC.:(MBC".:(MTI.:A)) by A26,RELAT_1:127 .=(MBC*MBC").:(MTI.:A) by RELAT_1:126 .=(id rng MBC).:(MTI.:A) by A42,FUNCT_1:39 .=MTI.:A by A47,A38,A39,A20,FUNCT_1:92; A54: MT"B c=nPP proof let x be set; assume A55: x in MT"B; then reconsider w=x as Element of TRn|BF by A29,A23,A31,A37,A48,FUNCT_1:94; MT.x in B by A55,FUNCT_1:def 7; then consider v be Element of TRn|AA such that A56: MT.x=v and A57: (v|--E)|k in P by A12; x in dom MT by A55,FUNCT_1:def 7; then A58: MTI.v=x by A33,A37,A56,FUNCT_1:34; x in BF by A38,A48,A55; then reconsider W=x as Element of TRn; A59: v in AA by A13; consider u be set such that A60: u in dom MBc and A61: MBc.u=w by A38,A48,A20,A55,FUNCT_1:def 3; A62: W|c1=u by A60,A61,MATRTOP1:38; reconsider u as Element of TRc by A60; u|--MBCe =w|--MTe by A61,A53,A45,A41,A52,Th19 .=v|--E by A25,A58,A59,Th19; then u in PPP by A57; hence thesis by A38,A48,A55,A62; end; A63: BF c=Vc1 proof let x be set; assume A64: x in BF; then reconsider f=x as Element of TRn; len f=n by CARD_1:def 7; then len(f|c1)=c1 by A11,FINSEQ_1:59; then f|c1 is c1-element by CARD_1:def 7; then A65: f|c1 is Element of TRc by Lm1; f in Lin rng(Bn|c1) by A17,A64,STRUCT_0:def 5; then f=(f|c1)^nc0 by MATRTOP2:20; hence thesis by A65; end; Vc1 c=BF proof let x be set; assume x in Vc1; then consider v be Element of TRc such that A66: x=v^nc0 and not contradiction; len v=c1 by CARD_1:def 7; then (v^(nc|->0))|c1=(v^(nc|->0))|dom v by FINSEQ_1:def 3 .=v by FINSEQ_1:21; then v^(nc|->0) in Lin rng(Bn|c1) by A35,MATRTOP2:20; hence thesis by A17,A66,STRUCT_0:def 5; end; then A67: BF=Vc1 by A63,XBOOLE_0:def 10; A68: nPP c=MT"B proof let x be set; assume x in nPP; then consider v be Element of TRn such that A69: x=v and A70: v|c1 in PPP and A71: v in BF; consider v1 be Element of TRc such that A72: v=v1^nc0 by A67,A71; consider u be Element of TRc such that A73: u=v|c1 and A74: (u|--MBCe)|k in P by A70; set w=MBc.u; A75: w=MTI.(MT.w) by A31,A33,A37,FUNCT_1:34; dom MBc=[#]TRc by FUNCT_2:def 1; then A76: w in BF by A20,FUNCT_1:def 3; then A77: MT.w in AA by A29,A31,FUNCT_1:def 6; u|--MBCe=w|--MBCeE by A41,A52,Th19 .=MT.w|--E by A25,A75,A77,Th19,A53,A45; then A78: MT.w in B by A12,A13,A74,A77; consider w1 be Element of TRc such that A79: w=w1^nc0 by A67,A76; w1=w|dom w1 by A79,FINSEQ_1:21 .=w|Seg len w1 by FINSEQ_1:def 3 .=w|c1 by CARD_1:def 7 .=v|c1 by A73,MATRTOP1:38 .=v|Seg len v1 by CARD_1:def 7 .=v|dom v1 by FINSEQ_1:def 3 .=v1 by A72,FINSEQ_1:21; hence thesis by A31,A69,A79,A72,A78,FUNCT_1:def 7; end; A80: len MBCe=len E by A4,A50,FINSEQ_4:62; then len E in dom MBCe by A5,FINSEQ_3:25; then MBCe.len E=(MBC").(0.TRn) by A28,FUNCT_1:12 .=0.TRc by A42,A18,FUNCT_1:34; then A81: MBCe.len MBCe=0*c1 by A80,EUCLID:70; MT1"B=BF/\(MT"B) by FUNCT_1:70 .=MT"B by A13,A38,RELAT_1:143,XBOOLE_1:28; then MT1"B=nPP by A54,A68,XBOOLE_0:def 10; then A82: PPP is open iff B is open by A34,A67,A36,Th8; card R=c1+1 by A27,A49,CARD_1:5; hence thesis by A81,A82,A51,Lm7; 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:62; then A6: len E>=1 by A2,NAT_1:14; then A7: len E in dom E by FINSEQ_3:25; then E.(len E) in A by A4,FUNCT_1:def 3; 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 Lm6; 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:57; A20: rng Ev=-EL+A by Def1; then len Ev=card A by A15,FINSEQ_4:62; then dom E=dom Ev by A5,FINSEQ_3:29; then Ev.len E=EL+(-EL) by A7,A19,FVSUM_1:17 .=0.TRn by RLVECT_1:5 .=0*n by EUCLID:70; then A21: Ev.len Ev=0*n by A5,A15,A20,FINSEQ_4:62; -EL+A is non empty by A2,A15; then T.:An is open iff Ak is open by A1,A21,A8,A18,Lm7; hence thesis by TOPGRP_1:25; set TAA=T.:AA; A22: rng(T|AA)=T.:AA by RELAT_1:115; dom T=[#]TRn by FUNCT_2:52; then A23: dom(T|AA)=AA by RELAT_1:62; [#](TRn|AA)=AA & [#](TRn|TAA)=TAA by PRE_TOPC:def 5; then reconsider TA=T|AA as Function of TRn|AA,TRn|TAA by A23,A22,FUNCT_2:1; 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 for 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:31; 0*cIB=cIB|->0 by EUCLID:def 4; then A13: P is closed by A12,PCOMPS_1:7; 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:91; Ia\/IB=Ia\/IA by XBOOLE_1:39 .=IA by A4,XBOOLE_1:12; then rng P12=IA by A14,A15,FINSEQ_1:31; then reconsider P12 as Enumeration of IA by A16,Def1; len P2=card IB by A15,FINSEQ_4:62; then A17: P12.:(Seg cIB)=P12.:dom P2 by FINSEQ_1:def 3 .=rng(P12|dom P2) by RELAT_1:115 .=rng P2 by FINSEQ_1:21 .=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:8; vP=(cIB|->0)^(vP/^cIB) by A1,A3,A5,A8,A18,A17,A11,A20,Th22; then vP|cIB=cIB|->0 by A21,FINSEQ_1:33; 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:8; 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:25; then E.(len E) in A by A9,FUNCT_1:def 3; 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:57; 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:62; then dom E=dom Ev by A10,FINSEQ_3:29; then Ev.len E=EL+(-EL) by A12,A13,FVSUM_1:17 .=0.Tn by RLVECT_1:5 .=0*n by EUCLID:70; then A22: Ev.len Ev=0*n by A10,A19,A21,FINSEQ_4:62; 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:33; TA.:B=T.:B by A3,RELAT_1:129; then A25: TAB={w where w is Element of Tn:w in Affin(-EL+A) & (w|--Ev)|k in Ak} by A8,Lm6; 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:33; hence thesis by A15,A27,A29; end; A30: T.:AA is non empty by A6,A17,RELAT_1:119; 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,Lm8; 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 12; per cases; suppose A2: p=q; {p} is closed by URYSOHN1:19; hence thesis by A1,A2,TOPREAL9:29; end; suppose A3: p<>q; A4: rng<*p,q*>=pq by FINSEQ_2:127; <*p,q*> is one-to-one by A3,FINSEQ_3:94; 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:44; reconsider L as Subset of R^1 by TOPMETR:17; 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 5; A8: card pq=2 by A3,CARD_2:57; A9: h is being_homeomorphism by A6,JORDAN2B:28; 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 6; then not p in Carrier(q|--{q}) by A3,TARSKI:def 1; then A12: (q|--{q}).p=0 by RLVECT_2:19; {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:36; then 0=(q|--pq).p by A12,A13,RLAFFIN1:77; then A17: (a*(q|--pq)).p=a*0 by RLVECT_2:def 11 .=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 10 .=(1-a)*((p|--pq).p)+0 by A17,RLVECT_2:def 11 .=1-a by A18; then W.p<=1-0 by A16,XREAL_1:10; 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:59; then reconsider wE1=wE|1 as Point of TOP-REAL 1 by TOPREAL3:46; A22: 1 in dom wE1 by A21,FINSEQ_3:25; then A23: wE1/.1=wE1.1 & wE1.1=wE.1 by FUNCT_1:47,PARTFUN1:def 6; A24: 1 in dom wE by A22,RELAT_1:57; h.wE1=wE1/.1 by A6; then h.wE1 in L by A5,A20,A23,A24,FUNCT_1:12; then wE1 in h"L by A10,FUNCT_1:def 7; then w in B; hence thesis; end; L is closed by BORSUK_5:41; 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 7; then A29: 1 in dom wE1 by FINSEQ_3:25; then A30: wE1/.1=wE1.1 & wE1.1=wE.1 by FUNCT_1:47,PARTFUN1:def 6; A31: 1 in dom wE by A29,RELAT_1:57; h.(wE|1) in L by A27,FUNCT_1:def 7; then W.p in L by A5,A28,A30,A31,FUNCT_1:12; then W.p<=1 by XXREAL_1:234; then A32: W.p-W.p<=1-W.p by XREAL_1:9; A33: sum W=1 by A7,RLAFFIN1:def 7; Carrier W c=pq by RLVECT_2:def 6; 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:33; 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 3; hence thesis by TOPMETR:17; end; suppose not x in dom vA; then vA.x=0 by FUNCT_1:def 2; hence thesis by Lm5,TOPMETR:17; 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:12; 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 6; 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:19; end; suppose not x in [#]V; then not x in dom(y|--A); hence Ax.y=0 by A3,FUNCT_1:def 2; end; end; dom Ax=[#]V by FUNCT_2:def 1; hence thesis by A2,FUNCOP_1:11; 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:7 .=(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 Lm5,TOPMETR:17; 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 5; then reconsider AxA as Function of TRn|AA,R^1 by FUNCT_2:32; 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:12; 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:42; 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 3; then reconsider b=AxA.x as Element of R^1 by A5; rng AxA={AxA.x} by A3,A6,A7,A8,FUNCT_1:4; then AxA =(TRn|AA)-->b by A2,A3,FUNCOP_1:9; 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:39; (P1 is one-to-one) & {x}misses Affn\{x} by FINSEQ_3:93,XBOOLE_1:79; then A11: P12 is one-to-one by A10,FINSEQ_3:91; rng P12=rng P1\/rng P2 by FINSEQ_1:31; then rng P12=Affn by A9,A10,ZFMISC_1:116; 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:28; 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:26; 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:2; assume P is closed; then A17: Pro"P is closed by A13,TOPGRP_1:24; A18: dom P1=Seg 1 by FINSEQ_1:38; then A19: P12.1=P1.1 by A16,FINSEQ_1:2,def 7 .=x by FINSEQ_1:40; 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 7; 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:57; Pro.vP1=vP1/.1 by A12 .=vP1.1 by A25,PARTFUN1:def 6 .=vP.1 by A25,FUNCT_1:47 .=(v|--Affn).x by A19,A26,FUNCT_1:12 .=Ax.v by A24,Def3; then Ax.v in P by A23,FUNCT_1:def 7; then AxA.v in P by A2,A3,A9,FUNCT_1:47; hence thesis by A2,A3,A9,A22,FUNCT_1:def 7; 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:59,NAT_1:14; then reconsider yP1=yP|1 as Element of TR1 by TOPREAL3:46; 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 7; then AxA.y=Ax.y by FUNCT_1:47 .=(y|--Affn).(P12.1) by A19,A3,A31,Def3 .=yP.1 by A18,A16,A15,FINSEQ_1:2,FUNCT_1:13 .=yP1.1 by A16,A29,FINSEQ_1:2,FUNCT_1:47 .=yP1/.1 by A16,A29,FINSEQ_1:2,PARTFUN1:def 6 .=Pro.yP1 by A12; then Pro.yP1 in P by A30,FUNCT_1:def 7; then yP1 in Pro"P by A27,FUNCT_1:def 7; 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 6; 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:93; 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 6; then A5: (AxA"P)` in the topology of the TopStruct of TRn by A3, PRE_TOPC:def 2; (AxA"P)`=(Ax"P)` by A4,A3,RELAT_1:69; then (Ax"P)` is open by A5,PRE_TOPC:def 2; hence Ax"P is closed by TOPS_1:3; end; hence thesis by PRE_TOPC:def 6; end; Lm9: 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:17; 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:42; 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 3; 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:62; 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 3; 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 3; then A16: meet rng f c=f.k by SETFAM_1:3; 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 7; 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 3; E.k in A by A1,A2,A8,A9,A4,A18,A21,FUNCT_1:def 3; 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 7; 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 3; (|--(A,E.k) is continuous) & L is closed by A1,Th32,TREAL_1:1; then |--(A,E.k)"L is closed by PRE_TOPC:def 6; 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:22; 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 Lm9; 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:17; 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:42; 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 3; 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:62; 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 3; 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 3; then A18: meet rng f c=f.k by SETFAM_1:3; 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 7; 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:19; end; Carrier(x|--A)c=A by RLVECT_2:def 6; 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 3; A36: E.k in A by A1,A3,A9,A10,A5,A26,A34,FUNCT_1:def 3; then reconsider Ek=E.k as Element of TRn; (x|--A).Ek<>0 by A32,A33,A36,RLVECT_2:19; 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:42; 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 7; 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 3; (|--(A,E.k) is continuous) & L is open by A1,Th32,JORDAN6:35; then |--(A,E.k)"L is open by A42,TOPS_2:43; 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:20; 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:22,77; then Int Affn = [#]TRn by A45,ZFMISC_1:33; hence thesis; end; end;