:: Sperner's Lemma
:: by Karol P\c{a}k
::
:: Received February 9, 2010
:: Copyright (c) 2010 Association of Mizar Users
environ
vocabularies ARYTM_1, ARYTM_3, XBOOLE_0, CARD_1, CARD_2, CLASSES1, COHSP_1,
COMPLEX1, CONVEX1, CONVEX2, CONVEX3, FINSEQ_1, FINSET_1, FUNCT_1,
MATROID0, MCART_1, ORDERS_1, PARTFUN1, PRE_TOPC, QC_LANG1, RELAT_1,
RLVECT_1, RLVECT_2, SEMI_AF1, SETFAM_1, SGRAPH1, SUBSET_1, TARSKI,
TOPS_1, ZFMISC_1, RLAFFIN1, RLAFFIN2, SIMPLEX0, SIMPLEX1, REAL_1,
FUNCOP_1, NAT_1, FUNCT_2, STRUCT_0, XXREAL_0, NUMBERS, ORDINAL1, CARD_3,
GLIB_000, FINSEQ_4;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, NAT_1,
XXREAL_3, XXREAL_0, ORDERS_1, CARD_1, REAL_1, FINSET_1, SETFAM_1,
DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1, FINSEQ_1, STRUCT_0,
CLASSES1, RVSUM_1, RLVECT_1, RLVECT_2, CONVEX1, CONVEX2, CONVEX3,
PRE_TOPC, RLAFFIN1, FUNCOP_1, PENCIL_1, MATROID0, MCART_1, CARD_2,
COHSP_1, SIMPLEX0, RLAFFIN2;
constructors BINOP_2, CONVEX1, CONVEX3, REAL_1, RVSUM_1, SEQ_1, SETFAM_1,
RLAFFIN1, SIMPLEX0, TOPS_2, LEXBFS, XXREAL_2, BORSUK_1, COHSP_1, CARD_2,
REARRAN1, RLAFFIN2;
registrations CARD_1, FINSET_1, FUNCT_1, MEMBERED, NAT_1, RELAT_1, RLVECT_1,
STRUCT_0, SUBSET_1, VALUED_0, XCMPLX_0, XREAL_0, XXREAL_0, XBOOLE_0,
RLAFFIN1, SIMPLEX0, FUNCOP_1, INT_1, XXREAL_3, MATROID0, REALSET1,
SETFAM_1, COHSP_1, RLAFFIN2, RELSET_1, ZFMISC_1, DILWORTH, RLVECT_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions MATROID0, ORDERS_1, ORDINAL1, RLAFFIN2, RLVECT_2, SETFAM_1,
STRUCT_0, SIMPLEX0, TARSKI, TOPS_2, XBOOLE_0, XXREAL_3;
theorems BORSUK_5, CARD_1, CARD_2, CARD_FIN, CLASSES1, COHSP_1, CONVEX1,
CONVEX3, FINSEQ_1, FINSEQ_3, FUNCOP_1, FUNCT_1, FUNCT_2, INT_1, MATROID0,
MCART_1, NAT_1, ORDINAL1, PENCIL_1, PRE_TOPC, RELAT_1, RELSET_2,
RLTOPSP1, RLVECT_1, RLVECT_2, RVSUM_1, SETFAM_1, STIRL2_1, TARSKI,
TOPS_2, WELLORD2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, XXREAL_3,
ZFMISC_1, RLAFFIN1, RLAFFIN2, SIMPLEX0;
schemes CLASSES1, FUNCT_1, FUNCT_2, NAT_1, RELAT_1;
begin :: Preliminaries
reserve x,y,X for set,
r for Real,
n,k for Nat;
theorem Th1:
for R be Relation, C be Cardinal st for x st x in X holds card Im(R,x) = C
holds card R = card(R|(dom R\X)) +` C*`card X
proof
let R be Relation,C be Cardinal such that
A1: for x st x in X holds card Im(R,x)=C;
set DA=(dom R)\X;
per cases;
suppose A2: X c=dom R;
deffunc F(set)=Im(R,$1);
consider f be Function such that
A3: dom f=X & for x st x in X holds f.x=F(x) from FUNCT_1:sch 3;
defpred P[set,set] means
ex g be Function st g=$2 & dom g=f.$1 & rng g=C & g is one-to-one;
A4: for x st x in X ex y st P[x,y]
proof
let x;
assume x in X;
then f.x=Im(R,x) & card Im(R,x)=C by A1,A3;
then f.x,C are_equipotent by CARD_1:def 5;
then consider g be Function such that
A5: g is one-to-one & dom g=f.x & rng g=C by WELLORD2:def 4;
take g;
thus thesis by A5;
end;
consider ff be Function such that
A6: dom ff=X & for x st x in X holds P[x,ff.x] from CLASSES1:sch 1(A4);
now let x;
assume x in dom ff;
then ex g be Function st g=ff.x & dom g=f.x & rng g=C & g is one-to-one by
A6;
hence ff.x is Function;
end;
then reconsider ff as Function-yielding Function by FUNCOP_1:def 6;
deffunc G(set)=[$1`1,(ff.($1`1)).($1`2)];
consider p be Function such that
A7: dom p=R|X & for x st x in R|X holds p.x=G(x) from FUNCT_1:sch 3;
A8: rng p=[:X,C:]
proof
hereby let y;
assume y in rng p;
then consider x such that
A9: x in dom p and
A10: p.x=y by FUNCT_1:def 5;
A11: p.x=[x`1,(ff.(x`1)).(x`2)] by A7,A9;
A12: x=[x`1,x`2] by A7,A9,MCART_1:23;
then x`1 in {x`1} & x in R by A7,A9,RELAT_1:def 11,TARSKI:def 1;
then A13: x`2 in R.:{x`1} by A12,RELAT_1:def 13;
A14: x`1 in X by A7,A9,A12,RELAT_1:def 11;
then consider g be Function such that
A15: g=ff.(x`1) and
A16: dom g=f.(x`1) and
A17: rng g=C and
g is one-to-one by A6;
f.(x`1)=Im(R,x`1) by A3,A14;
then x`2 in dom g by A13,A16,RELAT_1:def 16;
then g.(x`2) in C by A17,FUNCT_1:def 5;
hence y in [:X,C:] by A10,A11,A14,A15,ZFMISC_1:106;
end;
let y;
assume y in [:X,C:];
then consider y1,y2 be set such that
A18: y1 in X and
A19: y2 in C and
A20: y=[y1,y2] by ZFMISC_1:def 2;
consider g be Function such that
A21: g=ff.y1 and
A22: dom g=f.y1 and
A23: rng g=C and
g is one-to-one by A6,A18;
consider x2 be set such that
A24: x2 in dom g and
A25: g.x2=y2 by A19,A23,FUNCT_1:def 5;
[y1,x2]`1=y1 by MCART_1:7;
then A26: G([y1,x2])=y by A20,A21,A25,MCART_1:7;
f.y1=Im(R,y1) by A3,A18;
then [y1,x2] in R by A22,A24,RELSET_2:9;
then A27: [y1,x2] in R|X by A18,RELAT_1:def 11;
then p.([y1,x2])=G([y1,x2]) by A7;
hence thesis by A7,A26,A27,FUNCT_1:def 5;
end;
now let x1,x2 be set such that
A28: x1 in dom p and
A29: x2 in dom p and
A30: p.x1=p.x2;
A31: p.x1=G(x1) & p.x2=G(x2) by A7,A28,A29;
then A32: x1`1=x2`1 by A30,ZFMISC_1:33;
A33: x1=[x1`1,x1`2] by A7,A28,MCART_1:23;
then x1 in R by A7,A28,RELAT_1:def 11;
then A34: x1`2 in Im(R,x1`1) by A33,RELSET_2:9;
A35: x2=[x2`1,x2`2] by A7,A29,MCART_1:23;
then x2 in R by A7,A29,RELAT_1:def 11;
then A36: x2`2 in Im(R,x2`1) by A35,RELSET_2:9;
x2`1 in X by A7,A29,A35,RELAT_1:def 11;
then consider g2 be Function such that
A37: g2=ff.(x2`1) and
dom g2=f.(x2`1) and
rng g2=C and
g2 is one-to-one by A6;
A38: x1`1 in X by A7,A28,A33,RELAT_1:def 11;
then consider g1 be Function such that
A39: g1=ff.(x1`1) and
A40: dom g1=f.(x1`1) and
rng g1=C and
A41: g1 is one-to-one by A6;
A42: f.(x1`1)=Im(R,x1`1) by A3,A38;
g1.(x1`2)=g2.(x2`2) by A30,A31,A37,A39,ZFMISC_1:33;
hence x1=x2 by A32,A35,A36,A33,A34,A37,A39,A40,A41,A42,FUNCT_1:def 8;
end;
then p is one-to-one by FUNCT_1:def 8;
then R|X,[:X,C:]are_equipotent by A7,A8,WELLORD2:def 4;
then A43: card(R|X)=card[:X,C:] by CARD_1:21
.=card[:card X,C:] by CARD_2:14
.=C*`card X by CARD_2:def 2;
A44: R|X misses R|DA
proof
assume R|X meets R|DA;
then consider x such that
A45: x in R|X and
A46: x in R|DA by XBOOLE_0:3;
consider x1,x2 be set such that
A47: x=[x1,x2] by A45,RELAT_1:def 1;
x1 in X & x1 in DA by A45,A46,A47,RELAT_1:def 11;
hence contradiction by XBOOLE_0:def 5;
end;
DA\/X=dom R\/X by XBOOLE_1:39
.=dom R by A2,XBOOLE_1:12;
then (R|X)\/(R|DA)=R|(dom R) by RELAT_1:107
.=R by RELAT_1:98;
hence card R=card(R|DA)+`C*`card X by A43,A44,CARD_2:48;
end;
suppose not X c=dom R;
then consider x such that
A48: x in X and
A49: not x in dom R by TARSKI:def 3;
Im(R,x)={}
proof
assume Im(R,x)<>{};
then consider y such that
A50: y in Im(R,x) by XBOOLE_0:def 1;
[x,y] in R by A50,RELSET_2:9;
hence contradiction by A49,RELAT_1:20;
end;
then A51: C=card{} by A1,A48;
dom R misses X
proof
assume dom R meets X;
then consider x such that
A52: x in dom R and
A53: x in X by XBOOLE_0:3;
card Im(R,x)=C by A1,A53;
then A54: Im(R,x) is empty by A51;
ex y st[x,y] in R by A52,RELAT_1:def 4;
hence contradiction by A54,RELSET_2:9;
end;
then A55: DA=dom R by XBOOLE_1:83;
C*`card X=0 by A51,CARD_2:32;
then card(R|DA)+`C*`card X=card(R|DA) by CARD_2:29;
hence thesis by A55,RELAT_1:98;
end;
end;
theorem Th2:
for Y be non empty finite set st card X = card Y+1
for f be Function of X,Y st f is onto
ex y st y in Y & card(f"{y}) = 2 &
for x st x in Y & x <> y holds card (f"{x})=1
proof
let Y be non empty finite set such that
A1: card X=card Y+1;
reconsider XX=X as non empty finite set by A1;
card Y>0;
then reconsider c1=card Y-1 as Element of NAT by NAT_1:20;
let f be Function of X,Y such that
A2: f is onto;
A3: rng f=Y by A2,FUNCT_2:def 3;
reconsider F=f as Function of XX,Y;
A4: dom f=X by FUNCT_2:def 1;
ex y st y in Y & card(F"{y})>1
proof
assume A5: for y st y in Y holds card(F"{y})<=1;
now let y;
set fy=F"{y};
assume A6: y in Y;
then fy<>{} by A3,FUNCT_1:142;
then card fy=1 by A5,A6,NAT_1:26;
hence ex x st fy={x} by CARD_2:60;
end;
then f is one-to-one by A3,FUNCT_1:144;
then X,Y are_equipotent by A3,A4,WELLORD2:def 4;
then card X=card Y by CARD_1:21;
hence contradiction by A1;
end;
then consider y such that
A7: y in Y and
A8: card(F"{y})>1;
set fy=F"{y};
set fD=F|(dom f\fy);
take y;
A9: 1+1<=card fy by A8,NAT_1:13;
dom fD=dom f\fy by RELAT_1:91,XBOOLE_1:36;
then A10: card dom fD=card XX-card fy by A4,CARD_2:63;
set Yy=Y\{y};
A11: rng fD=Yy by A3,STIRL2_1:64;
then reconsider FD=fD as Function of dom fD,Yy by FUNCT_2:3;
card Y=c1+1;
then A12: card Yy=c1 by A7,STIRL2_1:65;
then c1 c=card dom fD by A11,CARD_1:28;
then card Y+-1<=card Y+(1-card fy) by A1,A10,NAT_1:40;
then -1<=1-card fy by XREAL_1:8;
then card fy<=1--1 by XREAL_1:13;
hence A13: y in Y & card(f"{y})=2 by A7,A9,XXREAL_0:1;
let x such that
A14: x in Y and
A15: x<>y;
A16: x in rng FD by A11,A14,A15,ZFMISC_1:64;
FD is onto by A11,FUNCT_2:def 3;
then FD is one-to-one by A1,A10,A12,A13,STIRL2_1:70;
then A17: ex z be set st FD"{x}={z} by A16,FUNCT_1:144;
FD"{x}=f"{x} by A15,STIRL2_1:64;
hence thesis by A17,CARD_1:50;
end;
definition
let X be 1-sorted;
mode SimplicialComplexStr of X is SimplicialComplexStr of the carrier of X;
mode SimplicialComplex of X is SimplicialComplex of the carrier of X;
end;
definition
let X be 1-sorted;
let K be SimplicialComplexStr of X;
let A be Subset of K;
func @A -> Subset of X equals
A;
coherence
proof
[#]K c=the carrier of X by SIMPLEX0:def 9;
hence thesis by XBOOLE_1:1;
end;
end;
definition
let X be 1-sorted;
let K be SimplicialComplexStr of X;
let A be Subset-Family of K;
func @A -> Subset-Family of X equals
A;
coherence
proof
[#]K c=the carrier of X by SIMPLEX0:def 9;
then bool[#]K c=bool the carrier of X by ZFMISC_1:79;
hence thesis by XBOOLE_1:1;
end;
end;
theorem Th3:
for X be 1-sorted
for K be subset-closed SimplicialComplexStr of X st K is total
for S be finite Subset of K st S is simplex-like
holds Complex_of {@S} is SubSimplicialComplex of K
proof
let X be 1-sorted;
let K be subset-closed SimplicialComplexStr of X such that
A1: K is total;
let S be finite Subset of K such that
A2: S is simplex-like;
S in the topology of K by A2,PRE_TOPC:def 5;
then A3: {S}c=the topology of K by ZFMISC_1:37;
set C=Complex_of{@S};
A4: [#]C c=[#]K by A1,SIMPLEX0:def 10;
the_family_of K is subset-closed;
then the topology of C c=the topology of K by A3,SIMPLEX0:def 1;
hence thesis by A4,SIMPLEX0:def 13;
end;
begin :: The Area of an Abstract Simplicial Complex
reserve RLS for non empty RLSStruct,
Kr,K1r,K2r for SimplicialComplexStr of RLS,
V for RealLinearSpace,
Kv for non void SimplicialComplex of V;
definition let RLS,Kr;
func |.Kr.| -> Subset of RLS means :Def3:
x in it iff ex A be Subset of Kr st A is simplex-like & x in conv @A;
existence
proof
set KC={conv@A where A is Subset of Kr:A is simplex-like};
KC c=bool the carrier of RLS
proof
let x;
assume x in KC;
then ex A be Subset of Kr st x=conv@A & A is simplex-like;
hence thesis;
end;
then reconsider KC as Subset-Family of RLS;
take IT=union KC;
let x;
hereby assume x in IT;
then consider y such that
A1: x in y and
A2: y in KC by TARSKI:def 4;
consider A be Subset of Kr such that
A3: y=conv@A & A is simplex-like by A2;
take A;
thus A is simplex-like & x in conv@A by A1,A3;
end;
given A be Subset of Kr such that
A4: A is simplex-like and
A5: x in conv@A;
conv@A in KC by A4;
hence thesis by A5,TARSKI:def 4;
end;
uniqueness
proof
let S1,S2 be Subset of RLS such that
A6: x in S1 iff ex A be Subset of Kr st A is simplex-like & x in conv@A and
A7: x in S2 iff ex A be Subset of Kr st A is simplex-like & x in conv@A;
now let x;
x in S1 iff ex A be Subset of Kr st A is simplex-like & x in conv@A by A6;
hence x in S1 iff x in S2 by A7;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th4:
the topology of K1r c= the topology of K2r implies |.K1r.| c= |.K2r.|
proof
assume A1: the topology of K1r c=the topology of K2r;
let x;
assume x in |.K1r.|;
then consider A be Subset of K1r such that
A2: A is simplex-like and
A3: x in conv@A by Def3;
A4: A in the topology of K1r by A2,PRE_TOPC:def 5;
then A in the topology of K2r by A1;
then reconsider A1=A as Subset of K2r;
@A=@A1 & A1 is simplex-like by A1,A4,PRE_TOPC:def 5;
hence thesis by A3,Def3;
end;
theorem Th5:
for A be Subset of Kr st A is simplex-like holds conv @A c= |.Kr.|
proof
let A be Subset of Kr such that
A1: A is simplex-like;
let x;
thus thesis by A1,Def3;
end;
theorem
for K be subset-closed SimplicialComplexStr of V holds
x in |.K.| iff ex A be Subset of K st A is simplex-like & x in Int @A
proof
let K be subset-closed SimplicialComplexStr of V;
hereby assume x in |.K.|;
then consider A be Subset of K such that
A1: A is simplex-like and
A2: x in conv@A by Def3;
conv@A=union{Int B where B is Subset of V:B c=@A} by RLAFFIN2:8;
then consider IB be set such that
A3: x in IB and
A4: IB in {Int B where B is Subset of V:B c=@A} by A2,TARSKI:def 4;
consider B be Subset of V such that
A5: IB=Int B and
A6: B c=@A by A4;
reconsider B1=B as Subset of K by A6,XBOOLE_1:1;
take B1;
A in the topology of K by A1,PRE_TOPC:def 5;
then K is non void by PENCIL_1:def 4;
hence B1 is simplex-like & x in Int@B1 by A1,A3,A5,A6,MATROID0:1;
end;
given A be Subset of K such that
A7: A is simplex-like and
A8: x in Int@A;
x in conv@A by A8,RLAFFIN2:def 1;
hence thesis by A7,Def3;
end;
theorem Th7:
|.Kr.| is empty iff Kr is empty-membered
proof
hereby assume A1: |.Kr.| is empty;
assume Kr is with_non-empty_element;
then the topology of Kr is with_non-empty_element by SIMPLEX0:def 7;
then consider x be non empty set such that
A2: x in the topology of Kr by SETFAM_1:def 11;
reconsider X=x as Subset of Kr by A2;
(ex y st y in conv@X) & X is simplex-like by A2,PRE_TOPC:def 5,XBOOLE_0:def
1;
hence contradiction by A1,Def3;
end;
assume A3: Kr is empty-membered;
assume|.Kr.| is non empty;
then consider x such that
A4: x in |.Kr.| by XBOOLE_0:def 1;
consider A be Subset of Kr such that
A5: A is simplex-like & x in conv@A by A4,Def3;
A is non empty & A in the topology of Kr by A5,PRE_TOPC:def 5;
then the topology of Kr is with_non-empty_element by SETFAM_1:def 11;
hence contradiction by A3,SIMPLEX0:def 7;
end;
theorem Th8:
for A be Subset of RLS holds |.Complex_of{A}.| = conv A
proof
let A be Subset of RLS;
set C=Complex_of{A};
reconsider A1=A as Subset of C;
A1: the topology of C=bool A by SIMPLEX0:4;
hereby let x;
assume x in |.C.|;
then consider S be Subset of C such that
A2: S is simplex-like and
A3: x in conv@S by Def3;
S in the topology of C by A2,PRE_TOPC:def 5;
then conv@S c=conv A by A1,RLAFFIN1:3;
hence x in conv A by A3;
end;
A c=A;
then @A1=A & A1 is simplex-like by A1,PRE_TOPC:def 5;
hence thesis by Th5;
end;
theorem
for A,B be Subset-Family of RLS holds
|.Complex_of (A\/B).| = |.Complex_of A.| \/ |.Complex_of B.|
proof
let A,B be Subset-Family of RLS;
set CA=Complex_of A,CB=Complex_of B,CAB=Complex_of(A\/B);
A1: (the topology of CA)\/the topology of CB=the topology of CAB by SIMPLEX0:
5;
thus|.CAB.|c=|.CA.|\/|.CB.|
proof
let x;
assume x in |.CAB.|;
then consider S be Subset of CAB such that
A2: S is simplex-like and
A3: x in conv@S by Def3;
A4: S in the topology of CAB by A2,PRE_TOPC:def 5;
per cases by A1,A4,XBOOLE_0:def 3;
suppose A5: S in the topology of CA;
reconsider S1=S as Subset of CA;
@S=@S1 & S1 is simplex-like by A5,PRE_TOPC:def 5;
then conv@S c=|.CA.| by Th5;
hence thesis by A3,XBOOLE_0:def 3;
end;
suppose A6: S in the topology of CB;
reconsider S1=S as Subset of CB;
@S=@S1 & S1 is simplex-like by A6,PRE_TOPC:def 5;
then conv@S c=|.CB.| by Th5;
hence thesis by A3,XBOOLE_0:def 3;
end;
end;
|.CA.|c=|.CAB.| & |.CB.|c=|.CAB.| by A1,Th4,XBOOLE_1:7;
hence thesis by XBOOLE_1:8;
end;
begin :: The Subdivision of a Simplicial Complex
definition let RLS,Kr;
mode SubdivisionStr of Kr -> SimplicialComplexStr of RLS means :Def4:
|.Kr.| c= |.it.| & for A be Subset of it st A is simplex-like
ex B be Subset of Kr st B is simplex-like & conv @A c= conv @B;
existence
proof
take Kr;
thus thesis;
end;
end;
theorem Th10:
for P be SubdivisionStr of Kr holds |.Kr.| = |.P.|
proof
let P be SubdivisionStr of Kr;
thus|.Kr.|c=|.P.| by Def4;
let x;
assume x in |.P.|;
then consider A be Subset of P such that
A1: A is simplex-like and
A2: x in conv@A by Def3;
ex B be Subset of Kr st B is simplex-like & conv@A c=conv@B by A1,Def4;
hence thesis by A2,Def3;
end;
registration let RLS;
let Kr be with_non-empty_element SimplicialComplexStr of RLS;
cluster -> with_non-empty_element SubdivisionStr of Kr;
coherence
proof
let P be SubdivisionStr of Kr;
|.Kr.| is non empty & |.Kr.|=|.P.| by Th7,Th10;
hence thesis by Th7;
end;
end;
theorem Th11:
Kr is SubdivisionStr of Kr
proof
thus|.Kr.|c=|.Kr.|;
thus thesis;
end;
theorem Th12:
Complex_of the topology of Kr is SubdivisionStr of Kr
proof
set TOP=the topology of Kr;
set C=Complex_of TOP;
[#]C=[#]Kr & [#]Kr c=the carrier of RLS by SIMPLEX0:def 9;
then reconsider C as SimplicialComplexStr of RLS by SIMPLEX0:def 9;
A1: |.Kr.|c=|.C.|
proof
let x;
assume x in |.Kr.|;
then consider A be Subset of Kr such that
A2: A is simplex-like and
A3: x in conv@A by Def3;
reconsider B=A as Subset of C;
A in TOP by A2,PRE_TOPC:def 5;
then A in the topology of C by SIMPLEX0:2;
then A4: B is simplex-like by PRE_TOPC:def 5;
@A=@B;
hence thesis by A3,A4,Def3;
end;
for A be Subset of C st A is simplex-like ex B be Subset of Kr st B is
simplex-like & conv@A c=conv@B
proof
let A be Subset of C;
assume A is simplex-like;
then A in the topology of C by PRE_TOPC:def 5;
then consider B be set such that
A5: A c=B and
A6: B in TOP by SIMPLEX0:2;
reconsider B as Subset of Kr by A6;
take B;
thus thesis by A5,A6,PRE_TOPC:def 5,RLAFFIN1:3;
end;
hence thesis by A1,Def4;
end;
theorem Th13:
for K be subset-closed SimplicialComplexStr of V
for SF be Subset-Family of K st SF = Sub_of_Fin the topology of K
holds Complex_of SF is SubdivisionStr of K
proof
let K be subset-closed SimplicialComplexStr of V;
set TOP=the topology of K;
let SF be Subset-Family of K such that
A1: SF=Sub_of_Fin TOP;
set C=Complex_of SF;
[#]C=[#]K & [#]K c=the carrier of V by SIMPLEX0:def 9;
then reconsider C as SimplicialComplexStr of V by SIMPLEX0:def 9;
A2: the_family_of K is subset-closed;
then A3: the topology of C=SF by A1,SIMPLEX0:7;
C is SubdivisionStr of K
proof
thus|.K.|c=|.C.|
proof
let x;
assume x in |.K.|;
then consider S be Subset of K such that
A4: S is simplex-like and
A5: x in conv@S by Def3;
reconsider S1=@S as non empty Subset of V by A5;
x in {Sum(L) where L is Convex_Combination of S1:
L in ConvexComb(V)} by A5,CONVEX3:5;
then consider L be Convex_Combination of S1 such that
A6: x=Sum L & L in ConvexComb(V);
reconsider Carr=Carrier L as non empty Subset of V by CONVEX1:21;
A7: Carr c=S by RLVECT_2:def 8;
then reconsider Carr1=Carr as Subset of C by XBOOLE_1:1;
S in TOP by A4,PRE_TOPC:def 5;
then Carr1 in TOP by A2,A7,CLASSES1:def 1;
then Carr1 in the topology of C by A1,A3,COHSP_1:def 3;
then A8: Carr1 is simplex-like by PRE_TOPC:def 5;
reconsider LC=L as Linear_Combination of Carr by RLVECT_2:def 8;
LC is convex;
then x in {Sum(M) where M is Convex_Combination of Carr:M in ConvexComb(V)}
by A6;
then A9: x in conv Carr by CONVEX3:5;
Carr=@Carr1;
hence thesis by A8,A9,Def3;
end;
let A be Subset of C;
reconsider B=A as Subset of K;
assume A is simplex-like;
then A in the topology of C by PRE_TOPC:def 5;
then A10: B is simplex-like by A1,A3,PRE_TOPC:def 5;
@A=@B;
hence thesis by A10;
end;
hence thesis;
end;
theorem Th14:
for P1 be SubdivisionStr of Kr for P2 be SubdivisionStr of P1
holds P2 is SubdivisionStr of Kr
proof
let P1 be SubdivisionStr of Kr;
let P2 be SubdivisionStr of P1;
|.P2.|=|.P1.| by Th10
.=|.Kr.| by Th10;
hence |.Kr.|c=|.P2.|;
let A2 be Subset of P2;
assume A2 is simplex-like;
then consider A1 be Subset of P1 such that
A1: A1 is simplex-like and
A2: conv@A2 c=conv@A1 by Def4;
ex A be Subset of Kr st A is simplex-like & conv@A1 c=conv@A by A1,Def4;
hence thesis by A2,XBOOLE_1:1;
end;
registration
let V;
let K be SimplicialComplexStr of V;
cluster finite-membered subset-closed SubdivisionStr of K;
existence
proof
reconsider C=Complex_of the topology of K as SubdivisionStr of K by Th12;
reconsider SF=Sub_of_Fin the topology of C as Subset-Family of C by XBOOLE_1:
1;
Complex_of SF is SubdivisionStr of C by Th13;
then reconsider CSF=Complex_of SF as SubdivisionStr of K by Th14;
take CSF;
thus thesis;
end;
end;
definition
let V;
let K be SimplicialComplexStr of V;
mode Subdivision of K is finite-membered subset-closed SubdivisionStr of K;
end;
theorem Th15:
for K be with_empty_element SimplicialComplex of V st |.K.| c= [#]K
for B be Function of BOOL the carrier of V,the carrier of V st
for S be Simplex of K st S is non empty holds B.S in conv @S
holds subdivision(B,K) is SubdivisionStr of K
proof
let K be with_empty_element SimplicialComplex of V such that
A1: |.K.|c=[#]K;
let B be Function of BOOL the carrier of V,the carrier of V such that
A2: for S be Simplex of K st S is non empty holds B.S in conv@S;
set P=subdivision(B,K);
defpred P[Nat] means
for x for A be Simplex of K st x in conv@A & card A=$1ex S be c=-linear
finite simplex-like Subset-Family of K,BS be Subset of P st BS=B.:S & x in conv
@BS & union S c=A;
A3: dom B=BOOL the carrier of V by FUNCT_2:def 1;
A4: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A5: P[n];
let x be set,A be Simplex of K such that
A6: x in conv@A and
A7: card A=n+1;
reconsider A1=@A as non empty Subset of V by A6;
A8: union{A}=A by ZFMISC_1:31;
A9: for P be Subset of K holds P in {A} implies P is simplex-like by TARSKI:
def 1;
then A10: {A} is simplex-like by TOPS_2:def 1;
A11: B.A1 in conv@A by A2;
then reconsider BA=B.A as Element of V;
A1=A;
then A12: A in dom B by A3,ZFMISC_1:64;
A13: B.:{A}=Im(B,A) by RELAT_1:def 16;
then A14: B.:{A}={BA} by A12,FUNCT_1:117;
BA in conv A1 & conv A1 c=|.K.| by A2,Th5;
then BA in |.K.|;
then [#]P=[#]K & {BA} is Subset of K by A1,SIMPLEX0:def 20,ZFMISC_1:37;
then reconsider BY=B.:{A} as Subset of P by A12,A13,FUNCT_1:117;
per cases;
suppose A15: x=B.A;
now let x1,x2 be set;
assume that
A16: x1 in {A} and
A17: x2 in {A};
x1=A by A16,TARSKI:def 1;
hence x1,x2 are_c=-comparable by A17,TARSKI:def 1;
end;
then reconsider Y={A} as c=-linear finite simplex-like Subset-Family of K
by A9,ORDINAL1:def 9,TOPS_2:def 1;
take Y,BY;
conv{BA}={BA} by RLAFFIN1:1;
hence thesis by A14,A15,TARSKI:def 1,ZFMISC_1:31;
end;
suppose x<>B.A;
then consider p,w be Element of V,r such that
A18: p in A and
A19: w in conv(A1\{p}) and
A20: 0<=r & r<1 & r*BA+(1-r)*w=x by A6,A11,RLAFFIN2:26;
@(A\{p})=A1\{p} & card(A\{p})=n by A7,A18,STIRL2_1:65;
then consider S be c=-linear finite simplex-like Subset-Family of K,BS be
Subset of P such that
A21: BS=B.:S and
A22: w in conv@BS and
A23: union S c=A\{p} by A5,A19;
set S1=S\/{A};
A24: A\{p}c=A by XBOOLE_1:36;
then A25: union S c=A by A23,XBOOLE_1:1;
for x1,x2 be set st x1 in S1 & x2 in S1 holds x1,x2 are_c=-comparable
proof
let x1,x2 be set such that
A26: x1 in S1 & x2 in S1;
per cases by A26,XBOOLE_0:def 3;
suppose x1 in S & x2 in S;
hence thesis by ORDINAL1:def 9;
end;
suppose x1 in S & x2 in {A};
then x1 c=union S & x2=A by TARSKI:def 1,ZFMISC_1:92;
then x1 c=x2 by A25,XBOOLE_1:1;
hence thesis by XBOOLE_0:def 9;
end;
suppose x2 in S & x1 in {A};
then x2 c=union S & x1=A by TARSKI:def 1,ZFMISC_1:92;
then x2 c=x1 by A25,XBOOLE_1:1;
hence thesis by XBOOLE_0:def 9;
end;
suppose A27: x1 in {A} & x2 in {A};
then x1=A by TARSKI:def 1;
hence thesis by A27,TARSKI:def 1;
end;
end;
then reconsider S1 as c=-linear finite simplex-like Subset-Family of K by
A10,ORDINAL1:def 9,TOPS_2:20;
A28: B.:S1=BS\/BY by A21,RELAT_1:153;
then reconsider BS1=B.:S1 as Subset of P;
A29: conv@BS c=conv@BS1 by A28,RLTOPSP1:21,XBOOLE_1:7;
BA in BY by A14,TARSKI:def 1;
then A30: BA in @BS1 by A28,XBOOLE_0:def 3;
take S1,BS1;
A31: @BS1 c=conv@BS1 by CONVEX1:41;
union S1=union S\/A by A8,ZFMISC_1:96
.=A by A23,A24,XBOOLE_1:1,12;
hence thesis by A20,A22,A29,A30,A31,RLTOPSP1:def 1;
end;
end;
A32: P[0 qua Nat]
proof
let x;
let A be Simplex of K;
assume that
A33: x in conv@A and
A34: card A=0;
@A is non empty by A33;
hence thesis by A34;
end;
A35: for n be Nat holds P[n] from NAT_1:sch 2(A32,A4);
thus|.K.|c=|.P.|
proof
let x;
assume x in |.K.|;
then consider A be Subset of K such that
A36: A is simplex-like and
A37: x in conv@A by Def3;
reconsider A as Simplex of K by A36;
P[card A] by A35;
then consider S be c=-linear finite simplex-like Subset-Family of K,BS be
Subset of P such that
A38: BS=B.:S and
A39: x in conv@BS and
union S c=A by A37;
BS is simplex-like by A38,SIMPLEX0:def 20;
then conv@BS c=|.P.| by Th5;
hence thesis by A39;
end;
for A be Subset of P st A is simplex-like ex B be Subset of K st B is
simplex-like & conv@A c=conv@B
proof
let A be Subset of P;
assume A is simplex-like;
then consider S be c=-linear finite simplex-like Subset-Family of K such
that
A40: A=B.:S by SIMPLEX0:def 20;
per cases;
suppose A41: S is empty;
take{}K;
thus thesis by A40,A41,RELAT_1:149;
end;
suppose A42: S is non empty;
take U=union S;
A43: A c=conv@U
proof
let x;
assume x in A;
then consider y such that
A44: y in dom B and
A45: y in S and
A46: B.y=x by A40,FUNCT_1:def 12;
reconsider y as Simplex of K by A45,TOPS_2:def 1;
y<>{} by A44,ZFMISC_1:64;
then A47: B.y in conv@y by A2;
conv@y c=conv@U by A45,RLTOPSP1:21,ZFMISC_1:92;
hence thesis by A46,A47;
end;
U in S by A42,SIMPLEX0:9;
hence thesis by A43,CONVEX1:30,TOPS_2:def 1;
end;
end;
hence thesis;
end;
registration let V,Kv;
cluster non void Subdivision of Kv;
existence
proof
reconsider P=Kv as Subdivision of Kv by Th11;
take P;
thus thesis;
end;
end;
begin :: The Barycentric Subdivision
definition
let V,Kv such that
A1: |.Kv.| c= [#]Kv;
func BCS Kv -> non void Subdivision of Kv equals :Def5:
subdivision(center_of_mass V,Kv);
coherence
proof
set B=center_of_mass V;
for S be Simplex of Kv st S is non empty holds B.S in conv@S by RLAFFIN2:16;
hence thesis by A1,Th15;
end;
end;
definition let n;
let V,Kv such that
A1: |.Kv.| c= [#]Kv;
func BCS(n,Kv) -> non void Subdivision of Kv equals :Def6:
subdivision(n,center_of_mass V,Kv);
coherence
proof
defpred P[Nat] means
subdivision($1,center_of_mass V,Kv) is non void Subdivision of Kv;
A2: for k st P[k] holds P[k+1]
proof
let k;
assume P[k];
then reconsider P=subdivision(k,center_of_mass V,Kv)
as non void Subdivision of Kv;
A3: |.P.|=|.Kv.| & [#]P=[#]Kv by Th10,SIMPLEX0:64;
k in NAT by ORDINAL1:def 13;
then subdivision(k+1,center_of_mass V,Kv)=
subdivision(1,center_of_mass V,subdivision(k,center_of_mass V,Kv))
by SIMPLEX0:63
.=subdivision(center_of_mass V,P) by SIMPLEX0:62
.=BCS P by A1,A3,Def5;
hence thesis by Th14;
end;
Kv=subdivision(0,center_of_mass V,Kv) by SIMPLEX0:61;
then A4: P[0 qua Nat] by Th11;
for k holds P[k] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
end;
theorem Th16:
|.Kv.| c= [#]Kv implies BCS(0,Kv) = Kv
proof
assume|.Kv.|c=[#]Kv;
hence BCS(0,Kv)=subdivision(0,center_of_mass V,Kv) by Def6
.=Kv by SIMPLEX0:61;
end;
theorem Th17:
|.Kv.| c= [#]Kv implies BCS(1,Kv) = BCS Kv
proof
assume A1: |.Kv.|c=[#]Kv;
hence BCS(1,Kv)=subdivision(1,center_of_mass V,Kv) by Def6
.=subdivision(center_of_mass V,Kv) by SIMPLEX0:62
.=BCS Kv by A1,Def5;
end;
theorem Th18:
|.Kv.| c= [#]Kv implies [#]BCS(n,Kv) = [#]Kv
proof
assume|.Kv.|c=[#]Kv;
then BCS(n,Kv)=subdivision(n,center_of_mass V,Kv) by Def6;
hence thesis by SIMPLEX0:64;
end;
theorem
|.Kv.| c= [#]Kv implies |.BCS(n,Kv).| = |.Kv.| by Th10;
theorem Th20:
|.Kv.| c= [#]Kv implies BCS(n+1,Kv) = BCS BCS(n,Kv)
proof
A1: |.BCS(n,Kv).|=|.Kv.| by Th10;
assume A2: |.Kv.|c=[#]Kv;
then A3: [#]BCS(n,Kv)=[#]Kv by Th18;
n in NAT by ORDINAL1:def 13;
then subdivision(1+n,center_of_mass V,Kv)
=subdivision(1,center_of_mass V,subdivision(n,center_of_mass V,Kv))
by SIMPLEX0:63
.=subdivision(1,center_of_mass V,BCS(n,Kv)) by A2,Def6
.=BCS(1,BCS(n,Kv)) by A2,A3,A1,Def6
.=BCS BCS(n,Kv) by A2,A3,A1,Th17;
hence thesis by A2,Def6;
end;
theorem Th21:
|.Kv.| c= [#]Kv & degree Kv <= 0 implies the TopStruct of Kv = BCS Kv
proof
reconsider o=1 as ext-real number;
assume that
A1: |.Kv.|c=[#]Kv and
A2: degree Kv<=0;
set B=center_of_mass V,BC=BCS Kv;
A3: BC=subdivision(center_of_mass V,Kv) by A1,Def5;
then A4: [#]BC=[#]Kv by SIMPLEX0:def 20;
A5: dom B=(bool the carrier of V)\{{}} by FUNCT_2:def 1;
A6: 0+o=0+1 & degree Kv+o<=0+o by A2,XXREAL_3:36,def 2;
A7: the topology of BC c=the topology of Kv
proof
let x;
assume x in the topology of BC;
then reconsider X=x as Simplex of BC by PRE_TOPC:def 5;
reconsider X1=X as Subset of Kv by A4;
consider S be c=-linear finite simplex-like Subset-Family of Kv such that
A8: X=B.:S by A3,SIMPLEX0:def 20;
A9: B.:S=B.:(S/\dom B) by RELAT_1:145;
per cases;
suppose X is empty;
then X1 is simplex-like;
hence thesis by PRE_TOPC:def 5;
end;
suppose A10: X is non empty;
then S is non empty by A8,RELAT_1:149;
then union S in S by SIMPLEX0:9;
then reconsider U=union S as Simplex of Kv by TOPS_2:def 1;
A11: U is non empty
proof
assume A12: U is empty;
S/\dom B is empty
proof
assume S/\dom B is non empty;
then consider y such that
A13: y in S/\dom B by XBOOLE_0:def 1;
y in S by A13,XBOOLE_0:def 4;
then A14: y c=U by ZFMISC_1:92;
y<>{} by A13,ZFMISC_1:64;
hence contradiction by A12,A14;
end;
hence contradiction by A8,A9,A10,RELAT_1:149;
end;
then A15: @U in dom B by A5,ZFMISC_1:64;
card U<=degree Kv+1 by SIMPLEX0:24;
then A16: card U<=1 by A6,XXREAL_0:2;
card U>=1 by A11,NAT_1:14;
then A17: card U=1 by A16,XXREAL_0:1;
then consider u be set such that
A18: {u}=@U by CARD_2:60;
u in {u} by TARSKI:def 1;
then reconsider u as Element of V by A18;
A19: S/\dom B c={U}
proof
let y;
assume A20: y in S/\dom B;
then y in S by XBOOLE_0:def 4;
then A21: y c=U by ZFMISC_1:92;
y<>{} by A20,ZFMISC_1:64;
then y=U by A18,A21,ZFMISC_1:39;
hence thesis by TARSKI:def 1;
end;
S/\dom B is non empty by A8,A9,A10,RELAT_1:149;
then S/\dom B={U} by A19,ZFMISC_1:39;
then X=Im(B,U) by A8,A9,RELAT_1:def 16
.={B.U} by A15,FUNCT_1:117
.={1/1*Sum{u}} by A17,A18,RLAFFIN2:def 2
.={Sum{u}} by RLVECT_1:def 11
.=U by A18,RLVECT_2:15;
hence thesis by PRE_TOPC:def 5;
end;
end;
the topology of Kv c=the topology of BC
proof
let x;
assume x in the topology of Kv;
then reconsider X=x as Simplex of Kv by PRE_TOPC:def 5;
reconsider X1=X as Subset of BC by A4;
per cases;
suppose X is empty;
then X1 is simplex-like;
hence thesis by PRE_TOPC:def 5;
end;
suppose A22: X is non empty;
for Y be Subset of Kv st Y in {X} holds Y is simplex-like by TARSKI:def 1;
then reconsider XX={X} as finite simplex-like Subset-Family of Kv by TOPS_2
:def 1;
now let x,y;
assume that
A23: x in XX and
A24: y in XX;
x=X by A23,TARSKI:def 1;
hence x,y are_c=-comparable by A24,TARSKI:def 1;
end;
then A25: XX is c=-linear by ORDINAL1:def 9;
card X<=degree Kv+1 by SIMPLEX0:24;
then A26: card X<=1 by A6,XXREAL_0:2;
card X>=1 by A22,NAT_1:14;
then A27: card X=1 by A26,XXREAL_0:1;
then consider u be set such that
A28: @X={u} by CARD_2:60;
A29: @X in dom B by A5,A22,ZFMISC_1:64;
u in {u} by TARSKI:def 1;
then reconsider u as Element of V by A28;
B.:XX=Im(B,X) by RELAT_1:def 16
.={B.X} by A29,FUNCT_1:117
.={1/1*Sum{u}} by A27,A28,RLAFFIN2:def 2
.={Sum{u}} by RLVECT_1:def 11
.=X1 by A28,RLVECT_2:15;
then X1 is simplex-like by A3,A25,SIMPLEX0:def 20;
hence thesis by PRE_TOPC:def 5;
end;
end;
hence thesis by A3,A4,A7,XBOOLE_0:def 10;
end;
theorem Th22:
n > 0 & |.Kv.| c= [#]Kv & degree Kv <= 0 implies
the TopStruct of Kv = BCS(n,Kv)
proof
assume that
A1: n>0 and
A2: |.Kv.|c=[#]Kv and
A3: degree Kv<=0;
defpred P[Nat] means
$1>0 implies the TopStruct of Kv=BCS($1,Kv) & degree BCS($1,Kv)<=0;
A4: for n st P[n] holds P[n+1]
proof
not{} in dom(center_of_mass V) by ZFMISC_1:64;
then A5: dom center_of_mass V is with_non-empty_elements by SETFAM_1:def 9;
let n such that
A6: P[n];
assume n+1>0;
per cases;
suppose A7: n=0;
A8: degree subdivision(center_of_mass V,Kv)<=degree Kv by A5,SIMPLEX0:52;
BCS(n+1,Kv)=BCS Kv by A2,A7,Th17;
hence thesis by A2,A3,A8,Def5,Th21;
end;
suppose A9: n>0;
A10: |.Kv.|=|.BCS(n,Kv).| by Th10;
[#]Kv=[#]BCS(n,Kv) by A6,A9;
then BCS(n,Kv)=BCS BCS(n,Kv) by A2,A6,A9,A10,Th21;
hence thesis by A2,A6,A9,Th20;
end;
end;
A11: P[0 qua Nat];
for n holds P[n] from NAT_1:sch 2(A11,A4);
hence thesis by A1;
end;
theorem Th23:
for Sv be non void SubSimplicialComplex of Kv st
|.Kv.| c= [#]Kv & |.Sv.| c= [#]Sv
holds BCS(n,Sv) is SubSimplicialComplex of BCS(n,Kv)
proof
let S be non void SubSimplicialComplex of Kv;
assume|.Kv.|c=[#]Kv & |.S.|c=[#]S;
then BCS(n,S)=subdivision(n,center_of_mass V,S) &
BCS(n,Kv)=subdivision(n,center_of_mass V,Kv)
by Def6;
hence thesis by SIMPLEX0:65;
end;
Lm1: card n=n
proof
card n=card card n;
hence thesis by CARD_1:71;
end;
theorem Th24:
|.Kv.| c= [#]Kv implies Vertices Kv c= Vertices BCS(n,Kv)
proof
set S=Skeleton_of(Kv,0);
assume A1: |.Kv.|c=[#]Kv;
per cases;
suppose n=0;
hence thesis by A1,Th16;
end;
suppose A2: n>0;
the topology of S c=the topology of Kv by SIMPLEX0:def 13;
then |.S.|c=|.Kv.| by Th4;
then A3: |.S.|c=[#]S by A1,XBOOLE_1:1;
then degree S<=0 & BCS(n,S) is SubSimplicialComplex of BCS(n,Kv) by A1,
Th23,SIMPLEX0:44;
then S is SubSimplicialComplex of BCS(n,Kv) by A2,A3,Th22;
then A4: Vertices S c=Vertices BCS(n,Kv) by SIMPLEX0:31;
let x;
assume A5: x in Vertices Kv;
then reconsider v=x as Element of Kv;
v is vertex-like by A5,SIMPLEX0:def 4;
then consider A be Subset of Kv such that
A6: A is simplex-like and
A7: v in A by SIMPLEX0:def 3;
reconsider vv={v} as Subset of Kv by A7,ZFMISC_1:37;
{v}c=A by A7,ZFMISC_1:37;
then vv is simplex-like by A6,MATROID0:1;
then A8: vv in the topology of Kv by PRE_TOPC:def 5;
card vv=1 & card 1=1 by Lm1,CARD_1:50;
then vv in the_subsets_with_limited_card(1,the topology of Kv) by A8,
SIMPLEX0:def 2;
then vv in the topology of S by SIMPLEX0:2;
then reconsider vv as Simplex of S by PRE_TOPC:def 5;
A9: v in vv by TARSKI:def 1;
reconsider v as Element of S;
v is vertex-like by A9,SIMPLEX0:def 3;
then v in Vertices S by SIMPLEX0:def 4;
hence thesis by A4;
end;
end;
registration
let n,V;
let K be non void total SimplicialComplex of V;
cluster BCS(n,K) -> total;
coherence
proof
A1: [#]K=[#]V by SIMPLEX0:def 10;
then |.K.|c=[#]K;
then [#]BCS(n,K)=[#]V by A1,Th18;
hence thesis by SIMPLEX0:def 10;
end;
end;
registration
let n,V;
let K be non void finite-vertices total SimplicialComplex of V;
cluster BCS(n,K) -> finite-vertices;
coherence
proof
defpred P[Nat] means
BCS($1,K) is finite-vertices;
[#]K=[#]V by SIMPLEX0:def 10;
then A1: |.K.|c=[#]K;
A2: for n st P[n] holds P[n+1]
proof
let n such that
A3: P[n];
[#]BCS(n,K)=[#]V by SIMPLEX0:def 10;
then A4: |.BCS(n,K).|c=[#]BCS(n,K);
BCS(n+1,K)=BCS BCS(n,K) by A1,Th20
.=subdivision(center_of_mass V,BCS(n,K)) by A4,Def5;
hence thesis by A3;
end;
A5: P[0 qua Nat] by A1,Th16;
for n holds P[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
end;
begin :: Selected Properties of Simplicial Complexes
definition
let V;
let K be SimplicialComplexStr of V;
attr K is affinely-independent means :Def7:
for A be Subset of K st A is simplex-like holds @A is affinely-independent;
end;
definition
let RLS,Kr;
attr Kr is simplex-join-closed means :Def8:
for A,B be Subset of Kr st A is simplex-like & B is simplex-like
holds conv @A /\ conv @B = conv @(A/\B);
end;
registration
let V;
cluster empty-membered -> affinely-independent SimplicialComplexStr of V;
coherence
proof
let K be SimplicialComplexStr of V;
assume K is empty-membered;
then A1: the topology of K is empty-membered by SIMPLEX0:def 7;
let A be Subset of K;
assume A is simplex-like;
then A in the topology of K by PRE_TOPC:def 5;
then A is empty by A1,SETFAM_1:def 11;
hence thesis;
end;
let F be affinely-independent Subset-Family of V;
cluster Complex_of F -> affinely-independent;
coherence
proof
let A be Subset of Complex_of F;
assume A is simplex-like;
then A in subset-closed_closure_of F by PRE_TOPC:def 5;
then consider x such that
A2: A c=x and
A3: x in F by SIMPLEX0:2;
x is affinely-independent Subset of V by A3,RLAFFIN1:def 5;
hence thesis by A2,RLAFFIN1:43;
end;
end;
registration
let RLS;
cluster empty-membered -> simplex-join-closed SimplicialComplexStr of RLS;
coherence
proof
let K be SimplicialComplexStr of RLS;
assume K is empty-membered;
then A1: the topology of K is empty-membered by SIMPLEX0:def 7;
let A,B be Subset of K;
assume that
A2: A is simplex-like and
A3: B is simplex-like;
A in the topology of K by A2,PRE_TOPC:def 5;
then A4: A is empty by A1,SETFAM_1:def 11;
B in the topology of K by A3,PRE_TOPC:def 5;
then B is empty by A1,SETFAM_1:def 11;
hence thesis by A4;
end;
end;
registration
let V;
let I be affinely-independent Subset of V;
cluster Complex_of{I} -> simplex-join-closed;
coherence
proof
set C=Complex_of{I};
let A,B be Subset of C;
assume that
A1: A is simplex-like and
A2: B is simplex-like;
A3: the topology of C=bool I by SIMPLEX0:4;
A4: B in the topology of C by A2,PRE_TOPC:def 5;
A5: A/\B c=A by XBOOLE_1:17;
A6: @A is affinely-independent by A1,Def7;
A7: conv@B c=Affin@B by RLAFFIN1:65;
A8: conv@A c=Affin@A by RLAFFIN1:65;
A9: A in the topology of C by A1,PRE_TOPC:def 5;
then A10: Affin@A c=Affin I by A3,RLAFFIN1:52;
A11: @(A/\B) is affinely-independent by A1,Def7;
thus conv@A/\conv@B c=conv@(A/\B)
proof
let x;
set IAB=I\@(A/\B);
A12: @(A/\B)=I/\@(A/\B) by A3,A5,A9,XBOOLE_1:1,28
.=I\IAB by XBOOLE_1:48;
assume A13: x in conv@A/\conv@B;
then A14: x in conv@A by XBOOLE_0:def 4;
then A15: x|--@A=x|--I by A3,A8,A9,RLAFFIN1:77;
x in conv@B by A13,XBOOLE_0:def 4;
then A16: x|--@B=x|--I by A3,A4,A7,RLAFFIN1:77;
A17: Carrier(x|--@A)c=A & Carrier(x|--@B)c=B by RLVECT_2:def 8;
A18: for y st y in IAB holds(x|--I).y=0
proof
let y;
assume A19: y in IAB;
then not y in A/\B by XBOOLE_0:def 5;
then not y in Carrier(x|--@A) or not y in Carrier(x|--@B) by A17,XBOOLE_0:
def 4;
hence thesis by A15,A16,A19;
end;
A20: x in Affin@A by A8,A14;
A21: now let v be Element of V;
assume v in @(A/\B);
0<=(x|--@A).v by A6,A14,RLAFFIN1:71;
hence 0<=(x|--@(A/\B)).v by A10,A12,A15,A18,A20,RLAFFIN1:75;
end;
x in Affin@(A/\B) by A10,A12,A18,A20,RLAFFIN1:75;
hence x in conv@(A/\B) by A11,A21,RLAFFIN1:73;
end;
conv@(A/\B)c=conv@A & conv@(A/\B)c=conv@B by RLTOPSP1:21,XBOOLE_1:17;
hence thesis by XBOOLE_1:19;
end;
end;
registration let V;
cluster non empty trivial affinely-independent Subset of V;
existence
proof
take {the Element of V};
thus thesis;
end;
end;
registration
let V;
cluster with_non-empty_element finite-vertices affinely-independent
simplex-join-closed total SimplicialComplex of V;
existence
proof
set v=the Element of V;
take Complex_of{{v}};
thus thesis by SIMPLEX0:def 7;
end;
end;
registration
let V;
let K be affinely-independent SimplicialComplexStr of V;
cluster -> affinely-independent SubSimplicialComplex of K;
coherence
proof
let S be SubSimplicialComplex of K;
let A be Subset of S;
assume A is simplex-like;
then A1: A in the topology of S by PRE_TOPC:def 5;
A2: the topology of S c=the topology of K by SIMPLEX0:def 13;
then A in the topology of K by A1;
then reconsider A1=A as Subset of K;
A1 is simplex-like by A1,A2,PRE_TOPC:def 5;
then @A1 is affinely-independent by Def7;
hence thesis;
end;
end;
registration
let V;
let K be simplex-join-closed SimplicialComplexStr of V;
cluster -> simplex-join-closed SubSimplicialComplex of K;
coherence
proof
let S be SubSimplicialComplex of K;
A1: the topology of S c=the topology of K by SIMPLEX0:def 13;
let A,B be Subset of S;
assume that
A2: A is simplex-like and
A3: B is simplex-like;
A4: A in the topology of S by A2,PRE_TOPC:def 5;
then A5: A in the topology of K by A1;
A6: B in the topology of S by A3,PRE_TOPC:def 5;
then B in the topology of K by A1;
then reconsider A1=A,B1=B as Subset of K by A5;
A7: A1 is simplex-like by A1,A4,PRE_TOPC:def 5;
B1 is simplex-like by A1,A6,PRE_TOPC:def 5;
then conv@A1/\conv@B1=conv@(A1/\B1) by A7,Def8;
hence thesis;
end;
end;
theorem Th25:
for K be subset-closed SimplicialComplexStr of V holds
K is simplex-join-closed
iff
for A,B be Subset of K st A is simplex-like & B is simplex-like &
Int @A meets Int @B
holds A=B
proof
let K be subset-closed SimplicialComplexStr of V;
hereby assume A1: K is simplex-join-closed;
let A,B be Subset of K such that
A2: A is simplex-like & B is simplex-like and
A3: Int@A meets Int@B;
A4: conv@A/\conv@B=conv@(A/\B) by A1,A2,Def8;
assume A<>B;
then A5: A/\B<>A or A/\B<>B;
A6: A/\B c=A & A/\B c=B by XBOOLE_1:17;
consider x such that
A7: x in Int@A and
A8: x in Int@B by A3,XBOOLE_0:3;
Int@A c=conv@A & Int@B c=conv@B by RLAFFIN2:5;
then A9: x in conv@A/\conv@B by A7,A8,XBOOLE_0:def 4;
per cases by A5,A6,XBOOLE_0:def 8;
suppose A/\B c affinely-independent;
coherence by Def7;
end;
theorem Th26:
As is simplex-like & Bs is simplex-like & Int@As meets conv@Bs
implies As c= Bs
proof
assume that
A1: As is simplex-like and
A2: Bs is simplex-like and
A3: Int@As meets conv@Bs;
consider x such that
A4: x in Int@As and
A5: x in conv@Bs by A3,XBOOLE_0:3;
x in union{Int b where b is Subset of V:b c=@Bs} by A5,RLAFFIN2:8;
then consider Ib be set such that
A6: x in Ib and
A7: Ib in {Int b where b is Subset of V:b c=@Bs} by TARSKI:def 4;
consider b be Subset of V such that
A8: Ib=Int b and
A9: b c=@Bs by A7;
reconsider b1=b as Subset of Ks by A9,XBOOLE_1:1;
As in the topology of Ks by A1,PRE_TOPC:def 5;
then Ks is non void by PENCIL_1:def 4;
then A10: b1 is simplex-like by A2,A9,MATROID0:1;
Int@As meets Int@b1 by A4,A6,A8,XBOOLE_0:3;
hence thesis by A1,A9,A10,Th25;
end;
theorem
As is simplex-like & @As is affinely-independent & Bs is simplex-like
implies (Int@As c= conv @Bs iff As c= Bs)
proof
assume that
A1: As is simplex-like and
A2: @As is affinely-independent and
A3: Bs is simplex-like;
As in the topology of Ks by A1,PRE_TOPC:def 5;
then A4: Ks is non void by PENCIL_1:def 4;
per cases;
suppose A5: As is empty;
then Int@As is empty;
hence thesis by A5,XBOOLE_1:2;
end;
suppose As is non empty;
then Int@As is non empty by A1,A2,A4,RLAFFIN2:20;
then consider x such that
A6: x in Int@As by XBOOLE_0:def 1;
hereby assume Int@As c=conv@Bs;
then x in conv@Bs by A6;
then x in union{Int b where b is Subset of V:b c=@Bs} by RLAFFIN2:8;
then consider Ib be set such that
A7: x in Ib and
A8: Ib in {Int b where b is Subset of V:b c=@Bs} by TARSKI:def 4;
consider b be Subset of V such that
A9: Ib=Int b and
A10: b c=@Bs by A8;
reconsider b1=b as Subset of Ks by A10,XBOOLE_1:1;
A11: b1 is simplex-like by A3,A4,A10,MATROID0:1;
Int@As meets Int@b1 by A6,A7,A9,XBOOLE_0:3;
hence As c=Bs by A1,A10,A11,Th25;
end;
assume As c=Bs;
then Int@As c=conv@As & conv@As c=conv@Bs by RLAFFIN1:3,RLAFFIN2:5;
hence thesis by XBOOLE_1:1;
end;
end;
theorem Th28:
|.Ka.| c= [#]Ka implies BCS Ka is affinely-independent
proof
set P=BCS Ka,B=center_of_mass V;
assume|.Ka.|c=[#]Ka;
then A1: P=subdivision(B,Ka) by Def5;
let A be Subset of P;
assume A is simplex-like;
then consider S be c=-linear finite simplex-like Subset-Family of Ka such
that
A2: A=B.:S by A1,SIMPLEX0:def 20;
per cases;
suppose S is empty;
then A={} by A2,RELAT_1:149;
hence thesis;
end;
suppose A3: S is non empty;
S c=bool union S & bool@union S c=bool the carrier of V by ZFMISC_1:79,100;
then reconsider s=S as c=-linear finite Subset-Family of V by XBOOLE_1:1;
union S in S by A3,SIMPLEX0:9;
then union S is simplex-like by TOPS_2:def 1;
then @union S is affinely-independent;
then union s is affinely-independent;
hence thesis by A2,RLAFFIN2:29;
end;
end;
registration
let V;
let Ka be non void affinely-independent total SimplicialComplex of V;
cluster BCS Ka -> affinely-independent;
coherence
proof
[#]Ka=the carrier of V by SIMPLEX0:def 10;
then |.Ka.|c=[#]Ka;
hence thesis by Th28;
end;
let n;
cluster BCS(n,Ka) -> affinely-independent;
coherence
proof
defpred P[Nat] means
BCS($1,Ka) is affinely-independent;
[#]Ka=[#]V by SIMPLEX0:def 10;
then A1: |.Ka.|c=[#]Ka;
A2: for n st P[n] holds P[n+1]
proof
let n such that
A3: P[n];
BCS(n+1,Ka)=BCS BCS(n,Ka) by A1,Th20;
hence thesis by A3;
end;
A4: P[0 qua Nat] by A1,Th16;
for n holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
end;
registration
let V,Kas;
cluster (center_of_mass V)|the topology of Kas -> one-to-one;
coherence
proof
now set B=center_of_mass V,T=the topology of Kas;
let x1,x2 be set;
set BT=B|T;
assume that
A1: x1 in dom BT and
A2: x2 in dom BT and
A3: BT.x1=BT.x2;
A4: BT.x1=B.x1 & BT.x2=B.x2 by A1,A2,FUNCT_1:70;
dom BT=dom B/\T by RELAT_1:90;
then x1 in T & x2 in T by A1,A2,XBOOLE_0:def 4;
then reconsider A1=x1,A2=x2 as Simplex of Kas by PRE_TOPC:def 5;
A1 is non empty by A1,ZFMISC_1:64;
then A5: B.A1 in conv@A1 by RLAFFIN2:16;
A2 is non empty by A2,ZFMISC_1:64;
then B.A2 in conv@A2 by RLAFFIN2:16;
then A6: B.A1 in conv@A1/\conv@A2 by A3,A4,A5,XBOOLE_0:def 4;
A7: conv@A1/\conv@A2=conv@(A1/\A2) & conv@(A1/\A2)c=Affin@(A1/\A2) by Def8,
RLAFFIN1:65;
then A1/\A2=A1 by A6,RLAFFIN2:21,XBOOLE_1:17;
hence x1=x2 by A3,A4,A6,A7,RLAFFIN2:21,XBOOLE_1:17;
end;
hence thesis by FUNCT_1:def 8;
end;
end;
theorem Th29:
|.Kas.| c= [#]Kas implies BCS Kas is simplex-join-closed
proof
set B=center_of_mass V;
set BC=BCS Kas;
defpred P[Nat] means
for S1,S2 be c=-linear finite simplex-like Subset-Family of Kas for A1,A2 be
Simplex of BC st A1=B.:S1 & A2=B.:S2 & card union S1<=$1 & card union S2<=$1 &
Int@A1 meets Int@A2 holds A1=A2;
assume A1: |.Kas.|c=[#]Kas;
then A2: BC=subdivision(B,Kas) by Def5;
A3: BC is affinely-independent by A1,Th28;
A4: dom B=(bool the carrier of V)\{{}} by FUNCT_2:def 1;
A5: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A6: P[n];
let S1,S2 be c=-linear finite simplex-like Subset-Family of Kas;
let A1,A2 be Simplex of BC such that
A7: A1=B.:S1 and
A8: A2=B.:S2 and
A9: card union S1<=n+1 and
card union S2<=n+1 and
A10: Int@A1 meets Int@A2;
A11: union S2 in S2 or S2 is empty by SIMPLEX0:9;
then A12: union S2 is simplex-like by TOPS_2:def 1,ZFMISC_1:2;
set U=union S1;
S2 c=bool union S2 & bool@union S2 c=bool the carrier of V by ZFMISC_1:79,
100;
then A13: S2 is Subset-Family of V by XBOOLE_1:1;
A14: union S1 in S1 or S1 is empty by SIMPLEX0:9;
then A15: union S1 is simplex-like by TOPS_2:def 1,ZFMISC_1:2;
S1 c=bool union S1 & bool@union S1 c=bool the carrier of V by ZFMISC_1:79,
100;
then A16: S1 is Subset-Family of V by XBOOLE_1:1;
then A17: Int(B.:S1)c=Int@union S1 by A15,RLAFFIN2:30;
Int@union S1 meets Int(B.:S2) by A7,A8,A10,A15,A16,RLAFFIN2:30,XBOOLE_1:63;
then Int@union S1 meets Int@union S2 by A13,A12,RLAFFIN2:30,XBOOLE_1:63;
then A18: union S1=union S2 by A12,A15,Th25;
per cases by A9,NAT_1:8;
suppose card union S1<=n;
hence thesis by A6,A7,A8,A10,A18;
end;
suppose A19: card union S1=n+1;
then A20: @union S1 is non empty;
then A21: union S1 in dom B by A4,ZFMISC_1:64;
then A22: B.union S1 in @A1 by A7,A14,A19,FUNCT_1:def 12,ZFMISC_1:2;
then reconsider Bu=B.union S1 as Element of V;
A23: {Bu}c=@A1 by A22,ZFMISC_1:37;
A24: B.union S1 in @A2 by A8,A11,A18,A19,A21,FUNCT_1:def 12,ZFMISC_1:2;
then A25: {Bu}c=@A2 by ZFMISC_1:37;
A26: Bu in {Bu} by ZFMISC_1:37;
A27: conv{Bu}={Bu} by RLAFFIN1:1;
consider x such that
A28: x in Int@A1 and
A29: x in Int@A2 by A10,XBOOLE_0:3;
reconsider x as Element of V by A28;
per cases;
suppose A1={Bu} & A2={Bu};
hence thesis;
end;
suppose A30: A1={Bu} & A2<>{Bu};
then {Bu}c<@A2 & Int@A1=@A1 by A25,RLAFFIN2:6,XBOOLE_0:def 8;
hence thesis by A27,A28,A29,A30,RLAFFIN2:def 1;
end;
suppose A31: A1<>{Bu} & A2={Bu};
then {Bu}c<@A1 & Int@A2=@A2 by A23,RLAFFIN2:6,XBOOLE_0:def 8;
hence thesis by A27,A28,A29,A31,RLAFFIN2:def 1;
end;
suppose A1<>{Bu} & A2<>{Bu};
then {Bu}c<@A1 by A23,XBOOLE_0:def 8;
then A32: Bu<>x by A26,A27,A28,RLAFFIN2:def 1;
S1\{U}c=S1 & S2\{U}c=S2 by XBOOLE_1:36;
then reconsider s1u=S1\{U},s2u=S2\{U} as c=-linear finite simplex-like
Subset-Family of Kas by TOPS_2:18;
A33: S1 c=the topology of Kas
proof
let x;
assume A34: x in S1;
then reconsider A=x as Subset of Kas;
A is simplex-like by A34,TOPS_2:def 1;
hence thesis by PRE_TOPC:def 5;
end;
[#]Kas c=the carrier of V by SIMPLEX0:def 9;
then bool the carrier of Kas c=bool the carrier of V by ZFMISC_1:79;
then reconsider S1U=s1u,S2U=s2u as Subset-Family of V by XBOOLE_1:1;
set Bu1=x|--@A1;
set Bu2=x|--@A2;
set BT=B|(the topology of Kas);
A35: S1\{U}c=S1 by XBOOLE_1:36;
A36: {U}c=S1 by A14,A19,ZFMISC_1:2,37;
A37: union s2u c=U by A18,XBOOLE_1:36,ZFMISC_1:95;
union s2u<>U
proof
assume A38: union s2u=U;
then union s2u in s2u by A20,SIMPLEX0:9,ZFMISC_1:2;
hence contradiction by A38,ZFMISC_1:64;
end;
then A39: union s2u c__=1;
then Bu1.Bu=1 by A44,XXREAL_0:1;
hence contradiction by A3,A32,A43,RLAFFIN1:72;
end;
conv@A1 c=Affin@A1 by RLAFFIN1:65;
then A46: x=Sum Bu1 by A3,A43,RLAFFIN1:def 7;
then Bu in Carrier Bu1 by A3,A22,A28,A43,RLAFFIN1:71,RLAFFIN2:11;
then A47: Bu1.Bu<>0 by RLVECT_2:28;
Bu1 is convex by A3,A43,RLAFFIN1:71;
then consider p1 be Element of V such that
A48: p1 in conv(@A1\{Bu}) and
A49: x=Bu1.Bu*Bu+(1-Bu1.Bu)*p1 and
1/Bu1.Bu*x+(1-1/Bu1.Bu)*p1=Bu by A32,A46,A47,RLAFFIN2:1;
A50: p1 in Int(@A1\{Bu}) by A3,A22,A28,A48,A49,RLAFFIN2:14;
A51: {Bu}=Im(B,union S1) by A21,FUNCT_1:117
.=B.:{union S1} by RELAT_1:def 16;
then A52: A1\{Bu}=BT.:S1\(B.:{U}) by A33,RELAT_1:162,A7
.=BT.:S1\(BT.:{U}) by A33,A36,RELAT_1:162,XBOOLE_1:1
.=BT.:(S1\{U}) by FUNCT_1:123
.=B.:(S1\{U}) by A35,A33,RELAT_1:162,XBOOLE_1:1;
then conv(@A1\{Bu})c=conv union S1U by CONVEX1:30,RLAFFIN2:17;
then A53: p1 in conv union S1U by A48;
card union s2u=1;
then Bu2.Bu=1 by A57,XXREAL_0:1;
hence contradiction by A3,A32,A56,RLAFFIN1:72;
end;
conv@A2 c=Affin@A2 by RLAFFIN1:65;
then A59: x=Sum Bu2 by A3,A56,RLAFFIN1:def 7;
then Bu in Carrier Bu2 by A3,A24,A29,A56,RLAFFIN1:71,RLAFFIN2:11;
then A60: Bu2.Bu<>0 by RLVECT_2:28;
Bu2 is convex by A3,A56,RLAFFIN1:71;
then consider p2 be Element of V such that
A61: p2 in conv(@A2\{Bu}) and
A62: x=Bu2.Bu*Bu+(1-Bu2.Bu)*p2 and
1/Bu2.Bu*x+(1-1/Bu2.Bu)*p2=Bu by A32,A59,A60,RLAFFIN2:1;
A63: p2 in Int(@A2\{Bu}) by A3,A24,A29,A61,A62,RLAFFIN2:14;
@U is non empty finite Subset of V by A19;
then A64: Bu in Int@U by A15,RLAFFIN2:20;
then A65: Bu in conv@U by RLAFFIN2:def 1;
A66: S2 c=the topology of Kas
proof
let x;
assume A67: x in S2;
then reconsider A=x as Subset of Kas;
A is simplex-like by A67,TOPS_2:def 1;
hence thesis by PRE_TOPC:def 5;
end;
union s1u<>U
proof
assume A68: union s1u=U;
then union s1u in s1u by A20,SIMPLEX0:9,ZFMISC_1:2;
hence contradiction by A68,ZFMISC_1:64;
end;
then A69: union s1u c____U by A70,XBOOLE_1:36,ZFMISC_1:64;
then U\{xS1U}c____U by A40,XBOOLE_1:36,ZFMISC_1:64;
then U\{xS2U}c____{} by A86,ZFMISC_1:64;
union S1 is empty by A83;
then x c={} by A87,ZFMISC_1:92;
hence thesis by A88;
end;
A89: for n holds P[n] from NAT_1:sch 2(A81,A5);
now let A1,A2 be Subset of BC;
assume that
A90: A1 is simplex-like and
A91: A2 is simplex-like and
A92: Int@A1 meets Int@A2;
consider S1 be c=-linear finite simplex-like Subset-Family of Kas such that
A93: A1=B.:S1 by A2,A90,SIMPLEX0:def 20;
consider S2 be c=-linear finite simplex-like Subset-Family of Kas such that
A94: A2=B.:S2 by A2,A91,SIMPLEX0:def 20;
card union S1<=card union S2 or card union S2<=card union S1;
hence A1=A2 by A89,A90,A91,A92,A93,A94;
end;
hence thesis by Th25;
end;
registration
let V,K;
cluster BCS K -> simplex-join-closed;
coherence
proof
[#]K=the carrier of V by SIMPLEX0:def 10;
then |.K.|c=[#]K;
hence thesis by Th29;
end;
let n;
cluster BCS(n,K) -> simplex-join-closed;
coherence
proof
defpred P[Nat] means
BCS($1,K) is simplex-join-closed affinely-independent;
[#]K=[#]V by SIMPLEX0:def 10;
then A1: |.K.|c=[#]K;
A2: for n st P[n] holds P[n+1]
proof
let n such that
A3: P[n];
BCS(n+1,K)=BCS BCS(n,K) by A1,Th20;
hence thesis by A3;
end;
A4: P[0 qua Nat] by A1,Th16;
for n holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
end;
theorem Th30:
|.Kv.| c= [#]Kv & (for n st n <= degree Kv ex S be Simplex of Kv st
card S = n+1 & @S is affinely-independent)
implies degree Kv = degree BCS Kv
proof
assume that
A1: |.Kv.|c=[#]Kv and
A2: for n st n<=degree Kv ex S be Simplex of Kv st card S=n+1 & @S is
affinely-independent;
A3: dom center_of_mass V=(bool the carrier of V)\{{}} by FUNCT_2:def 1;
A4: for n st n<=degree Kv ex S be Subset of Kv st S is simplex-like & card S=
n+1 & BOOL S c=dom center_of_mass V & (center_of_mass V).:BOOL S
is Subset of Kv & (center_of_mass V)|BOOL S is one-to-one
proof
let n;
assume n<=degree Kv;
then consider S be Simplex of Kv such that
A5: card S=n+1 and
A6: @S is affinely-independent by A2;
take S;
thus S is simplex-like & card S=n+1 by A5;
A7: the topology of Complex_of{@S}=bool S by SIMPLEX0:4;
reconsider SS={@S} as affinely-independent Subset-Family of V by A6;
A8: (center_of_mass V).:BOOL S c=conv@S
proof
let y;
assume y in (center_of_mass V).:BOOL S;
then consider x such that
A9: x in dom(center_of_mass V) and
A10: x in BOOL S & (center_of_mass V).x=y by FUNCT_1:def 12;
reconsider x as non empty Subset of V by A9,ZFMISC_1:64;
conv x c=conv@S & y in conv x by A10,RLAFFIN2:16,RLTOPSP1:21;
hence thesis;
end;
bool@S c=(bool the carrier of V) by ZFMISC_1:79;
hence BOOL S c=dom center_of_mass V by A3,XBOOLE_1:33;
conv@S c=|.Kv.| by Th5;
then conv@S c=[#]Kv by A1,XBOOLE_1:1;
hence (center_of_mass V).:BOOL S is Subset of Kv by A8,XBOOLE_1:1;
(center_of_mass V)|bool S|BOOL S=(center_of_mass V)|BOOL S &
Complex_of SS is SimplicialComplex of V by RELAT_1:103;
hence thesis by A6,A7,FUNCT_1:84;
end;
not{} in dom center_of_mass V by ZFMISC_1:64;
then A11: dom center_of_mass V is with_non-empty_elements by SETFAM_1:def 9;
BCS Kv=subdivision(center_of_mass V,Kv) by A1,Def5;
hence thesis by A4,A11,SIMPLEX0:53;
end;
theorem Th31:
|.Ka.| c= [#]Ka implies degree Ka = degree BCS Ka
proof
A1: for n st n<=degree Ka ex S be Simplex of Ka st card S=n+1 & @S is
affinely-independent
proof
let n;
reconsider N=n as ext-real number;
set S=the Simplex of n,Ka;
assume n<=degree Ka;
then A2: card S=N+1 by SIMPLEX0:def 18;
N+1=n+1 & @S is affinely-independent by XXREAL_3:def 2;
hence thesis by A2;
end;
assume|.Ka.|c=[#]Ka;
hence thesis by A1,Th30;
end;
theorem Th32:
|.Ka.| c= [#]Ka implies degree Ka = degree BCS(n,Ka)
proof
defpred P[Nat] means
degree Ka=degree BCS($1,Ka) & BCS($1,Ka) is non void affinely-independent;
assume A1: |.Ka.|c=[#]Ka;
A2: for n st P[n] holds P[n+1]
proof
let n such that
A3: P[n];
A4: [#]BCS(n,Ka)=[#]Ka by A1,Th18;
BCS(n+1,Ka)=BCS BCS(n,Ka) & |.BCS(n,Ka).|=|.Ka.| by A1,Th10,Th20;
hence thesis by A1,A3,A4,Th28,Th31;
end;
A5: P[0 qua Nat] by A1,Th16;
for n holds P[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem Th33:
for S be simplex-like Subset-Family of Kas st S is with_non-empty_elements
holds card S = card ((center_of_mass V).:S)
proof
set B=center_of_mass V;
set T=the topology of Kas;
let S be simplex-like Subset-Family of Kas such that
A1: S is with_non-empty_elements;
A2: not{} in S by A1;
[#]Kas c=the carrier of V by SIMPLEX0:def 9;
then bool the carrier of Kas c=bool the carrier of V by ZFMISC_1:79;
then dom B=(bool the carrier of V)\{{}} & S c=bool the carrier of V by
FUNCT_2:def 1,XBOOLE_1:1;
then A3: dom(B|S)=S by A2,RELAT_1:91,ZFMISC_1:40;
S c=T
proof
let x;
assume x in S;
then x is Simplex of Kas by TOPS_2:def 1;
hence thesis by PRE_TOPC:def 5;
end;
then B|T|S=B|S by RELAT_1:103;
then A4: B|S is one-to-one by FUNCT_1:84;
B.:S=rng(B|S) by RELAT_1:148;
then S,B.:S are_equipotent by A3,A4,WELLORD2:def 4;
hence thesis by CARD_1:21;
end;
reserve Aff for finite affinely-independent Subset of V,
Af,Bf for finite Subset of V,
B for Subset of V,
S,T for finite Subset-Family of V,
Sf for c=-linear finite finite-membered Subset-Family of V,
Sk,Tk for finite simplex-like Subset-Family of K,
Ak for Simplex of K;
theorem Th34:
for S1,S2 be simplex-like Subset-Family of Kas st
|.Kas.|c=[#]Kas & S1 is with_non-empty_elements &
(center_of_mass V).:S2 is Simplex of BCS Kas &
(center_of_mass V).:S1 c= (center_of_mass V).:S2
holds S1 c= S2 & S2 is c=-linear
proof
set B=center_of_mass V;
set BK=BCS Kas;
let S1,S2 be simplex-like Subset-Family of Kas;
assume that
A1: |.Kas.|c=[#]Kas and
A2: S1 is with_non-empty_elements and
A3: B.:S2 is Simplex of BCS Kas and
A4: B.:S1 c=B.:S2;
BK=subdivision(B,Kas) by A1,Def5;
then consider W2 be c=-linear finite simplex-like Subset-Family of Kas such
that
A5: B.:S2=B.:W2 by A3,SIMPLEX0:def 20;
reconsider s2=S2\{{}} as simplex-like Subset-Family of Kas by TOPS_2:18,
XBOOLE_1:36;
set TK=the topology of Kas;
set BTK=B|TK;
A6: dom BTK=dom B/\TK by RELAT_1:90;
A7: s2 c=TK by SIMPLEX0:14;
A8: dom B=(bool the carrier of V)\{{}} by FUNCT_2:def 1;
then @S2\{{}}c=dom B by XBOOLE_1:33;
then s2 c=dom B/\TK by A7,XBOOLE_1:19;
then A9: s2 c=dom BTK by RELAT_1:90;
W2/\dom B c=W2 by XBOOLE_1:17;
then reconsider w2=W2/\dom B as c=-linear finite simplex-like Subset-Family
of Kas by TOPS_2:18,XBOOLE_1:1;
A10: w2 c=TK by SIMPLEX0:14;
then A11: B.:W2=B.:(W2/\dom B) & B.:w2=BTK.:w2 by RELAT_1:145,162;
W2/\dom B c=dom B by XBOOLE_1:17;
then A12: w2 c=dom BTK by A6,A10,XBOOLE_1:19;
S2 c=TK by SIMPLEX0:14;
then B.:S2=BTK.:S2 by RELAT_1:162;
then A13: w2 c=S2 by A5,A11,A12,FUNCT_1:157;
A14: S1 c=TK by SIMPLEX0:14;
S2/\dom B=(@S2/\bool the carrier of V)\{{}} by A8,XBOOLE_1:49
.=s2 by XBOOLE_1:28;
then A15: B.:S2=B.:s2 by RELAT_1:145;
then BTK.:s2=B.:S2 by A7,RELAT_1:162;
then A16: s2 c=w2 by A5,A11,A9,FUNCT_1:157;
@S1 c=bool the carrier of V & not{} in S1 by A2;
then S1 c=dom B by A8,ZFMISC_1:40;
then A17: S1 c=dom BTK by A6,A14,XBOOLE_1:19;
B.:S1=BTK.:S1 by A14,RELAT_1:162;
then S1 c=w2 by A4,A5,A11,A17,FUNCT_1:157;
hence S1 c=S2 by A13,XBOOLE_1:1;
let x,y such that
A18: x in S2 & y in S2;
B.:s2=BTK.:s2 by A7,RELAT_1:162;
then w2 c=s2 by A5,A11,A12,A15,FUNCT_1:157;
then A19: s2=w2 by A16,XBOOLE_0:def 10;
per cases;
suppose x is empty or y is empty;
then x c=y or y c=x by XBOOLE_1:2;
hence thesis by XBOOLE_0:def 9;
end;
suppose x is non empty & y is non empty;
then x in w2 & y in w2 by A18,A19,ZFMISC_1:64;
hence thesis by ORDINAL1:def 9;
end;
end;
theorem Th35:
S is with_non-empty_elements & union S c= Aff & card S+n+1 <= card Aff
implies (
Bf is Simplex of n+card S,BCS Complex_of{Aff} & (center_of_mass V).:S c=Bf
iff
ex T st T misses S & T\/S is c=-linear with_non-empty_elements &
card T=n+1 & union T c= Aff &
Bf = (center_of_mass V).:S\/(center_of_mass V).:T)
proof
set B=center_of_mass V,U=union S;
assume that
A1: S is with_non-empty_elements and
A2: U c=Aff and
A3: card S+n+1<=card Aff;
set C=Complex_of{Aff};
reconsider c =card Aff as ext-real number;
set BTC=B|the topology of C;
set BC=BCS C;
A4: the topology of C=bool Aff by SIMPLEX0:4;
A5: degree C=c-1 by SIMPLEX0:26
.=card Aff+-1 by XXREAL_3:def 2;
reconsider c =card S+n as ext-real number;
A6: |.C.|c=[#]C;
then A7: BC=subdivision(B,C) by Def5;
card S+n<=card Aff-1 by A3,XREAL_1:21;
then A8: card S+n<=degree BC by A5,A6,Th31;
hereby A9: S c=the topology of C
proof
let x;
assume x in S;
then x c=U by ZFMISC_1:92;
then x c=Aff by A2,XBOOLE_1:1;
hence thesis by A4;
end;
then A10: B.:S=BTC.:S by RELAT_1:162;
dom B=(bool the carrier of V)\{{}} & not{} in S by A1,FUNCT_2:def 1;
then dom BTC=dom B/\the topology of C & S c=dom B by RELAT_1:90,ZFMISC_1:40;
then A11: S c=dom BTC by A9,XBOOLE_1:19;
assume that
A12: Bf is Simplex of n+card S,BCS Complex_of{Aff} and
A13: B.:S c=Bf;
consider a be c=-linear finite simplex-like Subset-Family of C such that
A14: Bf=B.:a by A7,A12,SIMPLEX0:def 20;
a/\dom B c=a by XBOOLE_1:17;
then reconsider AA=a/\dom B as c=-linear finite simplex-like Subset-Family
of C by TOPS_2:18,XBOOLE_1:1;
A15: B.:S c=B.:AA by A13,A14,RELAT_1:145;
reconsider T=AA\S as Subset-Family of V;
A16: AA c=the topology of C by SIMPLEX0:14;
then A17: B.:AA=BTC.:AA by RELAT_1:162;
A18: S\/T=AA\/S by XBOOLE_1:39
.=AA by A10,A11,A15,A17,FUNCT_1:157,XBOOLE_1:12;
T c=AA by XBOOLE_1:36;
then A19: T c=bool Aff by A4,A16,XBOOLE_1:1;
A20: not{} in AA by ZFMISC_1:64;
then B.:a=B.:(a/\(dom B)) & AA is with_non-empty_elements by RELAT_1:145,
SETFAM_1:def 9;
then A21: card Bf=card AA by A14,Th33;
A22: Bf=B.:AA by A14,RELAT_1:145
.=B.:S\/B.:T by A18,RELAT_1:153;
reconsider T as finite Subset-Family of V;
take T;
card Bf=c+1 by A8,A12,SIMPLEX0:def 18
.=card S+n+1 by XXREAL_3:def 2;
then union bool Aff=Aff & card S+card(AA\S)=card S+n+1 by A18,A21,CARD_2:53,
XBOOLE_1:79,ZFMISC_1:99;
hence T misses S & T\/S is c=-linear with_non-empty_elements & card T=n+
1 & union T c=Aff & Bf=B.:S\/B.:T by A18,A19,A20,A22,SETFAM_1:def 9,XBOOLE_1:79
,ZFMISC_1:95;
end;
given T be finite Subset-Family of V such that
A23: T misses S and
A24: T\/S is c=-linear with_non-empty_elements and
A25: card T=n+1 and
A26: union T c=Aff and
A27: Bf=(center_of_mass V).:S\/(center_of_mass V).:T;
reconsider TS=T\/S as Subset-Family of C;
reconsider t=T as finite Subset-Family of V;
A28: card TS=card t+card S by A23,CARD_2:53
.=card S+n+1 by A25;
union(T\/S)=union T\/union S by ZFMISC_1:96;
then union(T\/S)c=Aff by A2,A26,XBOOLE_1:8;
then T\/S c=bool union(T\/S) & bool union(T\/S)c=bool Aff by ZFMISC_1:79,100;
then A29: T\/S c=the topology of C by A4,XBOOLE_1:1;
A30: TS is simplex-like
proof
let a be Subset of C;
thus thesis by A29,PRE_TOPC:def 5;
end;
[#]BC=[#]C by A7,SIMPLEX0:def 20;
then reconsider BTS=B.:TS as Simplex of BC by A7,A24,A30,SIMPLEX0:def 20;
card TS=card(B.:TS) by A24,A30,Th33;
then A31: card BTS=c+1 by A28,XXREAL_3:def 2;
BTS=Bf by A27,RELAT_1:153;
hence thesis by A8,A27,A31,SIMPLEX0:def 18,XBOOLE_1:7;
end;
theorem Th36:
Sf is with_non-empty_elements & union Sf c=Aff implies
((center_of_mass V).:Sf is Simplex of card union Sf-1,BCS Complex_of {Aff}
iff
for n st 0 < n & n <= card union Sf ex x st x in Sf & card x = n)
proof
reconsider N=0 as Nat;
set U=union Sf;
assume that
A1: Sf is with_non-empty_elements and
A2: union Sf c=Aff;
set B=center_of_mass V,C=Complex_of{Aff};
reconsider s=Sf as c=-linear finite Subset-Family of C;
A3: the topology of C=bool Aff by SIMPLEX0:4;
card U c=card Aff by A2,CARD_1:27;
then card U<=card Aff by NAT_1:40;
then A4: N-1<=card U-1 & card U-1<=card Aff-1 by XREAL_1:11;
Sf c=bool U & bool U c=bool Aff by A2,ZFMISC_1:79,100;
then A5: s c=the topology of C by A3,XBOOLE_1:1;
A6: s is simplex-like
proof
let a be Subset of C;
assume a in s;
hence thesis by A5,PRE_TOPC:def 5;
end;
then A7: card s=card(B.:Sf) by A1,Th33;
card Sf c=card U by A1,SIMPLEX0:10;
then A8: card Sf<=card U by NAT_1:40;
set BC=BCS C;
reconsider c =card Aff as ext-real number;
A9: degree C=c-1 by SIMPLEX0:26
.=card Aff+-1 by XXREAL_3:def 2;
A10: |.C.|c=[#]C;
then A11: BC=subdivision(B,C) by Def5;
then [#]BC=[#]C by SIMPLEX0:def 20;
then reconsider BS=B.:Sf as Subset of BC;
A12: N-1<=card Aff-1 by XREAL_1:11;
A13: degree BC=degree C by A10,Th31;
thus(center_of_mass V).:Sf is Simplex of card U-1,BCS Complex_of{Aff} implies
for n st 0card Sf-n by A14,XREAL_1:8;
A17: card BS=c1+1 by A4,A9,A13,SIMPLEX0:def 18
.=card U-1+1 by XXREAL_3:def 2
.=card U;
then A18: Sf is non empty by A7,A14,A15;
then consider s1 be Subset-Family of U such that
A19: s c=s1 and
s1 is with_non-empty_elements c=-linear and
A20: card U=card s1 and
A21: for Z be set st Z in s1 & card Z<>1 ex x st x in Z & Z\{x} in s1 by A1
,SIMPLEX0:9,13;
card U=card Sf by A1,A6,A17,Th33;
then A22: s=s1 by A19,A20,CARD_FIN:1;
A23: for n st P[n] holds P[n+1]
proof
let n such that
A24: P[n];
assume A25: n+1U
proof
assume UA=U;
then A c=U by XBOOLE_1:7;
hence contradiction by A4,XBOOLE_1:67;
end;
not UA in S
proof
assume UA in S;
then UA c=U by ZFMISC_1:92;
hence contradiction by A6,A15,XBOOLE_0:def 10;
end;
then A16: card SUA=card S+1 by CARD_2:54;
U c1 ex x st x in X & X\{x} in ss1 by A1,
SIMPLEX0:9,13;
card(ss1\s)=card S+1-card S by A2,A5,A7,CARD_2:63;
then consider x such that
A9: ss1\s={x} by CARD_2:60;
reconsider c =card U as ext-real number;
set CU=Complex_of{U};
set TC=the topology of CU;
A10: TC=bool U by SIMPLEX0:4;
then reconsider ss=ss1 as Subset-Family of CU by XBOOLE_1:1;
set BC=BCS CU;
reconsider cc=card U-1 as ext-real number;
A11: |.CU.|c=[#]CU;
then A12: BC=subdivision(B,CU) by Def5;
then A13: [#]BC=[#]CU by SIMPLEX0:def 20;
then reconsider Bss=B.:ss as Subset of BC;
A14: ss is simplex-like
proof
let A be Subset of CU;
assume A in ss;
hence thesis by A10,PRE_TOPC:def 5;
end;
then A15: card Bss=card U by A6,A7,Th33;
then A16: card Bss=cc+1 by A2,XXREAL_3:def 2;
A17: x in {x} by TARSKI:def 1;
then A18: x in ss1 by A9,XBOOLE_0:def 5;
A19: not x in s by A9,A17,XBOOLE_0:def 5;
reconsider x as finite Subset of V by A9,A17,XBOOLE_1:1;
degree CU=c-1 by SIMPLEX0:26
.=card U +-1 by XXREAL_3:def 2;
then A20: cc=degree BC by A11,Th31;
Bss is simplex-like by A6,A12,A14,SIMPLEX0:def 20;
then A21: Bss is Simplex of card U-1,BC by A2,A16,A20,SIMPLEX0:def 18;
x<>{} by A6,A18;
then reconsider c1=card x-1 as Element of NAT by NAT_1:20;
ex xm be set st(xm in s or xm={}) & card xm=card x-1 & for y st y in s & y c=
x holds y c=xm
proof
per cases;
suppose A22: card x=1;
then A23: ex z be set st x={z} by CARD_2:60;
take xm={};
thus(xm in s or xm={}) & card xm=card x-1 by A22;
let y such that
A24: y in s and
A25: y c=x;
y<>x by A9,A17,A24,XBOOLE_0:def 5;
hence thesis by A23,A25,ZFMISC_1:39;
end;
suppose card x<>1;
then consider z be set such that
A26: z in x and
A27: x\{z} in ss1 by A8,A18;
take xm=x\{z};
A28: x=xm\/{z} by A26,ZFMISC_1:140;
xm in s
proof
assume not xm in s;
then xm in ss1\s by A27,XBOOLE_0:def 5;
then xm=x by A9,TARSKI:def 1;
hence thesis by A26,ZFMISC_1:64;
end;
hence xm in s or xm={};
card x=c1+1;
hence card xm=card x-1 by A26,STIRL2_1:65;
let y such that
A29: y in s and
A30: y c=x;
assume A31: not y c=xm;
xm,y are_c=-comparable by A5,A6,A27,A29,ORDINAL1:def 9;
then xm c=y by A31,XBOOLE_0:def 9;
hence contradiction by A19,A28,A29,A30,A31,BORSUK_5:2;
end;
end;
then consider xm be set such that
A32: xm in s or xm={} and
A33: card xm=card x-1 and
A34: for y st y in s & y c=x holds y c=xm;
A35: U in S by A4,SIMPLEX0:9;
then union ss1 c=U & U c=union ss by A5,ZFMISC_1:92;
then A36: union ss=U by XBOOLE_0:def 10;
x c____x2 and
A43: xM\xm={x1,x2} by A33,A38,CARD_2:79;
A44: x1 in {x1,x2} by TARSKI:def 2;
A45: x2 in {x1,x2} by TARSKI:def 2;
then reconsider x1,x2 as Element of V by A43,A44;
set xm1=xm\/{x1},xm2=xm\/{x2};
reconsider S1=S\/{xm1},S2=S\/{xm2} as Subset-Family of CU;
reconsider BS1=B.:S1,BS2=B.:S2 as Subset of BC by A13;
A46: BS1=B.:S\/B.:{xm1} by RELAT_1:153;
A47: not x1 in xm by A43,A44,XBOOLE_0:def 5;
then A48: card xm1=card xm+1 by CARD_2:54;
A49: not xm1 in S
proof
assume A50: xm1 in S;
then x,xm1 are_c=-comparable by A5,A6,A18,ORDINAL1:def 9;
then x c=xm1 or xm1 c=x by XBOOLE_0:def 9;
hence thesis by A19,A33,A48,A50,CARD_FIN:1;
end;
not x2 in xm by A43,A45,XBOOLE_0:def 5;
then A51: card xm2=card xm+1 by CARD_2:54;
A52: not xm2 in S
proof
assume A53: xm2 in S;
then x,xm2 are_c=-comparable by A5,A6,A18,ORDINAL1:def 9;
then x c=xm2 or xm2 c=x by XBOOLE_0:def 9;
hence thesis by A19,A33,A51,A53,CARD_FIN:1;
end;
x2 in xM by A43,A45,XBOOLE_0:def 5;
then {x2}c=xM by ZFMISC_1:37;
then A54: xm2 c=xM by A41,XBOOLE_1:8;
A55: S2 c=bool U
proof
let A be set such that
A56: A in S2;
per cases by A56,XBOOLE_0:def 3;
suppose A in S;
then A c=U by ZFMISC_1:92;
hence thesis;
end;
suppose A in {xm2};
then A=xm2 by TARSKI:def 1;
then A c=U by A37,A54,XBOOLE_1:1;
hence thesis;
end;
end;
A57: S2 is simplex-like
proof
let A be Subset of CU;
assume A in S2;
hence thesis by A10,A55,PRE_TOPC:def 5;
end;
then card BS2=card S2 by A1,Th33;
then A58: card BS2=card S+1 by A52,CARD_2:54;
x1 in xM by A43,A44,XBOOLE_0:def 5;
then {x1}c=xM by ZFMISC_1:37;
then A59: xm1 c=xM by A41,XBOOLE_1:8;
A60: S1 c=bool U
proof
let A be set such that
A61: A in S1;
per cases by A61,XBOOLE_0:def 3;
suppose A in S;
then A c=U by ZFMISC_1:92;
hence thesis;
end;
suppose A in {xm1};
then A=xm1 by TARSKI:def 1;
then A c=U by A37,A59,XBOOLE_1:1;
hence thesis;
end;
end;
then A62: BS1=(B|TC).:S1 by A10,RELAT_1:162;
A63: S1 is simplex-like
proof
let A be Subset of CU;
assume A in S1;
hence thesis by A10,A60,PRE_TOPC:def 5;
end;
then card BS1=card S1 by A1,Th33;
then A64: card BS1=card S+1 by A49,CARD_2:54;
A65: xm c=xm1 & xm c=xm2 by XBOOLE_1:7;
A66: for y1 be set st y1 in S holds y1,xm1 are_c=-comparable & y1,xm2
are_c=-comparable
proof
let y1 be set;
assume A67: y1 in S;
then A68: xM,y1 are_c=-comparable by A40,ORDINAL1:def 9;
per cases by A68,XBOOLE_0:def 9;
suppose xM c=y1 or xM=y1;
then xm1 c=y1 & xm2 c=y1 by A54,A59,XBOOLE_1:1;
hence thesis by XBOOLE_0:def 9;
end;
suppose A69: y1 c=xM & xM<>y1;
then reconsider y1 as finite set;
A70: y1 cx4 by A95,NAT_1:13;
then not x4 in {x} by TARSKI:def 1;
then A96: x4 in s by A9,A94,XBOOLE_0:def 5;
then x4 in S\/T by XBOOLE_0:def 3;
then x3,x4 are_c=-comparable by A84,A92,ORDINAL1:def 9;
then x3 c=x4 or x4 c=x3 by XBOOLE_0:def 9;
hence contradiction by A90,A95,A96,CARD_FIN:1;
end;
A97: xm c=x3 & xm<>x3
proof
per cases by A32;
suppose xm={};
hence thesis by A84,A92,XBOOLE_1:2;
end;
suppose A98: xm in s;
A99: not x3 c=xm
proof
assume x3 c=xm;
then A100: card x3<=card xm by NAT_1:44;
consider x4 be set such that
A101: x4 in ss and
A102: card x4=card x3 by A6,A36,A21,A84,A92,Th36,NAT_1:44;
card xm+1=card x by A33;
then card x<>card x3 by A100,NAT_1:13;
then not x4 in {x} by A102,TARSKI:def 1;
then A103: x4 in s by A9,A101,XBOOLE_0:def 5;
then x4 in S\/T by XBOOLE_0:def 3;
then x3,x4 are_c=-comparable by A84,A92,ORDINAL1:def 9;
then x3 c=x4 or x4 c=x3 by XBOOLE_0:def 9;
hence contradiction by A90,A102,A103,CARD_FIN:1;
end;
xm in T\/S by A98,XBOOLE_0:def 3;
then xm,x3 are_c=-comparable by A84,A92,ORDINAL1:def 9;
hence thesis by A99,XBOOLE_0:def 9;
end;
end;
then A104: x3=x3\/xm by XBOOLE_1:12;
xM in S\/T by A40,XBOOLE_0:def 3;
then xM,x3 are_c=-comparable by A84,A92,ORDINAL1:def 9;
then x3 c=xM by A93,XBOOLE_0:def 9;
then A105: x3\xm c=xM\xm by XBOOLE_1:33;
A106: xM=xm\/xM by A41,XBOOLE_1:12;
A107: x3\xm<>xM\xm
proof
assume x3\xm=xM\xm;
then x3=(xM\xm)\/xm by A104,XBOOLE_1:39;
hence contradiction by A93,A106,XBOOLE_1:39;
end;
A108: x3\xm<>{}
proof
assume x3\xm={};
then x3 c=xm by XBOOLE_1:37;
hence contradiction by A97,XBOOLE_0:def 10;
end;
x3\/xm=(x3\xm)\/xm by XBOOLE_1:39;
then x3=xm1 or x3=xm2 by A43,A104,A105,A107,A108,ZFMISC_1:42;
hence thesis by A79,A46,A81,A87,A88,TARSKI:def 2;
end;
A109: BS2=(B|TC).:S2 by A10,A55,RELAT_1:162;
A110: BS1<>BS2
proof
assume A111: BS1=BS2;
then BS1\BS2={} by XBOOLE_1:37;
then (B|TC).:(S1\S2)={} by A109,A62,FUNCT_1:123;
then A112: dom(B|TC)misses S1\S2 by RELAT_1:151;
BS2\BS1={} by A111,XBOOLE_1:37;
then (B|TC).:(S2\S1)={} by A109,A62,FUNCT_1:123;
then A113: dom(B|TC)misses S2\S1 by RELAT_1:151;
A114: dom(B|TC)=dom B/\TC by RELAT_1:90;
xm1 in {xm1} by TARSKI:def 1;
then A115: xm1 in S1 by XBOOLE_0:def 3;
A116: dom B=(bool the carrier of V)\{{}} by FUNCT_2:def 1;
A117: S1\S2 c=S1 by XBOOLE_1:36;
then not{} in S1\S2 by A1;
then A118: S1\S2 c=dom B by A116,ZFMISC_1:40;
A119: S2\S1 c=S2 by XBOOLE_1:36;
then not{} in S2\S1 by A1;
then A120: S2\S1 c=dom B by A116,ZFMISC_1:40;
S1\S2 c=bool U by A60,A117,XBOOLE_1:1;
then S1\S2 c=dom(B|TC) by A10,A114,A118,XBOOLE_1:19;
then A121: S1\S2={} by A112,XBOOLE_1:67;
S2\S1 c=bool U by A55,A119,XBOOLE_1:1;
then S2\S1 c=dom(B|TC) by A10,A114,A120,XBOOLE_1:19;
then S1=S2 by A113,A121,XBOOLE_1:32,67;
then xm1 in {xm2} by A49,A115,XBOOLE_0:def 3;
then A122: xm1=xm2 by TARSKI:def 1;
x1 in {x1} by TARSKI:def 1;
then x1 in xm1 by XBOOLE_0:def 3;
then x1 in {x2} by A47,A122,XBOOLE_0:def 3;
hence contradiction by A42,TARSKI:def 1;
end;
S2 is c=-linear
proof
let y1,y2 be set;
assume that
A123: y1 in S2 and
A124: y2 in S2;
y1 in S or y1 in {xm2} by A123,XBOOLE_0:def 3;
then A125: y1 in S or y1=xm2 by TARSKI:def 1;
y2 in S or y2 in {xm2} by A124,XBOOLE_0:def 3;
then y2 in S or y2=xm2 by TARSKI:def 1;
hence thesis by A66,A125,ORDINAL1:def 9;
end;
then BS2 is simplex-like by A12,A57,SIMPLEX0:def 20;
then A126: BS2 is Simplex of card U-1,BC by A2,A15,A16,A20,A58,SIMPLEX0:def
18;
B.:S c=B.:S\/B.:{xm2} by XBOOLE_1:7;
then BS2 in SS by A2,A79,A126;
then {BS1,BS2}c=SS by A78,ZFMISC_1:38;
then SS={BS1,BS2} by A80,XBOOLE_0:def 10;
hence thesis by A110,CARD_2:76;
end;
theorem Th40:
Aff is Simplex of K implies (B is Simplex of BCS Complex_of{Aff} iff
B is Simplex of BCS K & conv B c= conv Aff)
proof
set Bag=center_of_mass V;
set C=Complex_of{Aff};
A1: the topology of C=bool Aff by SIMPLEX0:4;
assume Aff is Simplex of K;
then reconsider s=Aff as Simplex of K;
A2: [#]K=the carrier of V by SIMPLEX0:def 10;
then |.K.|c=[#]K;
then A3: subdivision(Bag,K)=BCS K by Def5;
@s is affinely-independent;
then A4: Complex_of{Aff} is SubSimplicialComplex of K by Th3;
then the topology of C c=the topology of K by SIMPLEX0:def 13;
then A5: |.C.|c=|.K.| by Th4;
[#]C=[#]V;
then A6: subdivision(Bag,C)=BCS C by A5,Def5;
then BCS C is SubSimplicialComplex of BCS K by A3,A4,SIMPLEX0:58;
then A7: the topology of BCS C c=the topology of BCS K by SIMPLEX0:def 13;
hereby assume B is Simplex of BCS C;
then reconsider A=B as Simplex of BCS C;
A in the topology of BCS C by PRE_TOPC:def 5;
then A in the topology of BCS K by A7;
then reconsider a=A as Simplex of BCS K by PRE_TOPC:def 5;
|.BCS C.|=|.C.| & conv@A c=|.BCS C.| by Th5,Th10;
then conv@a c=conv Aff by Th8;
hence B is Simplex of BCS K & conv B c=conv Aff;
end;
assume that
A8: B is Simplex of BCS K and
A9: conv B c=conv Aff;
reconsider A=B as Simplex of BCS K by A8;
consider SS be c=-linear finite simplex-like Subset-Family of K such that
A10: B=Bag.:SS by A3,A8,SIMPLEX0:def 20;
reconsider ss=SS as c=-linear finite Subset-Family of C by A2;
[#]subdivision(Bag,C)=[#]C by SIMPLEX0:def 20;
then reconsider Bss=Bag.:ss as Subset of BCS C by A5,Def5;
A11: dom Bag=(bool the carrier of V)\{{}} by FUNCT_2:def 1;
ss is simplex-like
proof
let a be Subset of C such that
A12: a in ss;
reconsider aK=a as Simplex of K by A12,TOPS_2:def 1;
per cases;
suppose aK is empty;
hence thesis;
end;
suppose A13: aK is non empty;
then aK in dom Bag by A11,ZFMISC_1:64;
then A14: Bag.aK in A by A10,A12,FUNCT_1:def 12;
A15: Bag.aK in Int@aK by A13,RLAFFIN2:20;
A c=conv@A by RLAFFIN1:2;
then Bag.aK in conv@A by A14;
then Int@aK meets conv@s by A9,A15,XBOOLE_0:3;
then aK c=Aff by Th26;
hence thesis by A1,PRE_TOPC:def 5;
end;
end;
then Bss is simplex-like by A6,SIMPLEX0:def 20;
hence thesis by A10;
end;
theorem Th41:
Sk is with_non-empty_elements & card Sk+n <= degree K implies
(Af is Simplex of n+card Sk,BCS K & (center_of_mass V).:Sk c=Af
iff
ex Tk st Tk misses Sk & Tk\/Sk is c=-linear with_non-empty_elements &
card Tk=n+1 & Af = (center_of_mass V).:Sk\/(center_of_mass V).:Tk)
proof
set B=center_of_mass V;
set BK=BCS K;
assume that
A1: Sk is with_non-empty_elements and
A2: card Sk+n<=degree K;
reconsider nc=n+card Sk as ext-real number;
A3: nc+1-1=nc by XXREAL_3:22;
A4: [#]K=the carrier of V by SIMPLEX0:def 10;
then A5: |.K.|c=[#]K;
then A6: subdivision(B,K)=BK by Def5;
A7: nc<=degree BK by A2,A5,Th31;
hereby assume that
A8: Af is Simplex of n+card Sk,BK and
A9: B.:Sk c=Af;
consider T be c=-linear finite simplex-like Subset-Family of K such that
A10: Af=B.:T by A6,A8,SIMPLEX0:def 20;
union T is empty or union T in T by SIMPLEX0:9,ZFMISC_1:2;
then A11: union T is simplex-like by TOPS_2:def 1;
then @union T is affinely-independent;
then reconsider UT=union T as finite affinely-independent Subset of V;
UT=union@T;
then conv Af c=conv UT by A10,CONVEX1:30,RLAFFIN2:17;
then reconsider s1=Af as Simplex of BCS Complex_of{UT} by A8,A11,Th40;
card Af=nc+1 by A7,A8,SIMPLEX0:def 18;
then A12: s1 is Simplex of n+card Sk,BCS Complex_of{UT} by A3,SIMPLEX0:48;
set C=Complex_of{UT};
reconsider cT=card UT as ext-real number;
|.C.|c=[#]C;
then A13: degree C=degree BCS C by Th31;
degree C=cT-1 & card s1<=degree BCS C+1 by SIMPLEX0:24,26;
then card s1<=card UT by A13,XXREAL_3:22;
then nc+1<=card UT by A7,A8,SIMPLEX0:def 18;
then A14: card Sk+n+1<=card UT by XXREAL_3:def 2;
the_family_of K is subset-closed & UT in the topology of K by A11,PRE_TOPC:
def 5;
then A15: bool UT c=the topology of K by SIMPLEX0:1;
union@Sk c=union T by A1,A5,A8,A9,A10,Th34,ZFMISC_1:95;
then consider R be finite Subset-Family of V such that
A16: R misses Sk & R\/Sk is c=-linear with_non-empty_elements & card R=n+1
and
A17: union R c=UT and
A18: Af=(center_of_mass V).:Sk\/(center_of_mass V).:R
by A1,A9,A12,A14,Th35;
reconsider R as Subset-Family of K by A4;
R c=bool union R & bool union R c=bool UT by A17,SIMPLEX0:1,ZFMISC_1:100;
then R c=bool UT by XBOOLE_1:1;
then R c=the topology of K by A15,XBOOLE_1:1;
then reconsider R as simplex-like finite Subset-Family of K by SIMPLEX0:14;
take R;
thus R misses Sk & R\/Sk is c=-linear with_non-empty_elements & card R=n+1 &
Af=B.:Sk\/B.:R by A16,A18;
end;
given T be simplex-like finite Subset-Family of K such that
A19: T misses Sk and
A20: T\/Sk is c=-linear with_non-empty_elements and
A21: card T=n+1 and
A22: Af=B.:Sk\/B.:T;
set ST=Sk\/T;
[#]K=[#]BK by A6,SIMPLEX0:def 20;
then reconsider BST=B.:ST as Subset of BK by SIMPLEX0:def 10;
A23: ST is simplex-like by TOPS_2:20;
then reconsider BST as Simplex of BK by A6,A20,SIMPLEX0:def 20;
card ST=card Sk+card T by A19,CARD_2:53;
then card BST=card Sk+n+1 by A20,A21,A23,Th33;
then B.:Sk\/B.:T=B.:ST & card BST=nc+1 by RELAT_1:153,XXREAL_3:def 2;
hence thesis by A3,A22,SIMPLEX0:48,XBOOLE_1:7;
end;
theorem Th42:
Sk is c=-linear with_non-empty_elements & card Sk = card union Sk &
union Sk c= Ak & card Ak = card Sk+1
implies
{S1 where S1 is Simplex of card Sk,BCS K:
(center_of_mass V).:Sk c= S1 & conv @S1 c= conv @Ak}
= {(center_of_mass V).:Sk \/(center_of_mass V).:{Ak}}
proof
set B=center_of_mass V;
assume that
A1: Sk is c=-linear with_non-empty_elements and
A2: card Sk=card union Sk and
A3: union Sk c=Ak and
A4: card Ak=card Sk+1;
card(Ak\union Sk)=card Sk+1-card Sk by A2,A3,A4,CARD_2:63
.=1;
then consider v be set such that
A5: Ak\union Sk={v} by CARD_2:60;
reconsider Ak1=@Ak as affinely-independent finite Subset of V;
set C=Complex_of{Ak1};
reconsider c =card Ak as ext-real number;
A6: degree C=c-1 by SIMPLEX0:26
.=card Ak+-1 by XXREAL_3:def 2
.=card Sk by A4;
reconsider Sk1=@Sk as c=-linear finite finite-membered Subset-Family of V by
A1;
set XX={W where W is Simplex of card Sk,BCS C:B.:Sk c=W};
set YY={W where W is Simplex of card Sk,BCS K:B.:Sk c=W & conv@W c=conv@Ak};
[#]K=the carrier of V by SIMPLEX0:def 10;
then |.K.|c=[#]K;
then A7: subdivision(B,K)=BCS K by Def5;
A8: C is SubSimplicialComplex of K by Th3;
then the topology of C c=the topology of K by SIMPLEX0:def 13;
then A9: |.C.|c=|.K.| by Th4;
A10: [#]C=[#]V;
then A11: degree C=degree BCS C by A9,Th31;
subdivision(B,C)=BCS C by A9,A10,Def5;
then BCS C is SubSimplicialComplex of BCS K by A7,A8,SIMPLEX0:58;
then A12: degree BCS C<=degree BCS K by SIMPLEX0:32;
A13: XX c=YY
proof
let x;
assume x in XX;
then consider W be Simplex of card Sk,BCS C such that
A14: x=W & B.:Sk1 c=W;
W=@W;
then reconsider w=W as Simplex of BCS K by Th40;
card W=degree BCS C+1 by A6,A11,SIMPLEX0:def 18;
then A15: w is Simplex of card Sk,BCS K by A6,A11,A12,SIMPLEX0:def 18;
conv@W c=conv@Ak & @w=w by Th40;
hence thesis by A14,A15;
end;
A16: [#]subdivision(B,C)=[#]C by SIMPLEX0:def 20;
A17: YY c=XX
proof
let x;
reconsider c1=card Sk as ext-real number;
assume x in YY;
then consider W be Simplex of card Sk,BCS K such that
A18: W=x & B.:Sk c=W and
A19: conv@W c=conv@Ak;
reconsider w=@W as Subset of BCS C by A9,A16,Def5;
reconsider cW=card W as ext-real number;
card W=c1+1 by A6,A11,A12,SIMPLEX0:def 18
.=card Sk+1 by XXREAL_3:def 2;
then card Sk=card W+-1;
then A20: card Sk=cW-1 by XXREAL_3:def 2;
w is simplex-like by A19,Th40;
then w is Simplex of card Sk,BCS C by A20,SIMPLEX0:48;
hence thesis by A18;
end;
v in {v} by TARSKI:def 1;
then A21: v in Ak1 & not v in union Sk by A5,XBOOLE_0:def 5;
Ak=Ak\/union Sk by A3,XBOOLE_1:12
.={v}\/union Sk1 by A5,XBOOLE_1:39;
then XX={B.:Sk1\/B.:{Ak}} by A1,A2,A21,Th38;
hence thesis by A13,A17,XBOOLE_0:def 10;
end;
theorem Th43:
Sk is c=-linear with_non-empty_elements & card Sk+1 = card union Sk
implies card {S1 where S1 is Simplex of card Sk,BCS K:
(center_of_mass V).:Sk c= S1 & conv @S1 c= conv @union Sk} = 2
proof
set B=center_of_mass V;
assume that
A1: Sk is c=-linear with_non-empty_elements and
A2: card Sk+1=card union Sk;
Sk is non empty by A2,ZFMISC_1:2;
then union Sk in Sk by A1,SIMPLEX0:9;
then reconsider U=union Sk as Simplex of K by TOPS_2:def 1;
reconsider Sk1=@Sk as c=-linear finite finite-membered Subset-Family of V by
A1;
reconsider c =card U as ext-real number;
@U=union Sk1;
then reconsider U1=union Sk1 as finite affinely-independent Subset of V;
set C=Complex_of{U1};
A3: degree C=c-1 by SIMPLEX0:26
.=card U +-1 by XXREAL_3:def 2
.=card Sk by A2;
set YY={W where W is Simplex of card Sk,BCS K:B.:Sk c=W & conv@W c=conv@
union Sk};
[#]K=the carrier of V by SIMPLEX0:def 10;
then |.K.|c=[#]K;
then A4: subdivision(B,K)=BCS K by Def5;
set XX={W where W is Simplex of card Sk,BCS C:B.:Sk c=W};
A5: @U=U1;
then A6: C is SubSimplicialComplex of K by Th3;
then the topology of C c=the topology of K by SIMPLEX0:def 13;
then A7: |.C.|c=|.K.| by Th4;
A8: [#]C=[#]V;
then A9: degree C=degree BCS C by A7,Th31;
subdivision(B,C)=BCS C by A7,A8,Def5;
then BCS C is SubSimplicialComplex of BCS K by A4,A6,SIMPLEX0:58;
then A10: degree BCS C<=degree BCS K by SIMPLEX0:32;
A11: XX c=YY
proof
let x;
assume x in XX;
then consider W be Simplex of card Sk,BCS C such that
A12: x=W & B.:Sk1 c=W;
W=@W;
then reconsider w=W as Simplex of BCS K by A5,Th40;
card W=degree BCS C+1 by A3,A9,SIMPLEX0:def 18;
then A13: w is Simplex of card Sk,BCS K by A3,A9,A10,SIMPLEX0:def 18;
conv@W c=conv@U & @w=w by Th40;
hence thesis by A12,A13;
end;
A14: [#]subdivision(B,C)=[#]C by SIMPLEX0:def 20;
A15: YY c=XX
proof
let x;
reconsider c1=card Sk as ext-real number;
assume x in YY;
then consider W be Simplex of card Sk,BCS K such that
A16: W=x & B.:Sk c=W and
A17: conv@W c=conv@U;
reconsider w=@W as Subset of BCS C by A7,A14,Def5;
reconsider cW=card W as ext-real number;
card W=c1+1 by A3,A9,A10,SIMPLEX0:def 18
.=card Sk+1 by XXREAL_3:def 2;
then card Sk=card W+-1;
then A18: card Sk=cW-1 by XXREAL_3:def 2;
w is simplex-like by A17,Th40;
then w is Simplex of card Sk,BCS C by A18,SIMPLEX0:48;
hence thesis by A16;
end;
card XX=2 by A1,A2,Th39;
hence thesis by A11,A15,XBOOLE_0:def 10;
end;
theorem Th44:
for Af st K is Subdivision of Complex_of{Af} & card Af = n+1 & degree K = n &
for S be Simplex of n-1,K,X st X = {S1 where S1 is Simplex of n,K: S c= S1}
holds (conv @S meets Int Af implies card X = 2) &
(conv @S misses Int Af implies card X = 1)
holds
for S be Simplex of n-1,BCS K,X st
X = {S1 where S1 is Simplex of n,BCS K:S c= S1}
holds (conv @S meets Int Af implies card X = 2) &
(conv @S misses Int Af implies card X = 1)
proof
let A be finite Subset of V;
assume that
A1: K is Subdivision of Complex_of{A} and
A2: card A=n+1 and
A3: degree K=n and
A4: for S be Simplex of n-1,K,X be set st X={S1 where S1 is Simplex of n,K:S
c=S1} holds(conv@S meets Int A implies card X=2) & (conv@S misses Int A implies
card X=1);
|.Complex_of{A}.|=conv A by Th8;
then A5: |.K.|=conv A by A1,Th10;
A6: K is finite-degree by A3,SIMPLEX0:def 12;
A7: A is affinely-independent
proof
consider a be Subset of K such that
A8: a is simplex-like and
A9: card a=degree K+1 by A6,SIMPLEX0:def 12;
conv@a c=conv A by A5,A8,Th5;
then A10: Affin@a c=Affin A by RLAFFIN1:68;
card A=card a by A2,A3,A9,XXREAL_3:def 2;
hence thesis by A8,A10,RLAFFIN1:80;
end;
set B=center_of_mass V;
reconsider Z=0 as Nat;
set TK=the TopStruct of K;
reconsider n1=n-1 as ext-real number;
let S be Simplex of n-1,BCS K,X be set such that
A11: X={S1 where S1 is Simplex of n,BCS K:S c=S1};
[#]K=the carrier of V by SIMPLEX0:def 10;
then A12: |.K.|c=[#]K;
then A13: degree K=degree BCS K by Th31;
then A14: n+-1>=-1 & n-1<=degree BCS K by A3,XREAL_1:33,148;
then A15: card S=n1+1 by SIMPLEX0:def 18;
then A16: card S=(n-1)+1 by XXREAL_3:def 2;
A17: BCS K=subdivision(B,K) by A12,Def5;
per cases;
suppose A18: n=0;
then A19: TK=BCS K by A3,A12,Th21;
then S in the topology of K by PRE_TOPC:def 5;
then reconsider s=S as Simplex of K by PRE_TOPC:def 5;
reconsider s as Simplex of n-1,K by A3,A15,A18,SIMPLEX0:def 18;
set XX={W where W is Simplex of n,K:s c=W};
A20: @S=@s;
then A21: conv@S meets Int A implies card XX=2 by A4;
A22: XX c=X
proof
let x;
assume x in XX;
then consider W be Simplex of n,K such that
A23: x=W & S c=W;
W in the topology of BCS K by A19,PRE_TOPC:def 5;
then reconsider w=W as Simplex of BCS K by PRE_TOPC:def 5;
card W=(degree K)+1 by A3,SIMPLEX0:def 18;
then w is Simplex of n,BCS K by A3,A13,SIMPLEX0:def 18;
hence thesis by A11,A23;
end;
A24: X c=XX
proof
let x;
assume x in X;
then consider W be Simplex of n,BCS K such that
A25: x=W & S c=W by A11;
W in the topology of K by A19,PRE_TOPC:def 5;
then reconsider w=W as Simplex of K by PRE_TOPC:def 5;
card W=(degree BCS K)+1 by A3,A13,SIMPLEX0:def 18;
then w is Simplex of n,K by A3,A13,SIMPLEX0:def 18;
hence thesis by A25;
end;
conv@S misses Int A implies card XX=1 by A4,A20;
hence thesis by A22,A24,A21,XBOOLE_0:def 10;
end;
suppose A26: n>0;
consider SS be c=-linear finite simplex-like Subset-Family of K such that
A27: S=B.:SS by A17,SIMPLEX0:def 20;
SS\{{}}c=SS by XBOOLE_1:36;
then reconsider SS1=SS\{{}} as c=-linear finite simplex-like Subset-Family
of K by TOPS_2:18;
A28: SS1 c=bool@(union SS1) & bool@(union SS1)c=bool the carrier of V by
ZFMISC_1:79,100;
A29: not{} in SS1 by ZFMISC_1:64;
then A30: SS1 is with_non-empty_elements by SETFAM_1:def 9;
A31: dom B=(bool the carrier of V)\{{}} by FUNCT_2:def 1;
then A32: SS/\dom B=(SS/\(bool the carrier of V))\{{}} by XBOOLE_1:49
.=SS1/\(bool the carrier of V) by XBOOLE_1:49
.=SS1 by A28,XBOOLE_1:1,28;
then A33: B.:SS=B.:SS1 by RELAT_1:145;
then A34: card SS1=n by A16,A27,A30,Th33;
A35: S=B.:SS1 by A27,A32,RELAT_1:145;
A36: card SS1=card S by A27,A30,A33,Th33;
then A37: SS1 is non empty by A16,A26;
then A38: union SS1 in SS1 by SIMPLEX0:9;
then reconsider U=union SS1 as Simplex of K by TOPS_2:def 1;
card SS1 c=card U by A30,SIMPLEX0:10;
then A39: n<=card U by A16,A36,NAT_1:40;
card U<=degree K+1 by SIMPLEX0:24;
then A40: card U<=n+1 by A3,XXREAL_3:def 2;
A41: conv@U c=conv A by A5,Th5;
SS1 c=bool the carrier of V by A28,XBOOLE_1:1;
then A42: conv@S c=conv@U by A35,CONVEX1:30,RLAFFIN2:17;
per cases by A39,A40,NAT_1:9;
suppose A43: card U=n;
set XX={W where W is Simplex of n,K:U c=W};
A44: U is Simplex of n-1,K by A13,A14,A15,A16,A43,SIMPLEX0:def 18;
hereby assume conv@S meets Int A;
then conv@U meets Int A by A42,XBOOLE_1:63;
then A45: card XX=2 by A4,A44;
then XX is finite;
then consider w1,w2 be set such that
A46: w1<>w2 and
A47: XX={w1,w2} by A45,CARD_2:79;
w2 in XX by A47,TARSKI:def 2;
then consider W2 be Simplex of n,K such that
A48: w2=W2 and
A49: U c=W2;
A50: SS1 is with_non-empty_elements & S=B.:SS1 by A27,A29,A32,RELAT_1:145,
SETFAM_1:def 9;
w1 in XX by A47,TARSKI:def 2;
then consider W1 be Simplex of n,K such that
A51: w1=W1 and
A52: U c=W1;
A53: card W1=degree K+1 by A3,SIMPLEX0:def 18;
then A54: card W1=n+1 by A3,XXREAL_3:def 2;
then {W where W is Simplex of n,BCS K:S c=W & conv@W c=conv@W1}={S\/B.:{
W1}} by A16,A27,A30,A33,A36,A43,A52,Th42;
then S\/B.:{W1} in {W where W is Simplex of n,BCS K:S c=W & conv@W c=conv
@W1} by TARSKI:def 1;
then A55: ex R be Simplex of n,BCS K st R=S\/B.:{W1} & S c=R & conv@R c=
conv@W1;
A56: S\/B.:{W1}<>S\/B.:{W2}
proof
for A be Subset of K st A in {W1} holds A is simplex-like by TARSKI:def 1
;
then {W1} is simplex-like by TOPS_2:def 1;
then A57: SS1\/{W1} is simplex-like by TOPS_2:20;
A58: S\/B.:{W1}=B.:(SS1\/{W1}) & S\/B.:{W2}=B.:(SS1\/{W2}) by A35,RELAT_1
:153;
W1 in {W1} by TARSKI:def 1;
then A59: W1 in SS1\/{W1} by XBOOLE_0:def 3;
for A be Subset of K st A in {W2} holds A is simplex-like by TARSKI:def 1
;
then {W2} is simplex-like by TOPS_2:def 1;
then A60: SS1\/{W2} is simplex-like by TOPS_2:20;
assume A61: S\/B.:{W1}=S\/B.:{W2};
W1 is non empty by A3,A53;
then SS1\/{W1}c=SS1\/{W2} by A12,A30,A55,A60,A58,A57,A61,Th34;
then W1 in SS1 or W1 in {W2} by A59,XBOOLE_0:def 3;
then W1 c=U by A46,A48,A51,TARSKI:def 1,ZFMISC_1:92;
then W1=U by A52,XBOOLE_0:def 10;
hence contradiction by A43,A54;
end;
A62: card SS1+Z<=degree K by A3,A16,A27,A30,A33,Th33;
A63: X c={S\/B.:{W1},S\/B.:{W2}}
proof
let x;
A64: n+1=degree K+1 & n=degree K+1-1 by A3,XXREAL_3:22,def 2;
assume x in X;
then consider W be Simplex of n,BCS K such that
A65: x=W and
A66: S c=W by A11;
consider T be simplex-like finite Subset-Family of K such that
A67: T misses SS1 and
A68: T\/SS1 is c=-linear with_non-empty_elements and
A69: card T=Z+1 and
A70: @W=B.:SS1\/B.:T by A16,A36,A50,A62,A66,Th41;
consider t be set such that
A71: T={t} by A69,CARD_2:60;
set TS=T\/SS1;
A72: card TS=n+1 by A16,A36,A67,A69,CARD_2:53;
A73: union TS in TS by A68,A71,SIMPLEX0:9;
TS is simplex-like by TOPS_2:20;
then reconsider UTS=union TS as Simplex of K by A73,TOPS_2:def 1;
card TS c=card UTS by A68,SIMPLEX0:10;
then A74: card TS<=card UTS by NAT_1:40;
UTS in T
proof
assume not UTS in T;
then UTS in SS1 by A73,XBOOLE_0:def 3;
then card UTS<=card U by NAT_1:44,ZFMISC_1:92;
hence contradiction by A43,A72,A74,NAT_1:13;
end;
then A75: UTS=t by A71,TARSKI:def 1;
card UTS<=degree K+1 by SIMPLEX0:24;
then card UTS<=n+1 by A3,XXREAL_3:def 2;
then card UTS=n+1 by A72,A74,XXREAL_0:1;
then A76: UTS is Simplex of n,K by A64,SIMPLEX0:48;
U c=UTS by XBOOLE_1:7,ZFMISC_1:95;
then UTS in XX by A76;
then W=B.:SS1\/B.:{W1} or W=B.:SS1\/B.:{W2} by A47,A48,A51,A70,A71,A75
,TARSKI:def 2;
hence thesis by A35,A65,TARSKI:def 2;
end;
card W2=degree K+1 by A3,SIMPLEX0:def 18;
then card W2=n+1 by A3,XXREAL_3:def 2;
then {W where W is Simplex of n,BCS K:S c=W & conv@W c=conv@W2}={S\/B.:{
W2}} by A16,A30,A35,A36,A43,A49,Th42;
then S\/B.:{W2} in {W where W is Simplex of n,BCS K:S c=W & conv@W c=conv
@W2} by TARSKI:def 1;
then ex R be Simplex of n,BCS K st R=S\/B.:{W2} & S c=R & conv@R c=conv@
W2;
then A77: S\/B.:{W2} in X by A11;
S\/B.:{W1} in X by A11,A55;
then {S\/B.:{W1},S\/B.:{W2}}c=X by A77,ZFMISC_1:38;
then X={S\/B.:{W1},S\/B.:{W2}} by A63,XBOOLE_0:def 10;
hence card X=2 by A56,CARD_2:76;
end;
A78: conv@S c=conv A & A is non empty by A2,A41,A42,XBOOLE_1:1;
assume conv@S misses Int A;
then consider BB be Subset of V such that
A79: BB c=0 by A7,A86,RLAFFIN1:71;
BUU.(G.i)=1/card U by A92,A95,A99,RLAFFIN2:18;
hence 0<=F.i by A98,A100;
end;
B.U in conv@S by A84;
then A101: B.U in conv BB by A80;
assume not U c=conv B1;
then consider t be set such that
A102: t in U and
A103: not t in conv B1 by TARSKI:def 3;
A104: (t|--A).ab>0
proof
A\{ab}c=B1
proof
let x;
assume x in A\{ab};
then x in A & not x in {ab} by XBOOLE_0:def 5;
hence thesis by A83,XBOOLE_0:def 5;
end;
then A105: conv(A\{ab})c=conv B1 by RLAFFIN1:3;
assume A106: (t|--A).ab<=0;
(t|--A).ab>=0 by A7,A86,A102,RLAFFIN1:71;
then for x st x in {ab} holds(t|--A).x=0 by A106,TARSKI:def 1;
then t in conv(A\{ab}) by A7,A86,A102,RLAFFIN1:76;
hence contradiction by A103,A105;
end;
A107: BUU.t=1/card U by A102,RLAFFIN2:18;
then t in Carrier BUU by A102;
then consider n be set such that
A108: n in dom G and
A109: G.n=t by A92,FUNCT_1:def 5;
reconsider n as Nat by A108;
F.n=BUU.t*(t|--A).ab by A93,A94,A108,A109;
then 00 by A85,A89,A90,RLAFFIN1:def 7;
Carrier(B.U|--BB)c=BB by RLVECT_2:def 8;
then A111: not ab in Carrier(B.U|--BB) by A83,A87,XBOOLE_0:def 5;
conv BB c=Affin BB by RLAFFIN1:65;
then B.U|--A=B.U|--BB by A7,A81,A101,RLAFFIN1:77;
hence contradiction by A111,A110;
end;
then conv@U c=conv B1 by CONVEX1:30;
then conv@U misses Int A by A79,RLAFFIN2:7,XBOOLE_1:63;
then card XX=1 by A4,A44;
then consider w1 be set such that
A112: XX={w1} by CARD_2:60;
w1 in XX by A112,TARSKI:def 1;
then consider W1 be Simplex of n,K such that
A113: w1=W1 and
A114: U c=W1;
A115: card SS1+Z<=degree K by A3,A16,A27,A30,A33,Th33;
A116: X c={S\/B.:{W1}}
proof
let x;
A117: n+1=degree K+1 by A3,XXREAL_3:def 2;
assume x in X;
then consider W be Simplex of n,BCS K such that
A118: x=W and
A119: S c=W by A11;
consider T be simplex-like finite Subset-Family of K such that
A120: T misses SS1 and
A121: T\/SS1 is c=-linear with_non-empty_elements and
A122: card T=Z+1 and
A123: @W=B.:SS1\/B.:T by A16,A36,A88,A115,A119,Th41;
consider t be set such that
A124: T={t} by A122,CARD_2:60;
set TS=T\/SS1;
A125: card TS=n+1 by A16,A36,A120,A122,CARD_2:53;
A126: union TS in TS by A121,A124,SIMPLEX0:9;
TS is simplex-like by TOPS_2:20;
then reconsider UTS=union TS as Simplex of K by A126,TOPS_2:def 1;
card TS c=card UTS by A121,SIMPLEX0:10;
then A127: card TS<=card UTS by NAT_1:40;
UTS in T
proof
assume not UTS in T;
then UTS in SS1 by A126,XBOOLE_0:def 3;
then card UTS<=card U by NAT_1:44,ZFMISC_1:92;
hence contradiction by A43,A125,A127,NAT_1:13;
end;
then A128: UTS=t by A124,TARSKI:def 1;
card UTS<=degree K+1 by SIMPLEX0:24;
then card UTS<=n+1 by A3,XXREAL_3:def 2;
then card UTS=n+1 & SS1 c= TS by A125,A127,XXREAL_0:1,XBOOLE_1:7;
then U c= UTS & UTS is Simplex of n,K by A3,A117,SIMPLEX0:def 18,
ZFMISC_1:95;
then UTS in XX;
then W=B.:SS1\/B.:{W1} by A112,A113,A123,A124,A128,TARSKI:def 1;
hence thesis by A35,A118,TARSKI:def 1;
end;
card W1=degree K+1 by A3,SIMPLEX0:def 18;
then card W1=n+1 by A3,XXREAL_3:def 2;
then {W where W is Simplex of n,BCS K:S c=W & conv@W c=conv@W1}={S\/B.:{W1
}} by A16,A27,A30,A33,A36,A43,A114,Th42;
then S\/B.:{W1} in {W where W is Simplex of n,BCS K:S c=W & conv@W c=conv@
W1} by TARSKI:def 1;
then ex R be Simplex of n,BCS K st R=S\/B.:{W1} & S c=R & conv@R c=conv@W1
;
then S\/B.:{W1} in X by A11;
then X={S\/B.:{W1}} by A116,ZFMISC_1:39;
hence card X=1 by CARD_1:50;
end;
suppose A129: card U=n+1;
A130: conv@S meets Int A
proof
U is non empty by A129;
then @U in dom B by A31,ZFMISC_1:64;
then A131: S c=conv@S & B.U in @S by A35,A38,FUNCT_1:def 12,RLAFFIN1:2;
then B.U in conv@S;
then A132: B.U in conv@U by A42;
set BUU=B.U|--@U;
assume A133: conv@S misses Int A;
conv@S c=conv A & A is non empty by A2,A41,A42,XBOOLE_1:1;
then consider BB be Subset of V such that
A134: BB c=0 by A7,A140,RLAFFIN1:71;
BUU.(G.i)=1/card U by A145,A149,A153,RLAFFIN2:18;
hence 0<=F.i by A152,A154;
end;
B.U in conv@S by A131;
then A155: B.U in conv BB by A135;
assume not U c=conv B1;
then consider t be set such that
A156: t in U and
A157: not t in conv B1 by TARSKI:def 3;
U c=conv@U by RLAFFIN1:2;
then A158: t in conv@U by A156;
A159: (t|--A).ab>0
proof
assume A160: (t|--A).ab<=0;
(t|--A).ab>=0 by A7,A41,A158,RLAFFIN1:71;
then for y st y in A\B1 holds(t|--A).y=0 by A139,A160,TARSKI:def 1;
hence contradiction by A7,A41,A139,A148,A157,A158,RLAFFIN1:76;
end;
A161: BUU.t=1/card U by A156,RLAFFIN2:18;
then t in Carrier BUU by A156;
then consider n be set such that
A162: n in dom G and
A163: G.n=t by A145,FUNCT_1:def 5;
reconsider n as Nat by A162;
F.n=BUU.t*(t|--A).ab by A146,A147,A162,A163;
then 00 by A132,A142,A143,RLAFFIN1:def 7;
Carrier(B.U|--BB)c=BB by RLVECT_2:def 8;
then A165: not ab in Carrier(B.U|--BB) by A139,A141,XBOOLE_0:def 5;
conv BB c=Affin BB by RLAFFIN1:65;
then B.U|--A=B.U|--BB by A7,A136,A155,RLAFFIN1:77;
hence contradiction by A165,A164;
end;
then conv@U c=conv B1 by CONVEX1:30;
then Affin@U c=Affin B1 by RLAFFIN1:68;
hence contradiction by A129,A138,RLAFFIN1:79;
end;
set XX={S1 where S1 is Simplex of n,BCS K:S c=S1 & conv@S1 c=conv@U};
A166: card XX=2 by A16,A30,A35,A36,A129,Th43;
then XX is finite;
then consider w1,w2 be set such that
w1<>w2 and
A167: XX={w1,w2} by A166,CARD_2:79;
w2 in XX by A167,TARSKI:def 2;
then consider W2 be Simplex of n,BCS K such that
A168: w2=W2 and
A169: S c=W2 and
conv@W2 c=conv@U;
w1 in XX by A167,TARSKI:def 2;
then consider W1 be Simplex of n,BCS K such that
A170: w1=W1 and
A171: S c=W1 and
conv@W1 c=conv@U;
A172: W1 in X by A11,A171;
A173: X c=XX
proof
let w be set;
assume w in X;
then consider W be Simplex of n,BCS K such that
A174: w=W and
A175: S c=W by A11;
card SS1+Z<=degree K by A3,A16,A27,A30,A33,Th33;
then consider T be simplex-like finite Subset-Family of K such that
T misses SS1 and
A176: T\/SS1 is c=-linear with_non-empty_elements and
card T=Z+1 and
A177: @W=B.:SS1\/B.:T by A27,A30,A33,A34,A175,Th41;
reconsider TS=T\/SS1 as finite simplex-like Subset-Family of K by TOPS_2:
20;
A178: W=B.:@TS by A177,RELAT_1:153;
union TS in TS by A37,A176,SIMPLEX0:9;
then reconsider UTS=union TS as Simplex of K by TOPS_2:def 1;
card UTS<=degree K+1 by SIMPLEX0:24;
then A179: card UTS<=n+1 by A3,XXREAL_3:def 2;
A180: U c=union TS by XBOOLE_1:7,ZFMISC_1:95;
then n+1<=card UTS by A129,NAT_1:44;
then UTS=U by A129,A179,A180,CARD_FIN:1,XXREAL_0:1;
then conv@W c=conv@U by A178,CONVEX1:30,RLAFFIN2:17;
hence thesis by A174,A175;
end;
W2 in X by A11,A169;
then XX c=X by A167,A170,A168,A172,ZFMISC_1:38;
hence thesis by A130,A166,A173,XBOOLE_0:def 10;
end;
end;
end;
theorem Th45:
for S be Simplex of n-1,BCS(k,Complex_of{Aff}) st card Aff = n+1 &
X = {S1 where S1 is Simplex of n,BCS(k,Complex_of{Aff}): S c= S1}
holds (conv @S meets Int Aff implies card X = 2) &
(conv @S misses Int Aff implies card X = 1)
proof
let S be Simplex of n-1,BCS(k,Complex_of{Aff}) such that
A1: card Aff=n+1;
set C=Complex_of{Aff};
reconsider cA=card Aff as ext-real number;
A2: cA-1=card Aff+-1 by XXREAL_3:def 2
.=n by A1;
then A3: degree C=n by SIMPLEX0:26;
defpred P[Nat] means
for S be Simplex of n-1,BCS($1,C),X be set st
X={S1 where S1 is Simplex of n,BCS($1,C):S c=S1} holds
(conv@S meets Int Aff implies card X=2) &
(conv@S misses Int Aff implies card X=1);
A4: [#]C=[#]V & |.C.|c=[#]V;
A5: P[0 qua Nat]
proof
reconsider n1=n-1 as ext-real number;
A6: the topology of C=bool Aff by SIMPLEX0:4;
Aff in bool Aff by ZFMISC_1:def 1;
then reconsider A1=Aff as finite Simplex of C by A6,PRE_TOPC:def 5;
A7: BCS(0,C)=C by A4,Th16;
let S be Simplex of n-1,BCS(0,C),X be set such that
A8: X={S1 where S1 is Simplex of n,BCS(0,C):S c=S1};
A9: X c={Aff}
proof
let x;
reconsider N=n as ext-real number;
assume x in X;
then consider U be Simplex of n,C such that
A10: x=U and
S c=U by A7,A8;
A11: U in the topology of C by PRE_TOPC:def 5;
card U=N+1 by A3,SIMPLEX0:def 18
.=n+1 by XXREAL_3:def 2;
then Aff=U by A1,A6,A11,CARD_FIN:1;
hence thesis by A10,TARSKI:def 1;
end;
A12: S in bool Aff by A6,A7,PRE_TOPC:def 5;
A1 is Simplex of n,C by A2,SIMPLEX0:48;
then Aff in X by A7,A8,A12;
then A13: X={Aff} by A9,ZFMISC_1:39;
n+-1>=-1 & n-1<=degree C by A3,XREAL_1:33,148;
then card S=n1+1 by A7,SIMPLEX0:def 18
.=n-1+1 by XXREAL_3:def 2;
then S<>Aff by A1;
then S c0;
then A22: BCS(k,CA)=CA by A11,A21,Th16,Th22;
then A23: dom F=Vertices CA by A4,FUNCT_2:def 1;
take 0;
A in bool A by ZFMISC_1:def 1;
then reconsider A1=A as Simplex of CA by A16,PRE_TOPC:def 5;
A24: A1 is Simplex of 0,CA by A3,A19,A20,SIMPLEX0:48;
ex x st A={x} by A3,A19,CARD_2:60;
then A25: A={a} by A4,TARSKI:def 1;
then conv A=A by RLAFFIN1:1;
then F.a in A by A4,A9,A17,A22;
then A26: F.a=a by A25,TARSKI:def 1;
A27: XX c={A}
proof
let x;
assume x in XX;
then consider S be Simplex of 0,CA such that
A28: x=S and
F.:S=A by A3,A19,A22;
A29: S in the topology of CA by PRE_TOPC:def 5;
card S=Z+1 by A21,SIMPLEX0:def 18
.=1 by XXREAL_3:4;
then S=A by A3,A16,A19,A29,CARD_FIN:1;
hence thesis by A28,TARSKI:def 1;
end;
F.:A=Im(F,a) by A25,RELAT_1:def 16
.=A by A4,A17,A23,A25,A26,FUNCT_1:117;
then A in XX by A3,A19,A24,A22;
then XX={A} by A27,ZFMISC_1:39;
hence thesis by CARD_1:50;
end;
suppose A30: m>0;
defpred P[set,set] means
$1c=$2;
set XXA={S where S is Simplex of m-1,BCS(k,CA):F.:S=Aa & conv@S misses Int
A};
reconsider m1=m-1 as ext-real number;
reconsider M=m as ext-real number;
reconsider cA=card A as ext-real number;
set YA={S where S is Simplex of m,BCS(k,CA):Aa=F.:S};
A31: YA c=the topology of BCS(k,CA)
proof
let x;
assume x in YA;
then ex S be Simplex of m,BCS(k,CA) st S=x & Aa=F.:S;
hence thesis by PRE_TOPC:def 5;
end;
then reconsider YA as Subset-Family of BCS(k,CA) by XBOOLE_1:1;
reconsider YA as simplex-like Subset-Family of BCS(k,CA) by A31,SIMPLEX0:
14;
defpred P1[set,set] means
$2c=$1;
set Xm1={S where S is Simplex of m-1,BCS(k,CA):Aa=F.:S};
set Xm={S where S is Simplex of m,BCS(k,CA):not contradiction};
consider R1 be Relation such that
A32: for x,y holds[x,y] in R1 iff x in Xm & y in Xm1 & P1[x,y] from
RELAT_1:sch 1;
set DY=dom R1\YA;
A33: DY c=XX
proof
let x;
assume A34: x in DY;
then consider y such that
A35: [x,y] in R1 by RELAT_1:def 4;
x in Xm by A32,A35;
then consider S be Simplex of m,BCS(k,CA) such that
A36: x=S and
not contradiction;
not x in YA by A34,XBOOLE_0:def 5;
then A37: F.:S<>Aa by A36;
y in Xm1 by A32,A35;
then A38: ex W be Simplex of m-1,BCS(k,CA) st y=W & Aa=F.:W;
y c=x by A32,A35;
then Aa c=F.:S by A36,A38,RELAT_1:156;
then Aa c{};
then consider xy be set such that
A41: xy in RDY|(dom RDY\DY) by XBOOLE_0:def 1;
consider x,y such that
A42: xy=[x,y] by A41,RELAT_1:def 1;
A43: x in dom RDY\DY by A41,A42,RELAT_1:def 11;
then dom RDY c=DY & x in dom RDY by RELAT_1:87;
hence contradiction by A43,XBOOLE_0:def 5;
end;
A44: 2*`card YA=card 2*`card card YA by Lm1
.=card(2*card YA) by CARD_2:52;
A45: 2*card YA in NAT by ORDINAL1:def 13;
cA-1=m+1+-1 by A3,XXREAL_3:def 2;
then A46: degree CA=m by SIMPLEX0:26;
consider R be Relation such that
A47: for x,y holds[x,y] in R iff x in Xm1 & y in Xm & P[x,y] from RELAT_1:
sch 1;
A48: card R=card R1
proof
deffunc F(set)=[$1`2,$1`1];
A49: for x st x in R holds F(x) in R1
proof
let z be set;
assume A50: z in R;
then ex x,y st z=[x,y] by RELAT_1:def 1;
then A51: z=[z`1,z`2] by MCART_1:8;
then A52: z`2 in Xm by A47,A50;
(P[z`1,z`2]) & z`1 in Xm1 by A47,A50,A51;
hence thesis by A32,A52;
end;
consider f be Function of R,R1 such that
A53: for x st x in R holds f.x=F(x) from FUNCT_2:sch 2(A49);
per cases;
suppose A54: R1 is empty;
R is empty
proof
assume R is non empty;
then ex x st x in R by XBOOLE_0:def 1;
hence thesis by A49,A54;
end;
hence thesis by A54;
end;
suppose R1 is non empty;
then A55: dom f=R by FUNCT_2:def 1;
R1 c=rng f
proof
let z be set;
assume A56: z in R1;
then ex x,y st z=[x,y] by RELAT_1:def 1;
then A57: z=[z`1,z`2] by MCART_1:8;
then A58: z`2 in Xm1 by A32,A56;
(P1[z`1,z`2]) & z`1 in Xm by A32,A56,A57;
then A59: [z`2,z`1] in R by A47,A58;
[z`2,z`1]`1=z`2 by MCART_1:7;
then F([z`2,z`1])=z by A57,MCART_1:7;
then z=f.([z`2,z`1]) by A53,A59;
hence thesis by A55,A59,FUNCT_1:def 5;
end;
then A60: rng f=R1 by XBOOLE_0:def 10;
now let x1,x2 be set such that
A61: x1 in R and
A62: x2 in R and
A63: f.x1=f.x2;
f.x1=F(x1) & f.x2=F(x2) by A53,A61,A62;
then A64: x1`2=x2`2 & x1`1=x2`1 by A63,ZFMISC_1:33;
A65: ex x,y st x2=[x,y] by A62,RELAT_1:def 1;
ex x,y st x1=[x,y] by A61,RELAT_1:def 1;
hence x1=[x2`1,x2`2] by A64,MCART_1:8
.=x2 by A65,MCART_1:8;
end;
then f is one-to-one by A55,FUNCT_1:def 8;
then R,R1 are_equipotent by A55,A60,WELLORD2:def 4;
hence thesis by CARD_1:21;
end;
end;
A66: |.BCS(k,CAa).|=|.CAa.| & |.CAa.|=conv Aa by Th8,Th10;
set DX=dom R\XXA;
A67: DX c=the topology of BCS(k,CA)
proof
let x;
assume x in DX;
then ex y st[x,y] in R by RELAT_1:def 4;
then x in Xm1 by A47;
then ex S be Simplex of m-1,BCS(k,CA) st S=x & Aa=F.:S;
hence thesis by PRE_TOPC:def 5;
end;
set RDX=R|DX;
reconsider DX as Subset-Family of BCS(k,CA) by A67,XBOOLE_1:1;
reconsider DX as simplex-like Subset-Family of BCS(k,CA) by A67,SIMPLEX0:
14;
A68: RDX|(dom RDX\DX)={}
proof
assume RDX|(dom RDX\DX)<>{};
then consider xy be set such that
A69: xy in RDX|(dom RDX\DX) by XBOOLE_0:def 1;
consider x,y such that
A70: xy=[x,y] by A69,RELAT_1:def 1;
A71: x in dom RDX\DX by A69,A70,RELAT_1:def 11;
then dom RDX c=DX & x in dom RDX by RELAT_1:87;
hence contradiction by A71,XBOOLE_0:def 5;
end;
A72: m1+1=m-1+1 by XXREAL_3:def 2
.=m;
set FA=F|Vertices BCS(k,CAa);
A73: dom FA=Vertices BCS(k,CAa) by A18,A14,RELAT_1:91,SIMPLEX0:31;
A74: Vertices BCS(k,CAa) is non empty by A5,A6,A8,A30;
A75: for v be Vertex of BCS(k,CAa)for B be Subset of V st B c=Aa & v in
conv B holds FA.v in B
proof
let v be Vertex of BCS(k,CAa);
let B be Subset of V;
assume A76: B c=Aa & v in conv B;
v in Vertices BCS(k,CAa) by A74;
then F.v in B by A9,A12,A15,A76,XBOOLE_1:1;
hence thesis by A73,A74,FUNCT_1:70;
end;
rng FA c=Aa
proof
let y;
assume y in rng FA;
then consider x such that
A77: x in dom FA and
A78: FA.x=y by FUNCT_1:def 5;
reconsider v=x as Element of BCS(k,CAa) by A73,A77;
v is vertex-like by A73,A77,SIMPLEX0:def 4;
then consider S be Subset of BCS(k,CAa) such that
A79: S is simplex-like and
A80: v in S by SIMPLEX0:def 3;
A81: conv@S c=|.BCS(k,CAa).| by A79,Th5;
S c=conv@S by RLAFFIN1:2;
then A82: v in conv@S by A80;
x in Vertices BCS(k,CAa) by A18,A14,A77,RELAT_1:91,SIMPLEX0:31;
hence thesis by A66,A75,A78,A81,A82;
end;
then reconsider FA as Function of Vertices BCS(k,CAa),Aa by A73,FUNCT_2:
4;
set XXa={S where S is Simplex of m-1,BCS(k,CAa):FA.:S=Aa};
consider n such that
A83: card XXa=2*n+1 by A2,A5,A75;
A84: m-1<=m-0 & -1<=m+-1 by XREAL_1:12,33;
A85: for x st x in XXA holds card Im(R,x)=1
proof
let x;
assume x in XXA;
then consider S be Simplex of m-1,BCS(k,CA) such that
A86: x=S and
A87: F.:S=Aa and
A88: conv@S misses Int A;
set XX={S1 where S1 is Simplex of m,BCS(k,CA):S c=S1};
A89: R.:{S}c=XX
proof
let w be set;
assume w in R.:{S};
then consider s be set such that
A90: [s,w] in R and
A91: s in {S} by RELAT_1:def 13;
w in Xm by A47,A90;
then A92: ex W be Simplex of m,BCS(k,CA) st w=W & not contradiction;
s=S & s c=w by A47,A90,A91,TARSKI:def 1;
hence thesis by A92;
end;
XX c=R.:{S}
proof
let w be set;
assume w in XX;
then consider W be Simplex of m,BCS(k,CA) such that
A93: w=W and
A94: S c=W;
W in Xm & S in Xm1 by A87;
then S in {S} & [S,W] in R by A47,A94,TARSKI:def 1;
hence thesis by A93,RELAT_1:def 13;
end;
then A95: R.:{S}=XX by A89,XBOOLE_0:def 10;
card XX=1 by A3,A88,Th45;
hence thesis by A86,A95,RELAT_1:def 16;
end;
A96: degree CA=degree BCS(k,CA) by A11,Th32;
A97: M+1=m+1 by XXREAL_3:def 2;
A98: for x st x in YA holds card Im(R1,x)=2
proof
let x;
assume x in YA;
then consider S be Simplex of m,BCS(k,CA) such that
A99: x=S and
A100: Aa=F.:S;
set FS=F|S;
A101: rng FS=Aa by A100,RELAT_1:148;
A102: Aa is non empty by A5,A30;
A103: S in {x} by A99,TARSKI:def 1;
A104: dom FS=S by A18,RELAT_1:91,SIMPLEX0:17;
A105: card S=m+1 by A96,A46,A97,SIMPLEX0:def 18;
reconsider FS as Function of S,Aa by A101,A104,FUNCT_2:3;
FS is onto by A101,FUNCT_2:def 3;
then consider b be set such that
A106: b in Aa and
A107: card(FS"{b})=2 and
A108: for x st x in Aa & x<>b holds card(FS"{x})=1 by A5,A102,A105,Th2;
consider a1,a2 be set such that
A109: a1<>a2 and
A110: FS"{b}={a1,a2} by A107,CARD_2:79;
reconsider S1=S\{a1},S2=S\{a2} as Simplex of BCS(k,CA);
A111: a1 in {a1,a2} by TARSKI:def 2;
then A112: a1 in S2 by A109,A110,ZFMISC_1:64;
A113: card S1=m by A105,A110,A111,STIRL2_1:65;
A114: a2 in {a1,a2} by TARSKI:def 2;
then A115: card S2=m by A105,A110,STIRL2_1:65;
then reconsider S1,S2 as Simplex of m-1,BCS(k,CA) by A96,A84,A72,A46,
A113,SIMPLEX0:def 18;
A116: {a1}c=S by A110,A111,ZFMISC_1:37;
A117: FS.a2=F.a2 by A104,A110,A114,FUNCT_1:70;
A118: {a2}c=S by A110,A114,ZFMISC_1:37;
A119: R1.:{x}c={S1,S2}
proof
let Y be set;
assume Y in R1.:{x};
then consider X be set such that
A120: [X,Y] in R1 and
A121: X in {x} by RELAT_1:def 13;
Y in Xm1 by A32,A120;
then consider W be Simplex of m-1,BCS(k,CA) such that
A122: Y=W and
A123: Aa=F.:W;
X=x by A121,TARSKI:def 1;
then W c=S by A32,A99,A120,A122;
then A124: Aa=FS.:W by A123,RELAT_1:162;
then consider w be set such that
A125: w in dom FS and
A126: w in W and
A127: FS.w=b by A106,FUNCT_1:def 12;
A128: {w}c=W by A126,ZFMISC_1:37;
A129: S\{a1,a2}c=W
proof
let s be set;
assume A130: s in S\{a1,a2};
then A131: s in dom FS by A104,XBOOLE_0:def 5;
then A132: FS.s in Aa by A101,FUNCT_1:def 5;
then consider w be set such that
A133: w in dom FS and
A134: w in W and
A135: FS.w=FS.s by A124,FUNCT_1:def 12;
not s in FS"{b} by A110,A130,XBOOLE_0:def 5;
then not FS.s in {b} by A131,FUNCT_1:def 13;
then FS.s<>b by TARSKI:def 1;
then card(FS"{FS.s})=1 by A108,A132;
then consider z be set such that
A136: FS"{FS.s}={z} by CARD_2:60;
A137: FS.s in {FS.s} by TARSKI:def 1;
then A138: s in FS"{FS.s} by A131,FUNCT_1:def 13;
w in FS"{FS.s} by A133,A135,A137,FUNCT_1:def 13;
then w=z by A136,TARSKI:def 1;
hence thesis by A134,A136,A138,TARSKI:def 1;
end;
b in {b} by TARSKI:def 1;
then A139: w in FS"{b} by A125,A127,FUNCT_1:def 13;
A140: card W=m by A96,A84,A72,A46,SIMPLEX0:def 18;
A141: S/\{a1}={a1} by A116,XBOOLE_1:28;
A142: S/\{a2}={a2} by A118,XBOOLE_1:28;
per cases by A110,A139,TARSKI:def 2;
suppose w=a1;
then (S\{a1,a2})\/{w}=S\({a1,a2}\{a1}) by A141,XBOOLE_1:52
.=S2 by A109,ZFMISC_1:23;
then S2=W by A115,A128,A129,A140,CARD_FIN:1,XBOOLE_1:8;
hence thesis by A122,TARSKI:def 2;
end;
suppose w=a2;
then (S\{a1,a2})\/{w}=S\({a1,a2}\{a2}) by A142,XBOOLE_1:52
.=S1 by A109,ZFMISC_1:23;
then S1=W by A113,A128,A129,A140,CARD_FIN:1,XBOOLE_1:8;
hence thesis by A122,TARSKI:def 2;
end;
end;
A143: S c=dom F by A18,SIMPLEX0:17;
A144: FS.a1=F.a1 by A104,A110,A111,FUNCT_1:70;
A145: FS.a1 in {b} by A110,A111,FUNCT_1:def 13;
then A146: FS.a1=b by TARSKI:def 1;
A147: FS.a2 in {b} by A110,A114,FUNCT_1:def 13;
then A148: FS.a2=b by TARSKI:def 1;
A149: a2 in S & a2 in S1 by A109,A110,A114,ZFMISC_1:64;
A150: Aa c=F.:S1
proof
let z be set;
assume A151: z in Aa;
per cases;
suppose A152: z=b;
FS.a2 in F.:S1 by A143,A117,A149,FUNCT_1:def 12;
hence thesis by A147,A152,TARSKI:def 1;
end;
suppose A153: z<>b;
consider c be set such that
A154: c in dom F and
A155: c in S and
A156: z=F.c by A100,A151,FUNCT_1:def 12;
c in S1 by A144,A146,A153,A155,A156,ZFMISC_1:64;
hence thesis by A154,A156,FUNCT_1:def 12;
end;
end;
A157: S in Xm;
A158: a1 in S & a1 in S2 by A109,A110,A111,ZFMISC_1:64;
A159: Aa c=F.:S2
proof
let z be set;
assume A160: z in Aa;
per cases;
suppose A161: z=b;
FS.a1 in F.:S2 by A144,A143,A158,FUNCT_1:def 12;
hence thesis by A145,A161,TARSKI:def 1;
end;
suppose A162: z<>b;
consider c be set such that
A163: c in dom F and
A164: c in S and
A165: z=F.c by A100,A160,FUNCT_1:def 12;
c in S2 by A117,A148,A162,A164,A165,ZFMISC_1:64;
hence thesis by A163,A165,FUNCT_1:def 12;
end;
end;
F.:S1 c=Aa by A100,RELAT_1:156,XBOOLE_1:36;
then Aa=F.:S1 by A150,XBOOLE_0:def 10;
then S\{a1}c=S & S1 in Xm1 by XBOOLE_1:36;
then [S,S1] in R1 by A32,A157;
then A166: S1 in R1.:{x} by A103,RELAT_1:def 13;
F.:S2 c=Aa by A100,RELAT_1:156,XBOOLE_1:36;
then Aa=F.:S2 by A159,XBOOLE_0:def 10;
then S\{a2}c=S & S2 in Xm1 by XBOOLE_1:36;
then [S,S2] in R1 by A32,A157;
then S2 in R1.:{x} by A103,RELAT_1:def 13;
then {S1,S2}c=R1.:{x} by A166,ZFMISC_1:38;
then A167: R1.:{x}={S1,S2} by A119,XBOOLE_0:def 10;
S1<>S2 by A112,ZFMISC_1:64;
then card(R1.:{x})=2 by A167,CARD_2:76;
hence thesis by RELAT_1:def 16;
end;
A168: M-1=m+-1 by XXREAL_3:def 2;
XX c=DY
proof
let x;
assume x in XX;
then consider S be Simplex of m,BCS(k,CA) such that
A169: x=S and
A170: F.:S=A by A3;
set FS=F|S;
A171: rng FS=A by A170,RELAT_1:148;
A172: card A=card S by A3,A96,A46,A97,SIMPLEX0:def 18;
A173: dom FS=S by A18,RELAT_1:91,SIMPLEX0:17;
then reconsider FS as Function of S,A by A171,FUNCT_2:3;
consider s be set such that
A174: s in dom FS & FS.s=a by A4,A171,FUNCT_1:def 5;
set Ss=S\{s};
FS is onto by A171,FUNCT_2:def 3;
then A175: FS is one-to-one by A172,STIRL2_1:70;
then A176: FS.:Ss=FS.:S\FS.:{s} by FUNCT_1:123
.=A\FS.:{s} by A171,A173,RELAT_1:146
.=A\Im(FS,s) by RELAT_1:def 16
.=Aa by A174,FUNCT_1:117;
Ss,FS.:Ss are_equipotent by A173,A175,CARD_1:60,XBOOLE_1:36;
then A177: card Ss=m by A5,A176,CARD_1:21;
reconsider Ss as Simplex of BCS(k,CA);
reconsider Ss as Simplex of m-1,BCS(k,CA) by A168,A177,SIMPLEX0:48;
FS.:Ss=F.:Ss by RELAT_1:162,XBOOLE_1:36;
then A178: Ss in Xm1 by A176;
Ss c=S & S in Xm by XBOOLE_1:36;
then [S,Ss] in R1 by A32,A178;
then A179: S in dom R1 by RELAT_1:def 4;
for W be Simplex of m,BCS(k,CA) st S=W holds Aa<>F.:W by A4,A170,ZFMISC_1
:64;
then not S in YA;
hence thesis by A169,A179,XBOOLE_0:def 5;
end;
then A180: DY=XX by A33,XBOOLE_0:def 10;
for x st x in DY holds card Im(RDY,x)=1
proof
let x;
assume A181: x in DY;
then consider y such that
A182: [x,y] in R1 by RELAT_1:def 4;
A183: ex W be Simplex of m,BCS(k,CA) st x=W & F.:W=A by A3,A180,A181;
x in Xm by A32,A182;
then consider S be Simplex of m,BCS(k,CA) such that
A184: x=S and
not contradiction;
y in Xm1 by A32,A182;
then consider W be Simplex of m-1,BCS(k,CA) such that
A185: y=W and
A186: Aa=F.:W;
A187: card S=m+1 by A96,A46,A97,SIMPLEX0:def 18;
A188: RDY.:{x}c={y}
proof
let u be set;
set FS=F|S;
assume u in RDY.:{x};
then consider s be set such that
A189: [s,u] in RDY and
A190: s in {x} by RELAT_1:def 13;
A191: [s,u] in R1 by A189,RELAT_1:def 11;
then u in Xm1 by A32;
then consider U be Simplex of m-1,BCS(k,CA) such that
A192: u=U and
A193: Aa=F.:U;
A194: dom FS=S by A18,RELAT_1:91,SIMPLEX0:17;
A195: rng FS=A by A183,A184,RELAT_1:148;
then reconsider FS as Function of S,A by A194,FUNCT_2:3;
A196: W c=S by A32,A182,A184,A185;
then A197: FS.:W=F.:W by RELAT_1:162;
s=S by A184,A190,TARSKI:def 1;
then A198: U c=S by A32,A191,A192;
then A199: FS.:U=F.:U by RELAT_1:162;
FS is onto by A195,FUNCT_2:def 3;
then A200: FS is one-to-one by A3,A187,STIRL2_1:70;
then A201: U c=W by A186,A193,A194,A197,A198,A199,FUNCT_1:157;
W c=U by A186,A193,A194,A196,A197,A199,A200,FUNCT_1:157;
then u=y by A185,A192,A201,XBOOLE_0:def 10;
hence thesis by TARSKI:def 1;
end;
x in {x} & [x,y] in RDY by A181,A182,RELAT_1:def 11,TARSKI:def 1;
then y in RDY.:{x} by RELAT_1:def 13;
then RDY.:{x}={y} by A188,ZFMISC_1:39;
then Im(RDY,x)={y} by RELAT_1:def 16;
hence thesis by CARD_1:50;
end;
then card RDY=card{}+`1*`card DY by A40,Th1
.=1*`card DY by CARD_2:29
.=card DY by CARD_2:33;
then A202: card R1=card card XX+`card(2*card YA) by A44,A98,A180,Th1
.=card(card XX+2*card YA) by A45,CARD_2:51
.=card XX+2*card YA by Lm1;
A203: |.BCS(k,CA).|=|.CA.| & |.CA.|=conv A by Th8,Th10;
A204: XXA c=XXa
proof
let x;
assume x in XXA;
then consider S be Simplex of m-1,BCS(k,CA) such that
A205: x=S and
A206: F.:S=Aa and
A207: conv@S misses Int A;
A208: dom(F|S)=S by A18,RELAT_1:91,SIMPLEX0:17;
conv@S c=conv A by A203,Th5;
then consider B be Subset of V such that
A209: B cAa by A3,A5;
then A226: Aa c=-1 by INT_1:20;
then card DX+n-card YA>=(-1)/2 by XREAL_1:81;
then card DX+n-card YA>-1 by XXREAL_0:2;
then card DX+n-card YA>=0 by INT_1:21;
then reconsider cnc=card DX+n-card YA as Element of NAT by INT_1:16;
take cnc;
thus thesis by A48,A202,A245;
end;
end;
A246: P[0 qua Nat]
proof
let A be finite affinely-independent Subset of V such that
A247: card A=0;
A248: A={} by A247;
set C=Complex_of{A};
A249: |.C.|c=[#]V & [#]C=[#]V;
let F be Function of Vertices BCS(k,C),A such that
for v be Vertex of BCS(k,C)for B be Subset of V st B c=A & v in conv B
holds F.v in B;
set X={S where S is Simplex of card A-1,BCS(k,C):F.:S=A};
take 0;
A250: k=0 or k>0;
A251: Z-1=-1 by XXREAL_3:4;
then degree C=-1 by A247,SIMPLEX0:26;
then A252: C=BCS(k,C) by A249,A250,Th16,Th22;
A253: the topology of C=bool A by SIMPLEX0:4;
A254: X c={A}
proof
let x such that
A255: x in X;
consider S be Simplex of card A-1,BCS(k,C) such that
A256: S=x and
F.:S=A by A255;
S in the topology of C by A252,PRE_TOPC:def 5;
then S is empty by A248,A253;
hence thesis by A248,A256,TARSKI:def 1;
end;
A in bool A by ZFMISC_1:def 1;
then reconsider A1=A as Simplex of C by A253,PRE_TOPC:def 5;
A257: F.:A1=A by A248;
A1 is Simplex of-1,C by A247,A251,SIMPLEX0:48;
then A in X by A247,A252,A257;
then X={A} by A254,ZFMISC_1:39;
hence thesis by CARD_1:50;
end;
for k holds P[k] from NAT_1:sch 2(A246,A1);
hence thesis;
end;
:: Sperner's Lemma
theorem
for F st for v,B st B c= Aff & v in conv B holds F.v in B
ex S be Simplex of card Aff-1,BCS(k,Complex_of{Aff}) st F.:S = Aff
proof
let F be Function of Vertices BCS(k,Complex_of{Aff}),Aff;
set XX={S where S is Simplex of card Aff-1,BCS(k,Complex_of{Aff}):F.:S=Aff};
assume for v being Vertex of BCS(k,Complex_of{Aff})for B st B c=Aff & v in
conv B holds F.v in B;
then ex n st card XX=2*n+1 by Th46;
then XX is non empty;
then consider x such that
A1: x in XX by XBOOLE_0:def 1;
ex S be Simplex of card Aff-1,BCS(k,Complex_of{Aff}) st x=S & F.:S=Aff by A1
;
hence thesis;
end;
__