:: Continuity of Barycentric Coordinates in Euclidean Topological Spaces
:: by Karol P\kak
::
:: Received December 21, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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, 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, XXREAL_0, XXREAL_1,
ZFMISC_1, GROUP_1;
notations VECTSP_2, GCD_1, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1,
ORDINAL1, NUMBERS, XCMPLX_0, 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, 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_0, 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 VECTSP_2, GCD_1, 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, TOPMETR, TOPREAL9, TOPS_2, VECTSP_7,
VFUNCT_1, WELLORD2, MATRIX_1, FINSEQOP, MATRIX_3;
registrations CARD_1, EUCLID, EUCLID_7, EUCLID_9, FINSEQ_1, FINSEQ_2,
FINSET_1, FUNCT_1, JORDAN2B, MATRIX13, MATRTOP1, MONOID_0, NAT_1,
NUMBERS, PRE_TOPC, PRVECT_1, RELSET_1, RLAFFIN1, RLTOPSP1,
RLVECT_5, RVSUM_1, STRUCT_0, SUBSET_1, TOPMETR, TOPREAL1, TOPS_1,
VALUED_0, VECTSP_1, VECTSP_2, VECTSP_9, XBOOLE_0, XREAL_0,
XXREAL_0, ORDINAL1, LAPLACE;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions RLTOPSP1, TARSKI, XBOOLE_0;
equalities FINSEQ_1, MATRIX13, MATRTOP1, STRUCT_0, SUBSET_1;
expansions FINSEQ_1, STRUCT_0, TARSKI, XBOOLE_0;
theorems BORSUK_5, CARD_1, CARD_2, CARD_3, 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, 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,
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, STRUCT_0;
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
holds Intervals(f1,r)^Intervals(f2,r) = Intervals(f1^f2,r)
proof
let f1,f2 be real-valued FinSequence;
let r be Real;
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 object 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 object;
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 object 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 object 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 object;
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;
thus T is add-continuous
proof
let x1,x2 be Point of T,V be Subset of T such that
A2: V is open and
A3: 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 A2,PRE_TOPC:def 2;
then v is open by A1,PRE_TOPC:def 2;
then consider r be Real such that
A4: r>0 and
A5: Ball(X12,r)c=v by A3,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 A4,GOBOARD6:1,3,XREAL_1:215;
let x be object;
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
A6: x=b1+b2 and
A7: b1 in B1 and
A8: 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)<r2 by A8,METRIC_1:11;
then A9: |.y2-c2.|<r2 by SPPOL_1:5;
dist(X1,e1)<r2 by A7,METRIC_1:11;
then |.y1-c1.|<r2 by SPPOL_1:5;
then A10: |.(y1-c1).|+|.(y2-c2).|<r2+r2 by A9,XREAL_1:8;
A11: (y1+y2)-(c1+c2)=y1+y2+-(c2+c1) by RVSUM_1:31
.=y1+y2+(-c2+-c1) by RVSUM_1:26
.=((y1+y2)+-c2)+-c1 by RVSUM_1:15
.=((y2+-c2)+y1)+-c1 by RVSUM_1:15
.=(y2+-c2)+(y1+-c1) by RVSUM_1:15
.=(y2-c2)+(y1+-c1) by RVSUM_1:31
.=(y2-c2)+(y1-c1) by RVSUM_1:31;
A12: dist(X12,e12)=|.(y1-c1)+(y2-c2).| by A11,SPPOL_1:5;
|.(y1-c1)+(y2-c2).|<=|.(y1-c1).|+|.(y2-c2).| by EUCLID:12;
then dist(X12,e12)<r by A10,A12,XXREAL_0:2;
then e12 in Ball(X12,r) by METRIC_1:11;
hence x in V by A5,A6;
end;
let a be Real,x be Point of T,V be Subset of T such that
A13: V is open and
A14: a*x in V;
reconsider X=x,AX=a*x as Point of E by A1,TOPMETR:12;
reconsider v=V as Subset of TE by A1;
V in the topology of T by A13,PRE_TOPC:def 2;
then v is open by A1,PRE_TOPC:def 2;
then consider r be Real such that
A15: r>0 and
A16: Ball(AX,r)c=v by A14,TOPMETR:15;
set r2=r/2;
A17: r2>0 by A15,XREAL_1:215;
then A18: r2/2>0 by XREAL_1:215;
ex m be positive Real st |.a.|*m<r2
proof
per cases by COMPLEX1:46;
suppose |.a.|=0;
then |.a.|*1<r2 by A15,XREAL_1:215;
hence thesis;
end;
suppose A19: |.a.|>0;
then reconsider m=r2/2/|.a.| as positive Real
by A18,XREAL_1:139;
take m;
r2/2<r2 by A15,XREAL_1:215,216;
hence thesis by A19,XCMPLX_1:87;
end;
end;
then consider m be positive Real such that
A20: |.a.|*m<r2;
reconsider B=Ball(X,m) as Subset of T by A1,TOPMETR:12;
reconsider nr=r2/(|.x.|+m)
as positive Real by A17,XREAL_1:139;
take nr,B;
thus B is open & x in B by GOBOARD6:1,3;
let s being Real;
assume A21: |.s-a.|<nr;
let z be object;
assume z in s*B;
then z in {s*b where b is Element of T:b in B} by CONVEX1:def 1;
then consider b be Element of T such that
A22: z=s*b and
A23: b in B;
reconsider e=b,se=s*b as Point of E by A1,TOPMETR:12;
reconsider y=x,c =b as Element of REAL n by EUCLID:22;
reconsider Y=y,C=c as Element of n-tuples_on REAL by EUCLID:def 1;
c =C-(n|->0) by RVSUM_1:32
.=C-(Y-Y) by RVSUM_1:37
.=C-Y+Y by RVSUM_1:41;
then A24: |.c.|<=|.c-y.|+|.y.| by EUCLID:12;
A25: dist(X,e)<m by A23,METRIC_1:11;
then |.c-y.|<m by SPPOL_1:5;
then |.c-y.|+|.y.|<=m+|.x.| by XREAL_1:6;
then |.c.|<=m+|.x.| by A24,XXREAL_0:2;
then A26: nr*|.c.|<=nr*(m+|.x.|) by XREAL_1:64;
a*y+-a*c =a*y+(-1)*(a*c) by RVSUM_1:54
.=a*y+((-1)*a)*c by RVSUM_1:49
.=a*y+a*((-1)*c) by RVSUM_1:49
.=a*(y+(-1)*c) by RVSUM_1:51
.=a*(y+-c) by RVSUM_1:54
.=a*(y-c) by RVSUM_1:31;
then A27: |.a*y+-a*c.|=|.a.|*|.y-c.| by EUCLID:11;
|.a.|>=0 & |.y-c.|=dist(X,e) by COMPLEX1:46,SPPOL_1:5;
then |.a*y+-a*c.|<=|.a.|*m by A25,A27,XREAL_1:64;
then A28: |.a*y+-a*c.|<r2 by A20,XXREAL_0:2;
a*c+-s*c =a*c+(-1)*(s*c) by RVSUM_1:54
.=a*c+((-1)*s)*c by RVSUM_1:49
.=(a+(-1)*s)*c by RVSUM_1:50;
then |.a*c+-s*c.|=|.a-s.|*|.c.| by EUCLID:11
.=|.-(a-s).|*|.c.| by COMPLEX1:52;
then nr*(|.x.|+m)=r2 & |.a*c+-s*c.|<=nr*|.c.| by A21,XCMPLX_1:87,XREAL_1:64;
then |.a*c+-s*c.|<=r2 by A26,XXREAL_0:2;
then A29: |.a*y+-a*c+(a*c+-s*c).|<=|.a*y+-a*c.|+|.a*c+-s*c.| & |.a*y+-a*c.|+
|.a*c+-s*c.|<r2+r2 by A28,EUCLID:12,XREAL_1:8;
a*y-s*c =a*Y-(n|->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 SPPOL_1:5;
then dist(AX,se)<r by A29,XXREAL_0:2;
then se in Ball(AX,r) by METRIC_1:11;
hence z in V by A16,A22;
end;
cluster TOP-REAL n -> 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;
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 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 object;
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 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 object;
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 = the set of all v^(n|->0) where v is Element of TOP-REAL k
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=the set of all v^(n|->0) where v is Element of TRk;
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 object;
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 object;
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 object;
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;
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 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 object;
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 object;
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 object;
assume y in rf.:X;
then consider x be object 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 object;
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 object 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;
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;
end;
suppose A9: A is empty;
r*A is empty
proof
assume r*A is non empty;
then consider x be object such that
A10: x in r*A;
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 object 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;
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 set;
let A be finite Subset of X;
redefine mode Enumeration of A -> one-to-one FinSequence of X; :: redefines Enumeration (RLAFFIN3, definition)
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 object;
assume y in rng(e+cAv);
then consider x be object 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 object;
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 object 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;
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 be object;
func x|--E -> FinSequence of REAL equals
(x|--Av)*E;
coherence;
end;
theorem Th16:
for x being object holds
for E be Enumeration of Av holds len (x|--E) = card Av
proof let x be object;
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;
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 object 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 object 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;
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;
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 object 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 object 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 object;
assume x in A1;
then x in Lin A1 by VECTSP_7:8;
hence thesis;
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;
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;
reconsider ms = 1-sum KR1 as Element of REAL by XREAL_0:def 1;
consider KR0 being Function of the carrier of TR,REAL such that
A18: KR0.0.TR= ms 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 be object;
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;
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 object;
assume y in T.:U;
then consider x be object 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 object;
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<n+1 by NAT_1:13;
then len(FinS2MX(e|n)) = n by A2,A6,FINSEQ_1:59;
then reconsider M=FinS2MX(e|n) as Matrix of n,F_Real;
A7: card A-1=cA by NAT_1:14,XREAL_1:233;
set MT=Mx2Tran M;
assume A8: E.len E=0*n;
let P be Subset of TRk,B be Subset of TRn;
set PP={v where v is Element of TRn:v|k in P};
PP c=the carrier of TRn
proof
let x be object;
assume x in PP;
then ex v be Element of TRn st x=v & v|k in P;
hence thesis;
end;
then reconsider PP as Subset of TRn;
assume A9: B={v where v is Element of TRn:(v|--E)|k in P};
card A>=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 Det M is non zero;
then Det M is unital;
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 object;
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 object 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 object;
assume y in MT.:PP;
then consider x be object 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;
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<card A for E be Enumeration of A st E.len E=0*n for P be Subset of
TOP-REAL k for B be Subset of(TOP-REAL n)|Affin A st B={v where v is Element of
(TOP-REAL n)|(Affin A):(v|--E)|k in P} holds P is open iff B is open
proof
let n,k be Nat;
set TRn=TOP-REAL n;
let A be non empty finite affinely-independent Subset of TRn such that
A1: k<card A;
reconsider c1=card A-1 as Element of NAT by NAT_1:14,21;
set AA=Affin A;
let E be Enumeration of A such that
A2: E.len E=0*n;
A3: rng E=A by Def1;
then A4: len E=card A by FINSEQ_4:62;
then A5: len E>=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 len FinS2MX(Bn|c1) = c1 by A11,FINSEQ_1:59;
then reconsider BnC=FinS2MX(Bn|c1) as Matrix of c1,n,F_Real;
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 Det(M~) is unital by LAPLACE:34;
then Det(M~) is non zero by LAPLACE:42,43;
then A24: Det(M~)<>0.F_Real;
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;
Det M is unital by A21,LAPLACE:34;
then Det M is non zero by LAPLACE:42,43;
then A32: Det M<>0.F_Real;
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=the set of all v^nc0 where v is Element of TRc;
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 object;
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 object;
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 object 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 object;
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;
then f=(f|c1)^nc0 by MATRTOP2:20;
hence thesis by A65;
end;
Vc1 c=BF
proof
let x be object;
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;
end;
then A67: BF=Vc1 by A63;
A68: nPP c=MT"B
proof
let x be object;
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;
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 object;
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 object;
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;
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 object;
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 object;
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;
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<card A by A1,NAT_1:13;
A4: An`c=B1
proof
let x be object;
assume A5: x in An`;
then reconsider f=x as Element of TRn;
set fE=f|--E;
len fE=card A by Th16;
then len(fE|k)=k by A3,FINSEQ_1:59;
then A6: fE|k is Element of TRk by TOPREAL3:46;
assume not x in B1;
then not fE|k in Ak`;
then fE|k in Ak by A6,XBOOLE_0:def 5;
then f in An by A2;
hence contradiction by A5,XBOOLE_0:def 5;
end;
B1 c=An`
proof
let x be object;
assume x in B1;
then consider v be Element of TRn such that
A7: x=v and
A8: (v|--E)|k in Ak`;
assume not x in An`;
then v in An by A7,XBOOLE_0:def 5;
then ex w be Element of TRn st v=w & (w|--E)|k in Ak by A2;
hence contradiction by A8,XBOOLE_0:def 5;
end;
then An`=B1 by A4;
then Ak` is open iff An` is open by A1,Th25;
hence thesis by TOPS_1:3;
end;
registration
let n;
cluster Affine -> 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;
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_2:102,XBOOLE_1:36;
then A10: cIB<n+1 by A7,XXREAL_0:1;
then A11: cIB<card IA by A5,A8,A6,Th6;
set TRc=TOP-REAL cIB;
A12: 0*cIB=0.TRc by EUCLID:66;
then cIB|->0 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 object;
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 object;
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;
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<card A and
A2: B={v where v is Element of Tn|AA:(v|--E)|k in Ak};
set BB={u where u is Element of Tn:u in AA & (u|--E)|k in Ak};
A3: [#](Tn|AA)=AA by PRE_TOPC:def 5;
A4: BB c=B
proof
let x be object;
assume x in BB;
then consider u be Element of Tn such that
A5: x=u & u in AA & (u|--E)|k in Ak;
thus thesis by A2,A3,A5;
end;
A6: A is non empty by A1;
B c=BB
proof
let x be object;
assume x in B;
then consider u be Element of Tn|AA such that
A7: x=u & (u|--E)|k in Ak by A2;
AA is non empty by A6;
then u in AA by A3;
hence thesis by A7;
end;
then A8: BB=B by A4;
A9: rng E=A by Def1;
then A10: len E=card A by FINSEQ_4:62;
then A11: len E>=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<card(-EL+A) by A1,RLAFFIN1:7;
set T=transl(-EL,Tn);
set TAA=T.:AA;
A15: [#](Tn|TAA)=TAA by PRE_TOPC:def 5;
A16: rng(T|AA)=T.:AA by RELAT_1:115;
A17: dom T=[#]Tn by FUNCT_2:52;
then dom(T|AA)=AA by RELAT_1:62;
then reconsider TA=T|AA as Function of Tn|AA,Tn|TAA by A3,A15,A16,FUNCT_2:1;
reconsider TAB=TA.:B as Subset of Tn|TAA;
A18: TA is being_homeomorphism by METRIZTS:2;
reconsider Ev=E+(card A|->-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 object;
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 object;
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;
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<card A and
A2: B={v where v is Element of TRn|AA:(v|--E)|k in Ak};
set B1={v where v is Element of TRn|AA:(v|--E)|k in Ak`};
A3: B`c=B1
proof
let x be object;
assume A4: x in B`;
then reconsider v=x as Element of TRn|AA;
set vE=v|--E;
len vE=card A by Th16;
then len(vE|k)=k by A1,FINSEQ_1:59;
then A5: vE|k in [#]TOP-REAL k by TOPREAL3:46;
not v in B by A4,XBOOLE_0:def 5;
then not vE|k in Ak by A2;
then vE|k in Ak` by A5,XBOOLE_0:def 5;
hence thesis;
end;
A6: A is non empty by A1;
B1 c=B`
proof
let x be object;
assume x in B1;
then consider v be Element of TRn|AA such that
A7: x=v and
A8: (v|--E)|k in Ak`;
assume not x in B`;
then v in B by A6,A7,XBOOLE_0:def 5;
then ex w be Element of TRn|AA st w=v & (w|--E)|k in Ak by A2;
hence contradiction by A8,XBOOLE_0:def 5;
set vE=v|--E;
end;
then B1=B` by A3;
then Ak` is open iff B` is open by A1,Th27;
hence thesis by TOPS_1:3;
end;
registration
let n;
let p,q be Point of TOP-REAL n;
cluster halfline(p,q) -> closed;
coherence
proof
set pq={p,q};
per cases;
suppose A1: p=q;
{p} is closed by URYSOHN1:19;
hence thesis by A1,TOPREAL9:29;
end;
suppose A2: p<>q;
A3: rng<*p,q*>=pq by FINSEQ_2:127;
<*p,q*> is one-to-one by A2,FINSEQ_3:94;
then reconsider E=<*p,q*> as Enumeration of pq by A3,Def1;
set Apq=Affin pq;
set TRn=TOP-REAL n,TR1=TOP-REAL 1;
set L=].-infty,1 .];
A4: E.1=p;
reconsider L as Subset of R^1 by TOPMETR:17;
consider h be Function of TR1,R^1 such that
A5: 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 object;
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;
A6: [#](TRn|Apq)=Apq by PRE_TOPC:def 5;
A7: card pq=2 by A2,CARD_2:57;
A8: h is being_homeomorphism by A5,JORDAN2B:28;
then A9: dom h=[#]TR1 by TOPGRP_1:24;
A10: halfline(p,q)c=B
proof
Carrier(q|--{q})c={q} by RLVECT_2:def 6;
then not p in Carrier(q|--{q}) by A2,TARSKI:def 1;
then A11: (q|--{q}).p=0 by RLVECT_2:19;
{q} is Affine by RUSUB_4:23;
then A12: Affin{q}={q} by RLAFFIN1:50;
let x be object;
set W=x|--pq,wE=x|--E;
A13: p in pq by TARSKI:def 2;
assume x in halfline(p,q);
then consider a be Real such that
A14: x=(1-a)*p+a*q and
A15: 0<=a by TOPREAL9:26;
reconsider a as Real;
q in {q} & {q}c=pq by TARSKI:def 1,ZFMISC_1:36;
then 0=(q|--pq).p by A11,A12,RLAFFIN1:77;
then A16: (a*(q|--pq)).p=a*0 by RLVECT_2:def 11
.=0;
pq c=conv pq by CONVEX1:41;
then A17: (p|--pq).p=1 by A13,RLAFFIN1:72;
A18: q in pq & pq c=Affin pq by RLAFFIN1:49,TARSKI:def 2;
then W=(1-a)*(p|--pq)+a*(q|--pq) by A14,A13,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 A16,RLVECT_2:def 11
.=1-a by A17;
then W.p<=1-0 by A15,XREAL_1:10;
then A19: W.p in L by XXREAL_1:234;
(1-a)+a=1;
then reconsider w=x as Element of TRn|Apq by A6,A14,A13,A18,RLAFFIN1:78;
len wE=2 by A7,Th16;
then A20: len(wE|1)=1 by FINSEQ_1:59;
then reconsider wE1=wE|1 as Point of TOP-REAL 1 by TOPREAL3:46;
A21: 1 in dom wE1 by A20,FINSEQ_3:25;
then A22: wE1/.1=wE1.1 & wE1.1=wE.1 by FUNCT_1:47,PARTFUN1:def 6;
A23: 1 in dom wE by A21,RELAT_1:57;
h.wE1=wE1/.1 by A5;
then h.wE1 in L by A4,A19,A22,A23,FUNCT_1:12;
then wE1 in h"L by A9,FUNCT_1:def 7;
then w in B;
hence thesis;
end;
L is closed by BORSUK_5:41;
then h"L is closed by A8,TOPGRP_1:24;
then A24: B is closed by A7,Th28;
B c=halfline(p,q)
proof
let x be object;
assume x in B;
then consider w be Element of TRn|Apq such that
A25: x=w and
A26: (w|--E)|1 in h"L;
set W=w|--pq,wE=w|--E;
reconsider wE1=wE|1 as Point of TR1 by A26;
A27: h.wE1=wE1/.1 by A5;
len wE1=1 by CARD_1:def 7;
then A28: 1 in dom wE1 by FINSEQ_3:25;
then A29: wE1/.1=wE1.1 & wE1.1=wE.1 by FUNCT_1:47,PARTFUN1:def 6;
A30: 1 in dom wE by A28,RELAT_1:57;
h.(wE|1) in L by A26,FUNCT_1:def 7;
then W.p in L by A4,A27,A29,A30,FUNCT_1:12;
then W.p<=1 by XXREAL_1:234;
then A31: W.p-W.p<=1-W.p by XREAL_1:9;
A32: sum W=1 by A6,RLAFFIN1:def 7;
Carrier W c=pq by RLVECT_2:def 6;
then A33: sum W=W.p+W.q by A2,RLAFFIN1:33;
Sum W=w by A6,RLAFFIN1:def 7;
then w=(1-W.q)*p+W.q*q by A2,A33,A32,RLVECT_2:33;
hence thesis by A25,A33,A32,A31,TOPREAL9:26;
end;
then halfline(p,q)=B by A10;
hence thesis by A6,A24,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(object)=($1|--A).x;
A1: for v be object st v in the carrier of V
holds F(v) in the carrier of R^1
proof
let v be object 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 object 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 object;
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 object;
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 object 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;
A20: AA is non empty by A9;
A21: B c=AxA"P
proof
let y be object;
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 object;
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;
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(object)=|--(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 object;
assume y in rng f;
then consider x be object 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 object;
assume A11: x in meet rng f;
A12: now let v be Element of TRn;
assume v in A;
then consider k be object 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 object;
assume A20: x in conv A;
now let Y be set;
assume Y in rng f;
then consider k be object 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 object 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(object)=|--(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 object;
assume y in rng f;
then consider x be object 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 object;
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 object 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 object;
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;
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 object;
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 object 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 object 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;