:: Sperner's Lemma
:: by Karol P\c{a}k
::
:: Received February 9, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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, XXREAL_3,
XXREAL_0, XCMPLX_0, XREAL_0, ORDERS_1, CARD_1, REAL_1, FINSET_1,
WELLORD2, 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,
XTUPLE_0, MCART_1, CARD_2, COHSP_1, SIMPLEX0, RLAFFIN2;
constructors BINOP_2, CONVEX1, CONVEX3, REAL_1, RVSUM_1, RLAFFIN1, SIMPLEX0,
TOPS_2, BORSUK_1, COHSP_1, CARD_2, RLAFFIN2, XTUPLE_0;
registrations CARD_1, FINSET_1, FUNCT_1, 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, SETFAM_1, COHSP_1,
RLAFFIN2, RELSET_1, RLVECT_2, ORDINAL1, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions ORDINAL1, SETFAM_1, TARSKI, TOPS_2, XBOOLE_0, FINSET_1;
equalities MATROID0, ORDERS_1, RLVECT_2, STRUCT_0, SIMPLEX0, XXREAL_3,
ORDINAL1;
expansions MATROID0, ORDINAL1, SETFAM_1, SIMPLEX0, TARSKI, TOPS_2, XBOOLE_0;
theorems CARD_1, CARD_2, 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, STIRL2_1, TARSKI, TOPS_2, WELLORD2, XBOOLE_0,
XBOOLE_1, XREAL_1, XXREAL_0, XXREAL_3, ZFMISC_1, RLAFFIN1, RLAFFIN2,
SIMPLEX0, XTUPLE_0, FINSEQ_4;
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 being object 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 being object 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(object)=Im(R,$1);
consider f be Function such that
A3: dom f=X &
for x being object st x in X holds f.x=F(x) from FUNCT_1:sch 3;
defpred P[object,object] means
ex g be Function st g=$2 & dom g=f.$1 & rng g=C & g is one-to-one;
A4: for x being object st x in X ex y being object st P[x,y]
proof
let x be object;
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 2;
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 being object st x in X holds P[x,ff.x] from CLASSES1:sch 1(A4);
now let x be object;
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(object)=[$1`1,(ff.($1`1)).($1`2)];
consider p be Function such that
A7: dom p=R|X &
for x being object st x in R|X holds p.x=G(x) from FUNCT_1:sch 3;
A8: rng p=[:X,C:]
proof
hereby let y be object;
assume y in rng p;
then consider x being object such that
A9: x in dom p and
A10: p.x=y by FUNCT_1:def 3;
A11: p.x=[x`1,(ff.(x`1)).(x`2)] by A7,A9;
A12: x=[x`1,x`2] by A7,A9,MCART_1:21;
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 3;
hence y in [:X,C:] by A10,A11,A14,A15,ZFMISC_1:87;
end;
let y be object;
assume y in [:X,C:];
then consider y1,y2 be object 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 object such that
A24: x2 in dom g and
A25: g.x2=y2 by A19,A23,FUNCT_1:def 3;
A26: G([y1,x2])=y by A20,A21,A25;
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 3;
end;
now let x1,x2 be object 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,XTUPLE_0:1;
A33: x1=[x1`1,x1`2] by A7,A28,MCART_1:21;
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:21;
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,XTUPLE_0:1;
hence x1=x2 by A32,A35,A36,A33,A34,A37,A39,A40,A41,A42,FUNCT_1:def 4;
end;
then p is one-to-one by FUNCT_1:def 4;
then R|X,[:X,C:]are_equipotent by A7,A8,WELLORD2:def 4;
then A43: card(R|X)=card[:X,C:] by CARD_1:5
.=card[:card X,C:] by CARD_2:7
.=C*`card X by CARD_2:def 2;
A44: R|X misses R|DA
proof
assume R|X meets R|DA;
then consider x being object such that
A45: x in R|X and
A46: x in R|DA by XBOOLE_0:3;
consider x1,x2 be object 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:78
.=R;
hence card R=card(R|DA)+`C*`card X by A43,A44,CARD_2:35;
end;
suppose not X c=dom R;
then consider x being object such that
A48: x in X and
A49: not x in dom R;
Im(R,x)={}
proof
assume Im(R,x)<>{};
then consider y being object 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,XTUPLE_0:def 12;
end;
then A51: C=card{} by A1,A48;
dom R misses X
proof
assume dom R meets X;
then consider x being object 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 being object st[x,y] in R by A52,XTUPLE_0:def 12;
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:20;
then card(R|DA)+`C*`card X=card(R|DA) by CARD_2:18;
hence thesis by A55;
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 be object;
set fy=F"{y};
assume A6: y in Y;
then fy<>{} by A3,FUNCT_1:72;
then card fy=1 by A5,A6,NAT_1:25;
hence ex x being object st fy={x} by CARD_2:42;
end;
then f is one-to-one by A3,FUNCT_1:74;
then X,Y are_equipotent by A3,A4,WELLORD2:def 4;
then card X=card Y by CARD_1:5;
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:62,XBOOLE_1:36;
then A10: card dom fD=card XX-card fy by A4,CARD_2:44;
set Yy=Y\{y};
A11: rng fD=Yy by A3,STIRL2_1:54;
then reconsider FD=fD as Function of dom fD,Yy by FUNCT_2:1;
card Y=c1+1;
then A12: card Yy=c1 by A7,STIRL2_1:55;
then Segm c1 c= Segm card dom fD by A11,CARD_1:12;
then card Y+-1<=card Y+(1-card fy) by A1,A10,NAT_1:39;
then -1<=1-card fy by XREAL_1:6;
then card fy<=1--1 by XREAL_1:11;
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:56;
FD is onto by A11,FUNCT_2:def 3;
then FD is one-to-one by A1,A10,A12,A13,FINSEQ_4:63;
then A17: ex z be object st FD"{x}={z} by A16,FUNCT_1:74;
FD"{x}=f"{x} by A15,STIRL2_1:54;
hence thesis by A17,CARD_1:30;
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:67;
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;
then A3: {S}c=the topology of K by ZFMISC_1:31;
set C=Complex_of{@S};
A4: [#]C c=[#]K by A1;
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 be object;
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 be object;
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 be object;
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;
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;
hence thesis by A3,Def3;
end;
theorem Th5:
for A be Subset of Kr st A is simplex-like holds conv @A c= |.Kr.|
by Def3;
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;
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;
then consider x be non empty set such that
A2: x in the topology of Kr;
reconsider X=x as Subset of Kr by A2;
(ex y being object st y in conv@X) & X is simplex-like by A2,XBOOLE_0:def 1
;
hence contradiction by A1,Def3;
end;
assume A3: Kr is empty-membered;
assume|.Kr.| is non empty;
then consider x being object such that
A4: x in |.Kr.|;
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;
then the topology of Kr is with_non-empty_element;
hence contradiction by A3;
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 be object;
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;
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;
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 be object;
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;
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;
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;
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 be object;
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 for 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 be object;
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;
then A in the topology of C by SIMPLEX0:2;
then A4: B is simplex-like;
@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;
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,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 be object;
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 6;
then reconsider Carr1=Carr as Subset of C by XBOOLE_1:1;
S in TOP by A4;
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;
reconsider LC=L as Linear_Combination of Carr by RLVECT_2:def 6;
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;
then A10: B is simplex-like by A1,A3;
@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 for 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:25;
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;
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:56;
A13: B.:{A}=Im(B,A) by RELAT_1:def 16;
then A14: B.:{A}={BA} by A12,FUNCT_1:59;
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:31;
then reconsider BY=B.:{A} as Subset of P by A12,A13,FUNCT_1:59;
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 8,TOPS_2:def 1;
take Y,BY;
conv{BA}={BA} by RLAFFIN1:1;
hence thesis by A14,A15,TARSKI:def 1,ZFMISC_1:25;
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:55;
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;
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 8;
end;
suppose x1 in S & x2 in {A};
then x1 c=union S & x2=A by TARSKI:def 1,ZFMISC_1:74;
then x1 c=x2 by A25;
hence thesis;
end;
suppose x2 in S & x1 in {A};
then x2 c=union S & x1=A by TARSKI:def 1,ZFMISC_1:74;
then x2 c=x1 by A25;
hence thesis;
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 8,TOPS_2:13;
A28: B.:S1=BS\/BY by A21,RELAT_1:120;
then reconsider BS1=B.:S1 as Subset of P;
A29: conv@BS c=conv@BS1 by A28,RLTOPSP1:20,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:78
.=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 be object;
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;
end;
suppose A42: S is non empty;
take U=union S;
A43: A c=conv@U
proof
let x be object;
assume x in A;
then consider y being object such that
A44: y in dom B and
A45: y in S and
A46: B.y=x by A40,FUNCT_1:def 6;
reconsider y as Simplex of K by A45,TOPS_2:def 1;
y<>{} by A44,ZFMISC_1:56;
then A47: B.y in conv@y by A2;
conv@y c=conv@U by A45,RLTOPSP1:20,ZFMISC_1:74;
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 for 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 12;
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 12;
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 ExtReal;
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:35,def 2;
A7: the topology of BC c=the topology of Kv
proof
let x be object;
assume x in the topology of BC;
then reconsider X=x as Simplex of BC by PRE_TOPC:def 2;
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:112;
per cases;
suppose X is empty;
then X1 is simplex-like;
hence thesis;
end;
suppose A10: X is non empty;
then S is non empty by A8;
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 being object such that
A13: y in S/\dom B;
reconsider y as set by TARSKI:1;
y in S by A13,XBOOLE_0:def 4;
then A14: y c=U by ZFMISC_1:74;
y<>{} by A13,ZFMISC_1:56;
hence contradiction by A12,A14;
end;
hence contradiction by A8,A9,A10;
end;
then A15: @U in dom B by A5,ZFMISC_1:56;
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 object such that
A18: {u}=@U by CARD_2:42;
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 be object;
reconsider yy=y as set by TARSKI:1;
assume A20: y in S/\dom B;
then y in S by XBOOLE_0:def 4;
then A21: yy c=U by ZFMISC_1:74;
y<>{} by A20,ZFMISC_1:56;
then y=U by A18,A21,ZFMISC_1:33;
hence thesis by TARSKI:def 1;
end;
S/\dom B is non empty by A8,A9,A10;
then S/\dom B={U} by A19,ZFMISC_1:33;
then X=Im(B,U) by A8,A9,RELAT_1:def 16
.={B.U} by A15,FUNCT_1:59
.={1/1*Sum{u}} by A17,A18,RLAFFIN2:def 2
.={Sum{u}} by RLVECT_1:def 8
.=U by A18,RLVECT_2:9;
hence thesis by PRE_TOPC:def 2;
end;
end;
the topology of Kv c=the topology of BC
proof
let x be object;
assume x in the topology of Kv;
then reconsider X=x as Simplex of Kv by PRE_TOPC:def 2;
reconsider X1=X as Subset of BC by A4;
per cases;
suppose X is empty;
then X1 is simplex-like;
hence thesis;
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;
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 object such that
A28: @X={u} by CARD_2:42;
A29: @X in dom B by A5,A22,ZFMISC_1:56;
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:59
.={1/1*Sum{u}} by A27,A28,RLAFFIN2:def 2
.={Sum{u}} by RLVECT_1:def 8
.=X1 by A28,RLVECT_2:9;
then X1 is simplex-like by A3,A25,SIMPLEX0:def 20;
hence thesis;
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:56;
then A5: dom center_of_mass V is with_non-empty_elements;
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;
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;
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 be object;
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;
reconsider vv={v} as Subset of Kv by A7,ZFMISC_1:31;
{v}c=A by A7,ZFMISC_1:31;
then vv is simplex-like by A6,MATROID0:1;
then A8: vv in the topology of Kv;
card vv=1 & card 1=1 by CARD_1:30;
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 2;
A9: v in vv by TARSKI:def 1;
reconsider v as Element of S;
v is vertex-like by A9;
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;
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 for 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;
let A be Subset of K;
assume A is simplex-like;
then A in the topology of K;
then A is empty by A1;
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;
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 for
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;
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;
then A4: A is empty by A1;
B in the topology of K by A3;
then B is empty by A1;
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;
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;
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 be object;
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 6;
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:20,XBOOLE_1:17;
hence thesis by XBOOLE_1:19;
end;
end;
registration let V;
cluster 1-element affinely-independent for 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 for SimplicialComplex of V;
existence
proof
set v=the Element of V;
take Complex_of{{v}};
thus thesis;
end;
end;
registration
let V;
let K be affinely-independent SimplicialComplexStr of V;
cluster -> affinely-independent for 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;
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;
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 for 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;
then A5: A in the topology of K by A1;
A6: B in the topology of S by A3;
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;
B1 is simplex-like by A1,A6;
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;
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 being object 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;
suppose A/\B c<A;
then conv@(A/\B)misses Int@A by RLAFFIN2:7;
hence contradiction by A4,A7,A9,XBOOLE_0:3;
end;
suppose A/\B c<B;
then conv@(A/\B)misses Int@B by RLAFFIN2:7;
hence contradiction by A4,A8,A9,XBOOLE_0:3;
end;
end;
assume A10: for A,B be Subset of K st A is simplex-like & B is simplex-like &
Int@A meets Int@B holds A=B;
let A,B be Subset of K such that
A11: A is simplex-like and
A12: B is simplex-like;
A13: conv@A/\conv@B c=conv@(A/\B)
proof
let x be object;
A14: the_family_of K is subset-closed;
assume A15: x in conv@A/\conv@B;
then x in conv@A by XBOOLE_0:def 4;
then x in union{Int a where a is Subset of V:a c=@A} by RLAFFIN2:8;
then consider Ia be set such that
A16: x in Ia and
A17: Ia in {Int a where a is Subset of V:a c=@A} by TARSKI:def 4;
consider a be Subset of V such that
A18: Ia=Int a and
A19: a c=@A by A17;
x in conv@B by A15,XBOOLE_0:def 4;
then x in union{Int b where b is Subset of V:b c=@B} by RLAFFIN2:8;
then consider Ib be set such that
A20: x in Ib and
A21: Ib in {Int b where b is Subset of V:b c=@B} by TARSKI:def 4;
consider b be Subset of V such that
A22: Ib=Int b and
A23: b c=@B by A21;
reconsider a1=a,b1=b as Subset of K by A19,A23,XBOOLE_1:1;
A in the topology of K by A11;
then a1 in the topology of K by A14,A19,CLASSES1:def 1;
then A24: a1 is simplex-like;
B in the topology of K by A12;
then b1 in the topology of K by A14,A23,CLASSES1:def 1;
then A25: b1 is simplex-like;
Int@a1 meets Int@b1 by A16,A18,A20,A22,XBOOLE_0:3;
then a1=b1 by A10,A24,A25;
then a c=@(A/\B) by A19,A23,XBOOLE_1:19;
then A26: conv a c=conv@(A/\B) by RLAFFIN1:3;
x in conv a by A16,A18,RLAFFIN2:def 1;
hence thesis by A26;
end;
conv@(A/\B)c=conv@A & conv@(A/\B)c=conv@B by RLAFFIN1:3,XBOOLE_1:17;
then conv@(A/\B)c=conv@A/\conv@B by XBOOLE_1:19;
hence thesis by A13;
end;
reserve Ks for simplex-join-closed SimplicialComplex of V,
As,Bs for Subset of Ks,
Ka for non void affinely-independent SimplicialComplex of V,
Kas for non void affinely-independent simplex-join-closed
SimplicialComplex of V,
K for non void affinely-independent simplex-join-closed total
SimplicialComplex of V;
registration
let V,Ka;
let S be Simplex of Ka;
cluster @S -> 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 being object 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;
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;
then A4: Ks is non void by PENCIL_1:def 4;
per cases;
suppose A5: As is empty;
thus thesis by A5;
end;
suppose As is non empty;
then Int@As is non empty by A1,A2,A4,RLAFFIN2:20;
then consider x being object such that
A6: x in Int@As;
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;
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;
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:67,82;
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 object;
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:47;
dom BT=dom B/\T by RELAT_1:61;
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 2;
A1 is non empty by A1,ZFMISC_1:56;
then A5: B.A1 in conv@A1 by RLAFFIN2:16;
A2 is non empty by A2,ZFMISC_1:56;
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 4;
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:67,82
;
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:67,82
;
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:56;
then A22: B.union S1 in @A1 by A7,A14,A19,FUNCT_1:def 6,ZFMISC_1:2;
then reconsider Bu=B.union S1 as Element of V;
A23: {Bu}c=@A1 by A22,ZFMISC_1:31;
A24: B.union S1 in @A2 by A8,A11,A18,A19,A21,FUNCT_1:def 6,ZFMISC_1:2;
then A25: {Bu}c=@A2 by ZFMISC_1:31;
A26: Bu in {Bu} by ZFMISC_1:31;
A27: conv{Bu}={Bu} by RLAFFIN1:1;
consider x being object 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;
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;
hence thesis by A27,A28,A29,A31,RLAFFIN2:def 1;
end;
suppose A1<>{Bu} & A2<>{Bu};
then {Bu}c<@A1 by A23;
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:11;
A33: S1 c=the topology of Kas
proof
let x be object;
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;
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:67;
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,31;
A37: union s2u c=U by A18,XBOOLE_1:36,ZFMISC_1:77;
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:56;
end;
then A39: union s2u c<U by A37;
then consider xS2U be object such that
A40: xS2U in @U and
A41: not xS2U in union S2U by XBOOLE_0:6;
reconsider xS2U as Element of V by A40;
union S2U c=U\{xS2U} by A37,A41,ZFMISC_1:34;
then A42: conv union S2U c=conv@(U\{xS2U}) by RLAFFIN1:3;
A43: x in conv@A1 by A28,RLAFFIN2:def 1;
then A44: Bu1.Bu<=1 by A3,RLAFFIN1:71;
A45: Bu1.Bu<1
proof
assume Bu1.Bu>=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:19;
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:59
.=B.:{union S1} by RELAT_1:def 16;
then A52: A1\{Bu}=BT.:S1\(B.:{U}) by A33,A7,RELAT_1:129
.=BT.:S1\(BT.:{U}) by A33,A36,RELAT_1:129,XBOOLE_1:1
.=BT.:(S1\{U}) by FUNCT_1:64
.=B.:(S1\{U}) by A35,A33,RELAT_1:129,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<n+1 by A19,A39,CARD_2:48;
then A54: card union s2u<=n by NAT_1:13;
A55: union s1u c=U by XBOOLE_1:36,ZFMISC_1:77;
A56: x in conv@A2 by A29,RLAFFIN2:def 1;
then A57: Bu2.Bu<=1 by A3,RLAFFIN1:71;
A58: Bu2.Bu<1
proof
assume Bu2.Bu>=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:19;
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 be object;
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;
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:56;
end;
then A69: union s1u c<U by A55;
then consider xS1U be object such that
A70: xS1U in @U and
A71: not xS1U in union S1U by XBOOLE_0:6;
reconsider xS1U as Element of V by A70;
union S1U c=U\{xS1U} by A55,A71,ZFMISC_1:34;
then A72: conv union S1U c=conv@(U\{xS1U}) by RLAFFIN1:3;
U\{xS1U}c=U & U\{xS1U}<>U by A70,ZFMISC_1:56;
then U\{xS1U}c<U;
then A73: not Bu in conv@(U\{xS1U}) by A64,RLAFFIN2:def 1;
card union s1u<n+1 by A19,A69,CARD_2:48;
then A74: card union s1u<=n by NAT_1:13;
U\{xS2U}c=U & U\{xS2U}<>U by A40,ZFMISC_1:56;
then U\{xS2U}c<U;
then A75: not Bu in conv@(U\{xS2U}) by A64,RLAFFIN2:def 1;
A76: {U}c=S2 by A11,A18,A19,ZFMISC_1:2,31;
A77: S2\{U}c=S2 by XBOOLE_1:36;
A78: A2\{Bu}=BT.:S2\(B.:{U}) by A66,A8,A51,RELAT_1:129
.=BT.:S2\(BT.:{U}) by A76,A66,RELAT_1:129,XBOOLE_1:1
.=BT.:(S2\{U}) by FUNCT_1:64
.=B.:(S2\{U}) by A66,A77,RELAT_1:129,XBOOLE_1:1;
then conv(@A2\{Bu})c=conv union S2U by CONVEX1:30,RLAFFIN2:17;
then A79: p2 in conv union S2U by A61;
x in conv@U by A7,A17,A28,RLAFFIN2:def 1;
then p2=p1 by A15,A45,A49,A58,A62,A65,A42,A53,A75,A72,A73,A79,RLAFFIN2:2;
then A80: Int(@A1\{Bu})meets Int(@A2\{Bu}) by A50,A63,XBOOLE_0:3;
@A1\{Bu}=@(A1\{Bu}) & @A2\{Bu}=@(A2\{Bu});
then A1\{Bu}=A2\{Bu} by A6,A54,A52,A74,A78,A80;
hence A1=(A2\{Bu})\/{Bu} by A22,ZFMISC_1:116
.=A2 by A24,ZFMISC_1:116;
end;
end;
end;
A81: P[0 qua Nat]
proof
let S1,S2 be c=-linear finite simplex-like Subset-Family of Kas;
let A1,A2 be Simplex of BC such that
A82: A1=B.:S1 and
A2=B.:S2 and
A83: card union S1<=0 and
card union S2<=0 and
A84: Int@A1 meets Int@A2;
Int@A1 is non empty by A84;
then A1 is non empty;
then consider y being object such that
A85: y in A1;
consider x being object such that
A86: x in dom B and
A87: x in S1 and
B.x=y by A82,A85,FUNCT_1:def 6;
reconsider xx=x as set by TARSKI:1;
A88: x<>{} by A86,ZFMISC_1:56;
union S1 is empty by A83;
then xx c={} by A87,ZFMISC_1:74;
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 be object;
assume y in (center_of_mass V).:BOOL S;
then consider x being object 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 6;
reconsider x as non empty Subset of V by A9,ZFMISC_1:56;
conv x c=conv@S & y in conv x by A10,RLAFFIN2:16,RLTOPSP1:20;
hence thesis;
end;
bool@S c=(bool the carrier of V) by ZFMISC_1:67;
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;
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:74;
hence thesis by A6,A7,FUNCT_1:52;
end;
not{} in dom center_of_mass V by ZFMISC_1:56;
then A11: dom center_of_mass V is with_non-empty_elements;
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 ExtReal;
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:67;
then dom B=(bool the carrier of V)\{{}} & S c=bool the carrier of V by
FUNCT_2:def 1;
then A3: dom(B|S)=S by A2,RELAT_1:62,ZFMISC_1:34;
S c=T
proof
let x be object;
assume x in S;
then x is Simplex of Kas by TOPS_2:def 1;
hence thesis by PRE_TOPC:def 2;
end;
then B|T|S=B|S by RELAT_1:74;
then A4: B|S is one-to-one by FUNCT_1:52;
B.:S=rng(B|S) by RELAT_1:115;
then S,B.:S are_equipotent by A3,A4,WELLORD2:def 4;
hence thesis by CARD_1:5;
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:11
,XBOOLE_1:36;
set TK=the topology of Kas;
set BTK=B|TK;
A6: dom BTK=dom B/\TK by RELAT_1:61;
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:61;
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:11,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:112,129;
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:129;
then A13: w2 c=S2 by A5,A11,A12,FUNCT_1:87;
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:112;
then BTK.:s2=B.:S2 by A7,RELAT_1:129;
then A16: s2 c=w2 by A5,A11,A9,FUNCT_1:87;
@S1 c=bool the carrier of V & not{} in S1 by A2;
then S1 c=dom B by A8,ZFMISC_1:34;
then A17: S1 c=dom BTK by A6,A14,XBOOLE_1:19;
B.:S1=BTK.:S1 by A14,RELAT_1:129;
then S1 c=w2 by A4,A5,A11,A17,FUNCT_1:87;
hence S1 c=S2 by A13;
let x,y such that
A18: x in S2 & y in S2;
B.:s2=BTK.:s2 by A7,RELAT_1:129;
then w2 c=s2 by A5,A11,A12,A15,FUNCT_1:87;
then A19: s2=w2 by A16;
per cases;
suppose x is empty or y is empty;
then x c=y or y c=x;
hence thesis;
end;
suppose x is non empty & y is non empty;
then x in w2 & y in w2 by A18,A19,ZFMISC_1:56;
hence thesis by ORDINAL1:def 8;
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 ExtReal;
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 ExtReal;
A6: |.C.|c=[#]C;
then A7: BC=subdivision(B,C) by Def5;
card S+n<=card Aff-1 by A3,XREAL_1:19;
then A8: card S+n<=degree BC by A5,A6,Th31;
hereby A9: S c=the topology of C
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in S;
then xx c=U by ZFMISC_1:74;
then xx c=Aff by A2;
hence thesis by A4;
end;
then A10: B.:S=BTC.:S by RELAT_1:129;
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:61,ZFMISC_1:34;
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:11,XBOOLE_1:1;
A15: B.:S c=B.:AA by A13,A14,RELAT_1:112;
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:129;
A18: S\/T=AA\/S by XBOOLE_1:39
.=AA by A10,A11,A15,A17,FUNCT_1:87,XBOOLE_1:12;
T c=AA by XBOOLE_1:36;
then A19: T c=bool Aff by A4,A16;
A20: not{} in AA by ZFMISC_1:56;
then B.:a=B.:(a/\(dom B)) & AA is with_non-empty_elements by RELAT_1:112;
then A21: card Bf=card AA by A14,Th33;
A22: Bf=B.:AA by A14,RELAT_1:112
.=B.:S\/B.:T by A18,RELAT_1:120;
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:40
,XBOOLE_1:79,ZFMISC_1:81;
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,XBOOLE_1:79
,ZFMISC_1:77;
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:40
.=card S+n+1 by A25;
union(T\/S)=union T\/union S by ZFMISC_1:78;
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:67,82;
then A29: T\/S c=the topology of C by A4;
A30: TS is simplex-like
proof
let a be Subset of C;
thus thesis by A29;
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:120;
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;
Segm card U c= Segm card Aff by A2,CARD_1:11;
then card U<=card Aff by NAT_1:39;
then A4: N-1<=card U-1 & card U-1<=card Aff-1 by XREAL_1:9;
Sf c=bool U & bool U c=bool Aff by A2,ZFMISC_1:67,82;
then A5: s c=the topology of C by A3;
A6: s is simplex-like
proof
let a be Subset of C;
assume a in s;
hence thesis by A5;
end;
then A7: card s=card(B.:Sf) by A1,Th33;
Segm card Sf c= Segm card U by A1,SIMPLEX0:10;
then A8: card Sf<=card U by NAT_1:39;
set BC=BCS C;
reconsider c =card Aff as ExtReal;
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:9;
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 0<n & n<=card U ex x st x in Sf & card x=n
proof
assume B.:Sf is Simplex of card U-1,BC;
then reconsider BS=B.:Sf as Simplex of card U-1,BC;
reconsider c1=card U-1 as ExtReal;
let n;
reconsider s=Sf as Subset-Family of U by ZFMISC_1:82;
defpred P[Nat] means
$1<card Sf implies ex x be finite set st x in Sf & card x=card Sf-$1;
assume that
A14: 0<n and
A15: n<=card U;
A16: card Sf-(0 qua Real)>
(card Sf qua Real)-(n qua Real) by A14,XREAL_1:10;
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 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_2:102;
A23: for n st P[n] holds P[n+1]
proof
let n such that
A24: P[n];
assume A25: n+1<card Sf;
then consider X be finite set such that
A26: X in Sf and
A27: card X=card Sf-n by A24,NAT_1:13;
A28: n+1-n<card Sf-n by A25,XREAL_1:9;
then consider x such that
A29: x in X & X\{x} in Sf by A21,A22,A26,A27;
reconsider C=card X-1 as Element of NAT by A27,A28,NAT_1:20;
take X\{x};
card X=C+1;
hence thesis by A27,A29,STIRL2_1:55;
end;
A30: P[0 qua Nat] by A7,A17,A18,SIMPLEX0:9;
A31: for n holds P[n] from NAT_1:sch 2(A30,A23);
card Sf-n is Nat by A7,A15,A17,NAT_1:21;
then ex x be finite set st x in Sf & card x=card Sf-(card Sf-n) by A16,A31;
hence thesis;
end;
assume A32: for n st 0<n & n<=card U ex x st x in Sf & card x=n;
per cases;
suppose A33: U is empty;
reconsider O=-1 as ExtReal;
A34: O<=degree BC & 0=O+1 by A9,A10,A12,Th31,XXREAL_3:7;
Sf is empty by A1,A33;
then A35: BS is empty;
thus thesis by A33,A34,A35,SIMPLEX0:def 18;
end;
suppose A36: U is non empty;
reconsider c1=card U-1 as ExtReal;
consider x such that
A37: x in Sf and
card x=card U by A32,A36;
defpred P[object,object] means
ex D2 being set st D2 = $2 & card D2=$1;
A38: for x being object st x in Seg card U
ex y being object st y in Sf & P[x,y]
proof
let x being object such that
A39: x in Seg card U;
reconsider n=x as Nat by A39;
0<n & n<=card U by A39,FINSEQ_1:1;
then ex x st x in Sf & card x=n by A32;
hence thesis;
end;
consider f be Function of Seg card U,Sf such that
A40: for x being object st x in Seg card U holds P[x,f.x]
from FUNCT_2:sch 1(A38);
now let x1,x2 be object;
assume that
A41: x1 in dom f and
A42: x2 in dom f & f.x1=f.x2;
A43: P[x2,f.x2] by A40,A42;
P[x1,f.x1] by A40,A41;
hence x1=card(f.x1)
.=x2 by A42,A43;
end;
then A44: rng f c=Sf & f is one-to-one by FUNCT_1:def 4;
dom f=Seg card U by A37,FUNCT_2:def 1;
then Segm card Seg card U= Segm card U &
Segm card Seg card U c= Segm card Sf by A44,CARD_1:10
,FINSEQ_1:57;
then card U<=card Sf by NAT_1:39;
then A45: card BS=card U by A7,A8,XXREAL_0:1;
BS is Simplex of BC & c1+1=(card U-1)+1 by A6,A11,SIMPLEX0:def 20
,XXREAL_3:def 2;
hence thesis by A4,A9,A13,A45,SIMPLEX0:def 18;
end;
end;
Lm1: for S be finite finite-membered Subset-Family of V st S is c=-linear & S
is with_non-empty_elements & card S=card union S for A be non empty finite
Subset of V st A misses union S & union S\/A is affinely-independent holds
(center_of_mass V).:S\/(center_of_mass V).:{union S\/A} is
Simplex of card S,BCS Complex_of{union S\/A}
proof
let S be finite finite-membered Subset-Family of V such that
A1: S is c=-linear and
A2: S is with_non-empty_elements and
A3: card S=card union S;
set U=union S,B=center_of_mass V;
let A be non empty finite Subset of V such that
A4: A misses U and
A5: U\/A is affinely-independent;
reconsider UA=U\/A as finite affinely-independent Subset of V by A5;
set C=Complex_of{UA};
reconsider SUA=S\/{UA} as Subset-Family of C;
A6: U c=UA by XBOOLE_1:7;
A7: the topology of C=bool UA by SIMPLEX0:4;
A8: SUA c=the topology of C
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in SUA;
then x in S or x in {UA} by XBOOLE_0:def 3;
then xx c=U or x=UA by TARSKI:def 1,ZFMISC_1:74;
then xx c=UA by A6;
hence thesis by A7;
end;
A9: SUA is simplex-like
proof
let A be Subset of C;
assume A in SUA;
hence thesis by A8;
end;
set BC=BCS C;
A10: |.C.|c=[#]C;
then A11: BC=subdivision(B,C) by Def5;
then [#]BC=[#]C by SIMPLEX0:def 20;
then reconsider BSUA=B.:SUA as Subset of BC;
SUA is c=-linear
proof
let x,y be set such that
A12: x in SUA & y in SUA;
per cases by A12,XBOOLE_0:def 3;
suppose x in S & y in S;
hence thesis by A1;
end;
suppose x in S & y in {UA};
then x c=U & y=UA by TARSKI:def 1,ZFMISC_1:74;
then x c=y by A6;
hence thesis;
end;
suppose x in {UA} & y in S;
then x=UA & y c=U by TARSKI:def 1,ZFMISC_1:74;
then y c=x by A6;
hence thesis;
end;
suppose A13: x in {UA} & y in {UA};
then x=UA by TARSKI:def 1;
hence thesis by A13,TARSKI:def 1;
end;
end;
then reconsider BSUA as Simplex of BC by A9,A11,SIMPLEX0:def 20;
reconsider c =card UA as ExtReal;
A14: degree C=c-1 by SIMPLEX0:26
.=card UA+-1 by XXREAL_3:def 2;
A15: UA<>U
proof
assume UA=U;
then A c=U by XBOOLE_1:7;
hence contradiction by A4,XBOOLE_1:67;
end;
not UA in S
by ZFMISC_1:74,A6,A15;
then A16: card SUA=card S+1 by CARD_2:41;
U c<UA by A6,A15;
then card U<card UA by CARD_2:48;
then (card U)+1<=card UA by NAT_1:13;
then A17: card U<=card UA-1 by XREAL_1:19;
reconsider c =card S as ExtReal;
card BSUA=card SUA by A2,A9,Th33;
then A18: card BSUA=c+1 by A16,XXREAL_3:def 2;
degree BC=degree C by A10,Th31;
then BSUA is Simplex of card S,BC by A3,A14,A17,A18,SIMPLEX0:def 18;
hence thesis by RELAT_1:120;
end;
theorem Th37:
for S st S is c=-linear & S is with_non-empty_elements &
card S = card union S
for Af,Bf st Af is non empty & Af misses union S &
union S\/Af is affinely-independent & union S\/Af c=Bf
holds (center_of_mass V).:S \/ (center_of_mass V).:{union S\/Af}
is Simplex of card S,BCS Complex_of{Bf}
proof
let S be finite Subset-Family of V such that
A1: S is c=-linear & S is with_non-empty_elements and
A2: card S=card union S;
set U=union S,b=center_of_mass V;
let A,B be finite Subset of V such that
A3: A is non empty and
A4: A misses U & U\/A is affinely-independent and
A5: U\/A c=B;
reconsider UA=U\/A as finite Subset of V by A5;
dom b=(bool the carrier of V)\{{}} by FUNCT_2:def 1;
then UA in dom b by A3,ZFMISC_1:56;
then A6: {b.UA}=Im(b,UA) by FUNCT_1:59
.=b.:{UA} by RELAT_1:def 16;
set CA=Complex_of{UA};
set CB=Complex_of{B};
{UA}is_finer_than{B}
proof
let x;
assume x in {UA};
then A7: x=UA by TARSKI:def 1;
B in {B} by TARSKI:def 1;
hence thesis by A5,A7;
end;
then CA is SubSimplicialComplex of CB by SIMPLEX0:30;
then A8: subdivision(b,CA) is SubSimplicialComplex of subdivision(b,CB) by
SIMPLEX0:58;
|.CA.|c=[#]CA;
then A9: subdivision(b,CA)=BCS CA by Def5;
|.CB.|c=[#]CB;
then A10: BCS CA is SubSimplicialComplex of BCS CB by A8,A9,Def5;
S is finite-membered
proof
let x;
assume x in S;
then A11: x c=union S by ZFMISC_1:74;
union S is finite by A2;
hence thesis by A11;
end;
then b.:S\/b.:{UA} is Simplex of card S,BCS CA by A1,A2,A3,A4,Lm1;
hence thesis by A6,A10,SIMPLEX0:49;
end;
theorem Th38:
for Sf st Sf is with_non-empty_elements & card Sf = card union Sf
for v be Element of V st not v in union Sf &
union Sf\/{v} is affinely-independent
holds
{S1 where S1 is Simplex of card Sf,BCS Complex_of{union Sf\/{v}}:
(center_of_mass V).:Sf c= S1} =
{(center_of_mass V).:Sf\/(center_of_mass V).:{union Sf\/{v}}}
proof
let S be finite c=-linear finite-membered Subset-Family of V such that
A1: S is with_non-empty_elements and
A2: card S=card union S;
set U=union S;
set B=center_of_mass V;
let v be Element of V such that
A3: not v in U and
A4: U\/{v} is affinely-independent;
reconsider Uv=U\/{v} as finite affinely-independent Subset of V by A4;
set CUv=Complex_of{Uv};
set BC=BCS CUv;
set SS={S1 where S1 is Simplex of card S,BCS Complex_of{union S\/{v}}:B.:S
c=S1};
set TT={B.:S\/B.:{union S\/{v}}};
A5: U c=Uv by XBOOLE_1:7;
hereby let x be object;
reconsider n=0 as Nat;
assume x in SS;
then consider S1 be Simplex of card S,BC such that
A6: x=S1 and
A7: B.:S c=S1;
card S+n+1<=card Uv by A2,A3,CARD_2:41;
then consider T be finite Subset-Family of V such that
A8: T misses S and
A9: T\/S is c=-linear with_non-empty_elements and
A10: card T=n+1 and
A11: union T c=Uv and
A12: @S1=(center_of_mass V).:S\/(center_of_mass V).:T by A1,A5,A7,Th35;
A13: ex x being object st T={x} by A10,CARD_2:42;
A14: union(T\/S)=union T\/union S by ZFMISC_1:78;
T\/S is finite-membered
proof
let x;
assume x in T\/S;
then x c=union(T\/S) by ZFMISC_1:74;
hence thesis by A11,A14;
end;
then reconsider TS=T\/S as finite finite-membered Subset-Family of V;
union(T\/S)c=Uv by A5,A11,A14,XBOOLE_1:8;
then A15: card union TS c=card Uv by CARD_1:11;
card TS=card S+1 by A8,A10,CARD_2:40;
then A16: card TS=card Uv by A2,A3,CARD_2:41;
card TS c=card union TS by A9,SIMPLEX0:10;
then card union TS=card TS by A15,A16;
then A17: union TS=Uv by A5,A11,A14,A16,CARD_2:102,XBOOLE_1:8;
A18: union S c=union(T\/S) by A14,XBOOLE_1:7;
A19: not union TS in S
proof
assume union TS in S;
then union TS c=U by ZFMISC_1:74;
then A20: U=Uv by A17,A18;
v in {v} by TARSKI:def 1;
hence thesis by A3,A20,XBOOLE_0:def 3;
end;
T is non empty by A10;
then union TS in TS by A9,SIMPLEX0:9;
then union TS in T by A19,XBOOLE_0:def 3;
then T={Uv} by A13,A17,TARSKI:def 1;
hence x in TT by A6,A12,TARSKI:def 1;
end;
let x be object;
assume x in TT;
then A21: x=B.:S\/B.:{Uv} by TARSKI:def 1;
B.:S c=B.:S\/B.:{Uv} & B.:S\/B.:{Uv} is Simplex of card S,BC by A1,A2,A3,Th37
,XBOOLE_1:7,ZFMISC_1:50;
hence thesis by A21;
end;
theorem Th39:
for Sf st Sf is with_non-empty_elements & card Sf+1 = card union Sf &
union Sf is affinely-independent
holds card {S1 where S1 is Simplex of card Sf,BCS Complex_of{union Sf}:
(center_of_mass V).:Sf c= S1} = 2
proof
let S be finite c=-linear finite-membered Subset-Family of V such that
A1: S is with_non-empty_elements and
A2: card S+1=card union S and
A3: union S is affinely-independent;
set B=center_of_mass V;
reconsider U=union S as finite affinely-independent Subset of V by A3;
reconsider s=S as Subset-Family of U by ZFMISC_1:82;
A4: S is non empty by A2,ZFMISC_1:2;
then consider ss1 be Subset-Family of U such that
A5: s c=ss1 and
A6: ss1 is with_non-empty_elements c=-linear and
A7: card ss1=card U and
A8: for X st X in ss1 & card X<>1 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:44;
then consider x being object such that
A9: ss1\s={x} by CARD_2:42;
reconsider c =card U as ExtReal;
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 ExtReal;
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;
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 object st x={z} by CARD_2:42;
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:33;
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:116;
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:56;
end;
hence xm in s or xm={};
card x=c1+1;
hence card xm=card x-1 by A26,STIRL2_1:55;
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;
then xm c=y by A31;
hence contradiction by A19,A28,A29,A30,A31,ZFMISC_1:138;
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:74;
then A36: union ss=U;
x c<U by A9,A17,A19,A35;
then card x<card U by CARD_2:48;
then card x+1<=card U by NAT_1:13;
then consider xM be set such that
A37: xM in ss and
A38: card xM=card x+1 by A6,A36,A21,Th36;
reconsider xm as finite Subset of V by A32,XBOOLE_1:2;
reconsider xM as finite Subset of V by A37;
A39: not xM c=xm
proof
assume xM c=xm;
then card x+1<=card x+-1 by A33,A38,NAT_1:43;
hence contradiction by XREAL_1:6;
end;
A40: xM in s
proof
assume not xM in s;
then xM in ss\s by A37,XBOOLE_0:def 5;
then xM=x by A9,TARSKI:def 1;
hence contradiction by A38;
end;
then xm,xM are_c=-comparable or xm c=xM by A32,ORDINAL1:def 8;
then A41: xm c=xM by A39;
then card(xM\xm)=card xM-card xm by CARD_2:44;
then consider x1,x2 be object such that
A42: x1<>x2 and
A43: xM\xm={x1,x2} by A33,A38,CARD_2:60;
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:120;
A47: not x1 in xm by A43,A44,XBOOLE_0:def 5;
then A48: card xm1=card xm+1 by CARD_2:41;
A49: not xm1 in S
proof
assume A50: xm1 in S;
then x,xm1 are_c=-comparable by A5,A6,A18;
then x c=xm1 or xm1 c=x;
hence thesis by A19,A33,A48,A50,CARD_2:102;
end;
not x2 in xm by A43,A45,XBOOLE_0:def 5;
then A51: card xm2=card xm+1 by CARD_2:41;
A52: not xm2 in S
proof
assume A53: xm2 in S;
then x,xm2 are_c=-comparable by A5,A6,A18;
then x c=xm2 or xm2 c=x;
hence thesis by A19,A33,A51,A53,CARD_2:102;
end;
x2 in xM by A43,A45,XBOOLE_0:def 5;
then {x2}c=xM by ZFMISC_1:31;
then A54: xm2 c=xM by A41,XBOOLE_1:8;
A55: S2 c=bool U
proof
let A be object such that
A56: A in S2;
reconsider AA=A as set by TARSKI:1;
per cases by A56,XBOOLE_0:def 3;
suppose A in S;
then AA c=U by ZFMISC_1:74;
hence thesis;
end;
suppose A in {xm2};
then A=xm2 by TARSKI:def 1;
then AA 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;
end;
then card BS2=card S2 by A1,Th33;
then A58: card BS2=card S+1 by A52,CARD_2:41;
x1 in xM by A43,A44,XBOOLE_0:def 5;
then {x1}c=xM by ZFMISC_1:31;
then A59: xm1 c=xM by A41,XBOOLE_1:8;
A60: S1 c=bool U
proof
let A be object such that
A61: A in S1;
reconsider AA=A as set by TARSKI:1;
per cases by A61,XBOOLE_0:def 3;
suppose A in S;
then AA c=U by ZFMISC_1:74;
hence thesis;
end;
suppose A in {xm1};
then A=xm1 by TARSKI:def 1;
then AA c=U by A37,A59,XBOOLE_1:1;
hence thesis;
end;
end;
then A62: BS1=(B|TC).:S1 by A10,RELAT_1:129;
A63: S1 is simplex-like
proof
let A be Subset of CU;
assume A in S1;
hence thesis by A10,A60;
end;
then card BS1=card S1 by A1,Th33;
then A64: card BS1=card S+1 by A49,CARD_2:41;
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 8;
per cases by A68;
suppose xM c=y1 or xM=y1;
then xm1 c=y1 & xm2 c=y1 by A54,A59;
hence thesis;
end;
suppose A69: y1 c=xM & xM<>y1;
then reconsider y1 as finite set;
A70: y1 c<xM by A69;
A71: not x c=y1
proof
A72: card y1<card xM by A70,CARD_2:48;
assume A73: x c=y1;
then card x<=card y1 by NAT_1:43;
then card x=card y1 by A38,A72,NAT_1:9;
hence contradiction by A19,A67,A73,CARD_2:102;
end;
x in ss by A9,A17,XBOOLE_0:def 5;
then y1,x are_c=-comparable by A5,A6,A67;
then y1 c=x by A71;
then y1 c=xm by A34,A67;
then y1 c=xm1 & y1 c=xm2 by A65;
hence thesis;
end;
end;
S1 is c=-linear
proof
let y1,y2 be set;
assume that
A74: y1 in S1 and
A75: y2 in S1;
y1 in S or y1 in {xm1} by A74,XBOOLE_0:def 3;
then A76: y1 in S or y1=xm1 by TARSKI:def 1;
y2 in S or y2 in {xm1} by A75,XBOOLE_0:def 3;
then y2 in S or y2=xm1 by TARSKI:def 1;
hence thesis by A66,A76,ORDINAL1:def 8;
end;
then BS1 is simplex-like by A12,A63,SIMPLEX0:def 20;
then A77: BS1 is Simplex of card U-1,BC by A2,A15,A16,A20,A64,SIMPLEX0:def 18
;
set SS={S3 where S3 is Simplex of card S,BCS Complex_of{union S}:B.:S c=S3};
B.:S c=B.:S\/B.:{xm1} by XBOOLE_1:7;
then A78: BS1 in SS by A2,A46,A77;
A79: BS2=B.:S\/B.:{xm2} by RELAT_1:120;
A80: SS c={BS1,BS2}
proof
let w be object;
reconsider n=0 as Nat;
assume w in SS;
then consider W be Simplex of card S,BC such that
A81: w=W and
A82: B.:S c=W;
card S+n+1<=card U by A2;
then consider T be finite Subset-Family of V such that
A83: T misses S and
A84: T\/S is c=-linear with_non-empty_elements and
A85: card T=n+1 and
A86: union T c=U and
A87: @W=B.:S\/B.:T by A1,A82,Th35;
consider x3 be object such that
A88: {x3}=T by A85,CARD_2:42;
A89: x3 in T by A88,TARSKI:def 1;
then A90: not x3 in S by A83,XBOOLE_0:3;
reconsider x3 as set by TARSKI:1;
A91: x3 c=union T by A89,ZFMISC_1:74;
A92: x3 in T\/S by A89,XBOOLE_0:def 3;
reconsider x3 as finite Subset of U by A86,A91,XBOOLE_1:1;
A93: not xM c=x3
proof
consider x4 be set such that
A94: x4 in ss and
A95: card x4=card x3 by A6,A36,A21,A84,A92,Th36,NAT_1:43;
assume xM c=x3;
then card x+1<=card x3 by A38,NAT_1:43;
then x<>x4 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;
then x3 c=x4 or x4 c=x3;
hence contradiction by A90,A95,A96,CARD_2:102;
end;
A97: xm c=x3 & xm<>x3
proof
per cases by A32;
suppose xm={};
hence thesis by A84,A92;
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:43;
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:43;
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;
then x3 c=x4 or x4 c=x3;
hence contradiction by A90,A102,A103,CARD_2:102;
end;
xm in T\/S by A98,XBOOLE_0:def 3;
then xm,x3 are_c=-comparable by A84,A92;
hence thesis by A99;
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;
then x3 c=xM by A93;
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<>{}
by XBOOLE_1:37,A97;
x3\/xm=(x3\xm)\/xm by XBOOLE_1:39;
then x3=xm1 or x3=xm2 by A43,A104,A105,A107,A108,ZFMISC_1:36;
hence thesis by A79,A46,A81,A87,A88,TARSKI:def 2;
end;
A109: BS2=(B|TC).:S2 by A10,A55,RELAT_1:129;
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:64;
then A112: dom(B|TC)misses S1\S2 by RELAT_1:118;
BS2\BS1={} by A111,XBOOLE_1:37;
then (B|TC).:(S2\S1)={} by A109,A62,FUNCT_1:64;
then A113: dom(B|TC)misses S2\S1 by RELAT_1:118;
A114: dom(B|TC)=dom B/\TC by RELAT_1:61;
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:34;
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:34;
S1\S2 c=bool U by A60,A117;
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;
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 8;
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:32;
then SS={BS1,BS2} by A80;
hence thesis by A110,CARD_2:57;
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 2;
then A in the topology of BCS K by A7;
then reconsider a=A as Simplex of BCS K by PRE_TOPC:def 2;
|.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:56;
then A14: Bag.aK in A by A10,A12,FUNCT_1:def 6;
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;
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 ExtReal;
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 ExtReal;
|.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;
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:77;
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:82;
then R c=bool UT;
then R c=the topology of K by A15;
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:13;
then reconsider BST as Simplex of BK by A6,A20,SIMPLEX0:def 20;
card ST=card Sk+card T by A19,CARD_2:40;
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:120,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:44
.=1;
then consider v be object such that
A5: Ak\union Sk={v} by CARD_2:42;
reconsider Ak1=@Ak as affinely-independent finite Subset of V;
set C=Complex_of{Ak1};
reconsider c =card Ak as ExtReal;
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 be object;
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 be object;
reconsider c1=card Sk as ExtReal;
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 ExtReal;
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;
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 ExtReal;
@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 be object;
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 be object;
reconsider c1=card Sk as ExtReal;
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 ExtReal;
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 ExtReal;
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:31,146;
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 2;
then reconsider s=S as Simplex of K by PRE_TOPC:def 2;
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 be object;
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 2;
then reconsider w=W as Simplex of BCS K by PRE_TOPC:def 2;
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 be object;
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 2;
then reconsider w=W as Simplex of K by PRE_TOPC:def 2;
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:11;
A28: SS1 c=bool@(union SS1) & bool@(union SS1)c=bool the carrier of V by
ZFMISC_1:67,82;
A29: not{} in SS1 by ZFMISC_1:56;
then A30: SS1 is with_non-empty_elements;
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:112;
then A34: card SS1=n by A16,A27,A30,Th33;
A35: S=B.:SS1 by A27,A32,RELAT_1:112;
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;
Segm card SS1 c= Segm card U by A30,SIMPLEX0:10;
then A39: n<=card U by A16,A36,NAT_1:39;
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;
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;
consider w1,w2 be object such that
A46: w1<>w2 and
A47: XX={w1,w2} by A45,CARD_2:60;
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:112;
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;
then A57: SS1\/{W1} is simplex-like by TOPS_2:13;
A58: S\/B.:{W1}=B.:(SS1\/{W1}) & S\/B.:{W2}=B.:(SS1\/{W2}) by A35,
RELAT_1:120;
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;
then A60: SS1\/{W2} is simplex-like by TOPS_2:13;
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:74;
then W1=U by A52;
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 be object;
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 object such that
A71: T={t} by A69,CARD_2:42;
set TS=T\/SS1;
A72: card TS=n+1 by A16,A36,A67,A69,CARD_2:40;
A73: union TS in TS by A68,A71,SIMPLEX0:9;
TS is simplex-like by TOPS_2:13;
then reconsider UTS=union TS as Simplex of K by A73;
Segm card TS c= Segm card UTS by A68,SIMPLEX0:10;
then A74: card TS<=card UTS by NAT_1:39;
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:43,ZFMISC_1:74;
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:77;
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:32;
then X={S\/B.:{W1},S\/B.:{W2}} by A63;
hence card X=2 by A56,CARD_2:57;
end;
A78: conv@S c=conv A & A is non empty by A2,A41,A42;
assume conv@S misses Int A;
then consider BB be Subset of V such that
A79: BB c<A and
A80: conv@S c=conv BB by A7,A78,RLAFFIN2:23;
A81: BB c=A by A79;
then reconsider B1=BB as finite Subset of V;
card B1<n+1 by A2,A79,CARD_2:48;
then A82: card B1<=n by NAT_1:13;
Affin@S c=Affin BB by A80,RLAFFIN1:68;
then n<=card B1 by A16,RLAFFIN1:79;
then card B1=n by A82,XXREAL_0:1;
then card(A\BB)=n+1-n by A2,A81,CARD_2:44;
then consider ab be object such that
A83: A\BB={ab} by CARD_2:42;
U is non empty by A26,A43;
then @U in dom B by A31,ZFMISC_1:56;
then A84: S c=conv@S & B.U in @S by A35,A38,FUNCT_1:def 6,RLAFFIN1:2;
then B.U in conv@S;
then A85: B.U in conv@U by A42;
set BUU=B.U|--@U;
@U c=conv@U by RLAFFIN1:2;
then A86: @U c=conv A by A41;
A87: ab in {ab} by TARSKI:def 1;
then reconsider ab as Element of V by A83;
A88: SS1 is with_non-empty_elements & S=B.:SS1 by A27,A29,A32,RELAT_1:112;
A89: conv@U c=Affin@U by RLAFFIN1:65;
then sum BUU=1 by A85,RLAFFIN1:def 7;
then consider F be FinSequence of REAL,G be FinSequence of the carrier of V
such that
A90: (Sum BUU|--A).ab=Sum F and
A91: len G=len F and
G is one-to-one and
A92: rng G=Carrier BUU and
A93: for n st n in dom F holds F.n=BUU.(G.n)*(G.n|--A).ab by A7,A86,
RLAFFIN2:3;
A94: dom G=dom F by A91,FINSEQ_3:29;
U c=conv B1
proof
A95: Carrier BUU c=U by RLVECT_2:def 6;
A96: now let i be Nat such that
A97: i in dom F;
A98: F.i=BUU.(G.i)*(G.i|--A).ab by A93,A97;
A99: G.i in rng G by A94,A97,FUNCT_1:def 3;
then G.i in U by A92,A95;
then A100: (G.i|--A).ab>=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 object such that
A102: t in U and
A103: not t in conv B1;
reconsider tt=t as set by TARSKI:1;
A104: (t|--A).ab>0
proof
A\{ab}c=B1
proof
let x be object;
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 object such that
A108: n in dom G and
A109: G.n=t by A92,FUNCT_1:def 3;
reconsider n as Nat by A108;
F.n=BUU.tt*(t|--A).ab by A93,A94,A108,A109;
then 0<Sum F by A94,A96,A102,A104,A107,A108,RVSUM_1:85;
then A110: (B.U|--A).ab>0 by A85,A89,A90,RLAFFIN1:def 7;
Carrier(B.U|--BB)c=BB by RLVECT_2:def 6;
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 object such that
A112: XX={w1} by CARD_2:42;
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 be object;
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 object such that
A124: T={t} by A122,CARD_2:42;
set TS=T\/SS1;
A125: card TS=n+1 by A16,A36,A120,A122,CARD_2:40;
A126: union TS in TS by A121,A124,SIMPLEX0:9;
TS is simplex-like by TOPS_2:13;
then reconsider UTS=union TS as Simplex of K by A126;
Segm card TS c= Segm card UTS by A121,SIMPLEX0:10;
then A127: card TS<=card UTS by NAT_1:39;
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:43,ZFMISC_1:74;
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,XBOOLE_1:7,XXREAL_0:1;
then U c= UTS & UTS is Simplex of n,K by A3,A117,SIMPLEX0:def 18
,ZFMISC_1:77;
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:33;
hence card X=1 by CARD_1:30;
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:56;
then A131: S c=conv@S & B.U in @S by A35,A38,FUNCT_1:def 6,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;
then consider BB be Subset of V such that
A134: BB c<A and
A135: conv@S c=conv BB by A7,A133,RLAFFIN2:23;
A136: BB c=A by A134;
then reconsider B1=BB as finite Subset of V;
Affin@S c=Affin BB by A135,RLAFFIN1:68;
then A137: n<=card B1 by A16,RLAFFIN1:79;
A138: card B1<n+1 by A2,A134,CARD_2:48;
then card B1<=n by NAT_1:13;
then card B1=n by A137,XXREAL_0:1;
then card(A\BB)=n+1-n by A2,A136,CARD_2:44;
then consider ab be object such that
A139: A\BB={ab} by CARD_2:42;
@U c=conv@U by RLAFFIN1:2;
then A140: @U c=conv A by A41;
A141: ab in {ab} by TARSKI:def 1;
then reconsider ab as Element of V by A139;
A142: conv@U c=Affin@U by RLAFFIN1:65;
then sum BUU=1 by A132,RLAFFIN1:def 7;
then consider F be FinSequence of REAL,G be FinSequence of the carrier of
V such that
A143: (Sum BUU|--A).ab=Sum F and
A144: len G=len F and
G is one-to-one and
A145: rng G=Carrier BUU and
A146: for n st n in dom F holds F.n=BUU.(G.n)*(G.n|--A).ab by A7,A140,
RLAFFIN2:3;
A147: dom G=dom F by A144,FINSEQ_3:29;
A148: A\{ab}=A/\BB by A139,XBOOLE_1:48
.=BB by A136,XBOOLE_1:28;
U c=conv B1
proof
A149: Carrier BUU c=U by RLVECT_2:def 6;
A150: now let i be Nat such that
A151: i in dom F;
A152: F.i=BUU.(G.i)*(G.i|--A).ab by A146,A151;
A153: G.i in rng G by A147,A151,FUNCT_1:def 3;
then G.i in U by A145,A149;
then A154: (G.i|--A).ab>=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 object such that
A156: t in U and
A157: not t in conv B1;
reconsider tt=t as set by TARSKI:1;
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 object such that
A162: n in dom G and
A163: G.n=t by A145,FUNCT_1:def 3;
reconsider n as Nat by A162;
F.n=BUU.tt*(t|--A).ab by A146,A147,A162,A163;
then 0<Sum F by A147,A150,A156,A159,A161,A162,RVSUM_1:85;
then A164: (B.U|--A).ab>0 by A132,A142,A143,RLAFFIN1:def 7;
Carrier(B.U|--BB)c=BB by RLVECT_2:def 6;
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;
consider w1,w2 be object such that
w1<>w2 and
A167: XX={w1,w2} by A166,CARD_2:60;
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 object;
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:13;
A178: W=B.:@TS by A177,RELAT_1:120;
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:77;
then n+1<=card UTS by A129,NAT_1:43;
then UTS=U by A129,A179,A180,CARD_2:102,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:32;
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 ExtReal;
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 ExtReal;
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 2;
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 be object;
reconsider N=n as ExtReal;
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 2;
card U=N+1 by A3,SIMPLEX0:def 18
.=n+1 by XXREAL_3:def 2;
then Aff=U by A1,A6,A11,CARD_2:102;
hence thesis by A10,TARSKI:def 1;
end;
A12: S in bool Aff by A6,A7,PRE_TOPC:def 2;
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:33;
n+-1>=-1 & n-1<=degree C by A3,XREAL_1:31,146;
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 c<Aff by A12;
hence thesis by A13,CARD_1:30,RLAFFIN2:7;
end;
A14: for k st P[k] holds P[k+1]
proof
let k such that
A15: P[k];
A16: degree BCS(k,C)=n & BCS(k+1,C)=BCS BCS(k,C) by A3,A4,Th20,Th32;
let S be Simplex of n-1,BCS(k+1,C),X such that
A17: X={S1 where S1 is Simplex of n,BCS(k+1,C):S c=S1};
thus thesis by A1,A15,A16,A17,Th44;
end;
for k holds P[k] from NAT_1:sch 2(A5,A14);
hence thesis;
end;
begin :: The Main Theorem
reserve v for Vertex of BCS(k,Complex_of{Aff}),
F for Function of Vertices BCS(k,Complex_of{Aff}),Aff;
theorem Th46:
for F st for v,B st B c= Aff & v in conv B holds F.v in B
ex n st card {S where S is Simplex of card Aff-1,BCS(k,Complex_of{Aff}):
F.:S = Aff} = 2*n+1
proof
reconsider O=1 as ExtReal;
reconsider Z=0 as ExtReal;
defpred P[Nat] means
for A be finite affinely-independent Subset of V st card A=$1
for F be Function of Vertices BCS(k,Complex_of{A}),A st
for v be Vertex of BCS(k,Complex_of{A})
for B be Subset of V st B c=A & v in conv B holds F.v in B ex n st card{S
where S is Simplex of card A-1,BCS(k,Complex_of{A}):F.:S=A}=2*n+1;
A1: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat such that
A2: P[m];
let A be finite affinely-independent Subset of V such that
A3: card A=m+1;
A is non empty by A3;
then consider a be object such that
A4: a in A;
reconsider a as Element of V by A4;
A5: card(A\{a})=m by A3,A4,STIRL2_1:55;
reconsider Aa=A\{a} as finite affinely-independent Subset of V
by RLAFFIN1:43,XBOOLE_1:36;
set CAa=Complex_of{Aa};
the topology of CAa=bool Aa by SIMPLEX0:4;
then A6: Vertices CAa=union bool Aa by SIMPLEX0:16
.=Aa by ZFMISC_1:81;
A7: [#]CAa=[#]V & |.CAa.|c=[#]V;
then A8: Vertices CAa c=Vertices BCS(k,CAa) by Th24;
set CA=Complex_of{A};
let F be Function of Vertices BCS(k,CA),A such that
A9: for v be Vertex of BCS(k,CA)for B be Subset of V st B c=A & v in conv
B holds F.v in B;
set XX={S where S is Simplex of card A-1,BCS(k,CA):F.:S=A};
A10: XX c=the topology of BCS(k,CA)
proof
let x be object;
assume x in XX;
then ex S be Simplex of card A-1,BCS(k,CA) st S=x & A=F.:S;
hence thesis by PRE_TOPC:def 2;
end;
then reconsider XX as Subset-Family of BCS(k,CA) by XBOOLE_1:1;
reconsider XX as simplex-like Subset-Family of BCS(k,CA) by A10,SIMPLEX0:14;
A11: [#]CA=[#]V & |.CA.|c=[#]V;
A12: A\{a}c=A by XBOOLE_1:36;
for x st x in {Aa}ex y st y in {A} & x c=y
proof
let x;
assume A13: x in {Aa};
take A;
thus thesis by A12,A13,TARSKI:def 1;
end;
then {Aa}is_finer_than{A};
then CAa is SubSimplicialComplex of CA by SIMPLEX0:30;
then A14: BCS(k,CAa) is SubSimplicialComplex of BCS(k,CA) by A11,A7,Th23;
then A15: Vertices BCS(k,CAa)c=Vertices BCS(k,CA) by SIMPLEX0:31;
A16: the topology of CA=bool A by SIMPLEX0:4;
then A17: Vertices CA=union bool A by SIMPLEX0:16
.=A by ZFMISC_1:81;
A18: dom F=Vertices BCS(k,CA) by A4,FUNCT_2:def 1;
per cases;
suppose A19: m=0;
A20: O-1=0 by XXREAL_3:7;
then A21: degree CA=0 by A3,A19,SIMPLEX0:26;
k=0 or k>0;
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 2;
A24: A1 is Simplex of 0,CA by A3,A19,A20,SIMPLEX0:48;
ex x being object st A={x} by A3,A19,CARD_2:42;
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 be object;
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 2;
card S=Z+1 by A21,SIMPLEX0:def 18
.=1 by XXREAL_3:4;
then S=A by A3,A16,A19,A29,CARD_2:102;
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:59;
then A in XX by A3,A19,A24,A22;
then XX={A} by A27,ZFMISC_1:33;
hence thesis by CARD_1:30;
end;
suppose A30: m>0;
defpred P[object,object] means
ex D1,D2 being set st D1 = $1 & D2 = $2 & D1 c= D2;
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 ExtReal;
reconsider M=m as ExtReal;
reconsider cA=card A as ExtReal;
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 be object;
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 2;
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[object,object] means
ex D1,D2 being set st D1 = $1 & D2 = $2 & D2 c= D1;
set Xm1={S where S is Simplex of m-1,BCS(k,CA):Aa=F.:S};
set Xm=the set of all S where S is Simplex of m,BCS(k,CA);
consider R1 be Relation such that
A32: for x,y being object
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 be object;
reconsider xx=x as set by TARSKI:1;
assume A34: x in DY;
then consider y being object such that
A35: [x,y] in R1 by XTUPLE_0:def 12;
reconsider yy=y as set by TARSKI:1;
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;
P1[xx,yy] by A32,A35;
then yy c=xx;
then Aa c=F.:S by A36,A38,RELAT_1:123;
then Aa c<F.:S by A37;
then m<card(F.:S) by A5,CARD_2:48;
then A39: m+1<=card(F.:S) by NAT_1:13;
card(F.:S)<=m+1 by A3,NAT_1:43;
then F.:S=A by A3,A39,CARD_2:102,XXREAL_0:1;
hence thesis by A3,A36;
end;
set RDY=R1|DY;
A40: RDY|(dom RDY\DY)={}
proof
assume RDY|(dom RDY\DY)<>{};
then consider xy be object such that
A41: xy in RDY|(dom RDY\DY) by XBOOLE_0:def 1;
consider x,y being object 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:58;
hence contradiction by A43,XBOOLE_0:def 5;
end;
A44: 2*`card YA=card 2*`card card YA
.=card(2*card YA) by CARD_2:39;
cA-1=m+1+-1 by A3,XXREAL_3:def 2;
then A45: degree CA=m by SIMPLEX0:26;
consider R be Relation such that
A46: for x,y being object holds[x,y] in R iff x in Xm1 & y in Xm & P[x,y]
from RELAT_1:
sch 1;
A47: card R=card R1
proof
deffunc F(object)=[$1`2,$1`1];
A48: for x being object st x in R holds F(x) in R1
proof
let z be object;
assume A49: z in R;
then ex x,y being object st z=[x,y] by RELAT_1:def 1;
then A50: z=[z`1,z`2];
then A51: z`2 in Xm by A46,A49;
(P[z`1,z`2]) & z`1 in Xm1 by A46,A49,A50;
hence thesis by A32,A51;
end;
consider f be Function of R,R1 such that
A52: for x being object st x in R holds f.x=F(x) from FUNCT_2:sch 2(A48);
per cases;
suppose A53: R1 is empty;
R is empty
by A48,A53;
hence thesis by A53;
end;
suppose R1 is non empty;
then A54: dom f=R by FUNCT_2:def 1;
R1 c=rng f
proof
let z be object;
assume A55: z in R1;
then ex x,y being object st z=[x,y] by RELAT_1:def 1;
then A56: z=[z`1,z`2];
then A57: z`2 in Xm1 by A32,A55;
(P1[z`1,z`2]) & z`1 in Xm by A32,A55,A56;
then A58: [z`2,z`1] in R by A46,A57;
F([z`2,z`1])=z by A56;
then z=f.([z`2,z`1]) by A52,A58;
hence thesis by A54,A58,FUNCT_1:def 3;
end;
then A59: rng f=R1;
now let x1,x2 be object such that
A60: x1 in R and
A61: x2 in R and
A62: f.x1=f.x2;
f.x1=F(x1) & f.x2=F(x2) by A52,A60,A61;
then A63: x1`2=x2`2 & x1`1=x2`1 by A62,XTUPLE_0:1;
A64: ex x,y being object st x2=[x,y] by A61,RELAT_1:def 1;
ex x,y being object st x1=[x,y] by A60,RELAT_1:def 1;
hence x1=[x2`1,x2`2] by A63
.=x2 by A64;
end;
then f is one-to-one by A54,FUNCT_1:def 4;
then R,R1 are_equipotent by A54,A59,WELLORD2:def 4;
hence thesis by CARD_1:5;
end;
end;
A65: |.BCS(k,CAa).|=|.CAa.| & |.CAa.|=conv Aa by Th8,Th10;
set DX=dom R\XXA;
A66: DX c=the topology of BCS(k,CA)
proof
let x be object;
assume x in DX;
then ex y being object st[x,y] in R by XTUPLE_0:def 12;
then x in Xm1 by A46;
then ex S be Simplex of m-1,BCS(k,CA) st S=x & Aa=F.:S;
hence thesis by PRE_TOPC:def 2;
end;
set RDX=R|DX;
reconsider DX as Subset-Family of BCS(k,CA) by A66,XBOOLE_1:1;
reconsider DX as simplex-like Subset-Family of BCS(k,CA) by A66,SIMPLEX0:14
;
A67: RDX|(dom RDX\DX)={}
proof
assume RDX|(dom RDX\DX)<>{};
then consider xy be object such that
A68: xy in RDX|(dom RDX\DX) by XBOOLE_0:def 1;
consider x,y being object such that
A69: xy=[x,y] by A68,RELAT_1:def 1;
A70: x in dom RDX\DX by A68,A69,RELAT_1:def 11;
then dom RDX c=DX & x in dom RDX by RELAT_1:58;
hence contradiction by A70,XBOOLE_0:def 5;
end;
A71: m1+1=m-1+1 by XXREAL_3:def 2
.=m;
set FA=F|Vertices BCS(k,CAa);
A72: dom FA=Vertices BCS(k,CAa) by A18,A14,RELAT_1:62,SIMPLEX0:31;
A73: Vertices BCS(k,CAa) is non empty by A5,A6,A8,A30;
A74: 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 A75: B c=Aa & v in conv B;
v in Vertices BCS(k,CAa) by A73;
then F.v in B by A9,A12,A15,A75,XBOOLE_1:1;
hence thesis by A72,A73,FUNCT_1:47;
end;
rng FA c=Aa
proof
let y be object;
assume y in rng FA;
then consider x being object such that
A76: x in dom FA and
A77: FA.x=y by FUNCT_1:def 3;
reconsider v=x as Element of BCS(k,CAa) by A72,A76;
v is vertex-like by A72,A76,SIMPLEX0:def 4;
then consider S be Subset of BCS(k,CAa) such that
A78: S is simplex-like and
A79: v in S;
A80: conv@S c=|.BCS(k,CAa).| by A78,Th5;
S c=conv@S by RLAFFIN1:2;
then A81: v in conv@S by A79;
x in Vertices BCS(k,CAa) by A18,A14,A76,RELAT_1:62,SIMPLEX0:31;
hence thesis by A65,A74,A77,A80,A81;
end;
then reconsider FA as Function of Vertices BCS(k,CAa),Aa by A72,FUNCT_2:2;
set XXa={S where S is Simplex of m-1,BCS(k,CAa):FA.:S=Aa};
consider n such that
A82: card XXa=2*n+1 by A2,A5,A74;
A83: m-1<=m-0 & -1<=m+-1 by XREAL_1:10,31;
A84: for x being object st x in XXA holds card Im(R,x)=1
proof
let x be object;
assume x in XXA;
then consider S be Simplex of m-1,BCS(k,CA) such that
A85: x=S and
A86: F.:S=Aa and
A87: conv@S misses Int A;
set XX={S1 where S1 is Simplex of m,BCS(k,CA):S c=S1};
A88: R.:{S}c=XX
proof
let w be object;
reconsider ww=w as set by TARSKI:1;
assume w in R.:{S};
then consider s be object such that
A89: [s,w] in R and
A90: s in {S} by RELAT_1:def 13;
reconsider ss = s as set by TARSKI:1;
w in Xm by A46,A89;
then A91: ex W be Simplex of m,BCS(k,CA) st w=W;
P[ss,ww] by A46,A89;
then s=S & ss c=ww by A90,TARSKI:def 1;
hence thesis by A91;
end;
XX c=R.:{S}
proof
let w be object;
assume w in XX;
then consider W be Simplex of m,BCS(k,CA) such that
A92: w=W and
A93: S c=W;
W in Xm & S in Xm1 by A86;
then S in {S} & [S,W] in R by A46,A93,TARSKI:def 1;
hence thesis by A92,RELAT_1:def 13;
end;
then A94: R.:{S}=XX by A88;
card XX=1 by A3,A87,Th45;
hence thesis by A85,A94,RELAT_1:def 16;
end;
A95: degree CA=degree BCS(k,CA) by A11,Th32;
A96: M+1=m+1 by XXREAL_3:def 2;
A97: for x being object st x in YA holds card Im(R1,x)=2
proof
let x be object;
assume x in YA;
then consider S be Simplex of m,BCS(k,CA) such that
A98: x=S and
A99: Aa=F.:S;
set FS=F|S;
A100: rng FS=Aa by A99,RELAT_1:115;
A101: Aa is non empty by A5,A30;
A102: S in {x} by A98,TARSKI:def 1;
A103: dom FS=S by A18,RELAT_1:62,SIMPLEX0:17;
A104: card S=m+1 by A95,A45,A96,SIMPLEX0:def 18;
reconsider FS as Function of S,Aa by A100,A103,FUNCT_2:1;
FS is onto by A100,FUNCT_2:def 3;
then consider b be set such that
A105: b in Aa and
A106: card(FS"{b})=2 and
A107: for x st x in Aa & x<>b holds card(FS"{x})=1 by A5,A101,A104,Th2;
consider a1,a2 be object such that
A108: a1<>a2 and
A109: FS"{b}={a1,a2} by A106,CARD_2:60;
reconsider S1=S\{a1},S2=S\{a2} as Simplex of BCS(k,CA);
A110: a1 in {a1,a2} by TARSKI:def 2;
then A111: a1 in S2 by A108,A109,ZFMISC_1:56;
A112: card S1=m by A104,A109,A110,STIRL2_1:55;
A113: a2 in {a1,a2} by TARSKI:def 2;
then A114: card S2=m by A104,A109,STIRL2_1:55;
then reconsider S1,S2 as Simplex of m-1,BCS(k,CA) by A95,A83,A71,A45,A112,
SIMPLEX0:def 18;
A115: {a1}c=S by A109,A110,ZFMISC_1:31;
A116: FS.a2=F.a2 by A103,A109,A113,FUNCT_1:47;
A117: {a2}c=S by A109,A113,ZFMISC_1:31;
A118: R1.:{x}c={S1,S2}
proof
let Y be object;
assume Y in R1.:{x};
then consider X be object such that
A119: [X,Y] in R1 and
A120: X in {x} by RELAT_1:def 13;
Y in Xm1 by A32,A119;
then consider W be Simplex of m-1,BCS(k,CA) such that
A121: Y=W and
A122: Aa=F.:W;
X=x by A120,TARSKI:def 1;
then P1[S,W] by A32,A98,A119,A121;
then W c=S;
then A123: Aa=FS.:W by A122,RELAT_1:129;
then consider w be object such that
A124: w in dom FS and
A125: w in W and
A126: FS.w=b by A105,FUNCT_1:def 6;
A127: {w}c=W by A125,ZFMISC_1:31;
A128: S\{a1,a2}c=W
proof
let s be object;
assume A129: s in S\{a1,a2};
then A130: s in dom FS by A103,XBOOLE_0:def 5;
then A131: FS.s in Aa by A100,FUNCT_1:def 3;
then consider w be object such that
A132: w in dom FS and
A133: w in W and
A134: FS.w=FS.s by A123,FUNCT_1:def 6;
not s in FS"{b} by A109,A129,XBOOLE_0:def 5;
then not FS.s in {b} by A130,FUNCT_1:def 7;
then FS.s<>b by TARSKI:def 1;
then card(FS"{FS.s})=1 by A107,A131;
then consider z be object such that
A135: FS"{FS.s}={z} by CARD_2:42;
A136: FS.s in {FS.s} by TARSKI:def 1;
then A137: s in FS"{FS.s} by A130,FUNCT_1:def 7;
w in FS"{FS.s} by A132,A134,A136,FUNCT_1:def 7;
then w=z by A135,TARSKI:def 1;
hence thesis by A133,A135,A137,TARSKI:def 1;
end;
b in {b} by TARSKI:def 1;
then A138: w in FS"{b} by A124,A126,FUNCT_1:def 7;
A139: card W=m by A95,A83,A71,A45,SIMPLEX0:def 18;
A140: S/\{a1}={a1} by A115,XBOOLE_1:28;
A141: S/\{a2}={a2} by A117,XBOOLE_1:28;
per cases by A109,A138,TARSKI:def 2;
suppose w=a1;
then (S\{a1,a2})\/{w}=S\({a1,a2}\{a1}) by A140,XBOOLE_1:52
.=S2 by A108,ZFMISC_1:17;
then S2=W by A114,A127,A128,A139,CARD_2:102,XBOOLE_1:8;
hence thesis by A121,TARSKI:def 2;
end;
suppose w=a2;
then (S\{a1,a2})\/{w}=S\({a1,a2}\{a2}) by A141,XBOOLE_1:52
.=S1 by A108,ZFMISC_1:17;
then S1=W by A112,A127,A128,A139,CARD_2:102,XBOOLE_1:8;
hence thesis by A121,TARSKI:def 2;
end;
end;
A142: S c=dom F by A18,SIMPLEX0:17;
A143: FS.a1=F.a1 by A103,A109,A110,FUNCT_1:47;
A144: FS.a1 in {b} by A109,A110,FUNCT_1:def 7;
then A145: FS.a1=b by TARSKI:def 1;
A146: FS.a2 in {b} by A109,A113,FUNCT_1:def 7;
then A147: FS.a2=b by TARSKI:def 1;
A148: a2 in S & a2 in S1 by A108,A109,A113,ZFMISC_1:56;
A149: Aa c=F.:S1
proof
let z be object;
assume A150: z in Aa;
per cases;
suppose A151: z=b;
FS.a2 in F.:S1 by A142,A116,A148,FUNCT_1:def 6;
hence thesis by A146,A151,TARSKI:def 1;
end;
suppose A152: z<>b;
consider c be object such that
A153: c in dom F and
A154: c in S and
A155: z=F.c by A99,A150,FUNCT_1:def 6;
c in S1 by A143,A145,A152,A154,A155,ZFMISC_1:56;
hence thesis by A153,A155,FUNCT_1:def 6;
end;
end;
A156: S in Xm;
A157: a1 in S & a1 in S2 by A108,A109,A110,ZFMISC_1:56;
A158: Aa c=F.:S2
proof
let z be object;
assume A159: z in Aa;
per cases;
suppose A160: z=b;
FS.a1 in F.:S2 by A143,A142,A157,FUNCT_1:def 6;
hence thesis by A144,A160,TARSKI:def 1;
end;
suppose A161: z<>b;
consider c be object such that
A162: c in dom F and
A163: c in S and
A164: z=F.c by A99,A159,FUNCT_1:def 6;
c in S2 by A116,A147,A161,A163,A164,ZFMISC_1:56;
hence thesis by A162,A164,FUNCT_1:def 6;
end;
end;
F.:S1 c=Aa by A99,RELAT_1:123,XBOOLE_1:36;
then Aa=F.:S1 by A149;
then S\{a1}c=S & S1 in Xm1 by XBOOLE_1:36;
then [S,S1] in R1 by A32,A156;
then A165: S1 in R1.:{x} by A102,RELAT_1:def 13;
F.:S2 c=Aa by A99,RELAT_1:123,XBOOLE_1:36;
then Aa=F.:S2 by A158;
then S\{a2}c=S & S2 in Xm1 by XBOOLE_1:36;
then [S,S2] in R1 by A32,A156;
then S2 in R1.:{x} by A102,RELAT_1:def 13;
then {S1,S2}c=R1.:{x} by A165,ZFMISC_1:32;
then A166: R1.:{x}={S1,S2} by A118;
S1<>S2 by A111,ZFMISC_1:56;
then card(R1.:{x})=2 by A166,CARD_2:57;
hence thesis by RELAT_1:def 16;
end;
A167: M-1=m+-1 by XXREAL_3:def 2;
XX c=DY
proof
let x be object;
assume x in XX;
then consider S be Simplex of m,BCS(k,CA) such that
A168: x=S and
A169: F.:S=A by A3;
set FS=F|S;
A170: rng FS=A by A169,RELAT_1:115;
A171: card A=card S by A3,A95,A45,A96,SIMPLEX0:def 18;
A172: dom FS=S by A18,RELAT_1:62,SIMPLEX0:17;
then reconsider FS as Function of S,A by A170,FUNCT_2:1;
consider s be object such that
A173: s in dom FS & FS.s=a by A4,A170,FUNCT_1:def 3;
set Ss=S\{s};
FS is onto by A170,FUNCT_2:def 3;
then A174: FS is one-to-one by A171,FINSEQ_4:63;
then A175: FS.:Ss=FS.:S\FS.:{s} by FUNCT_1:64
.=A\FS.:{s} by A170,A172,RELAT_1:113
.=A\Im(FS,s) by RELAT_1:def 16
.=Aa by A173,FUNCT_1:59;
Ss,FS.:Ss are_equipotent by A172,A174,CARD_1:33,XBOOLE_1:36;
then A176: card Ss=m by A5,A175,CARD_1:5;
reconsider Ss as Simplex of BCS(k,CA);
reconsider Ss as Simplex of m-1,BCS(k,CA) by A167,A176,SIMPLEX0:48;
FS.:Ss=F.:Ss by RELAT_1:129,XBOOLE_1:36;
then A177: Ss in Xm1 by A175;
Ss c=S & S in Xm by XBOOLE_1:36;
then [S,Ss] in R1 by A32,A177;
then A178: S in dom R1 by XTUPLE_0:def 12;
for W be Simplex of m,BCS(k,CA) st S=W holds Aa<>F.:W by A4,A169,
ZFMISC_1:56;
then not S in YA;
hence thesis by A168,A178,XBOOLE_0:def 5;
end;
then A179: DY=XX by A33;
for x being object st x in DY holds card Im(RDY,x)=1
proof
let x be object;
assume A180: x in DY;
then consider y being object such that
A181: [x,y] in R1 by XTUPLE_0:def 12;
A182: ex W be Simplex of m,BCS(k,CA) st x=W & F.:W=A by A3,A179,A180;
x in Xm by A32,A181;
then consider S be Simplex of m,BCS(k,CA) such that
A183: x=S and
not contradiction;
y in Xm1 by A32,A181;
then consider W be Simplex of m-1,BCS(k,CA) such that
A184: y=W and
A185: Aa=F.:W;
A186: card S=m+1 by A95,A45,A96,SIMPLEX0:def 18;
A187: RDY.:{x}c={y}
proof
let u be object;
set FS=F|S;
assume u in RDY.:{x};
then consider s be object such that
A188: [s,u] in RDY and
A189: s in {x} by RELAT_1:def 13;
A190: [s,u] in R1 by A188,RELAT_1:def 11;
then u in Xm1 by A32;
then consider U be Simplex of m-1,BCS(k,CA) such that
A191: u=U and
A192: Aa=F.:U;
A193: dom FS=S by A18,RELAT_1:62,SIMPLEX0:17;
A194: rng FS=A by A182,A183,RELAT_1:115;
then reconsider FS as Function of S,A by A193,FUNCT_2:1;
P1[S,W] by A32,A181,A183,A184;
then
A195: W c=S;
then A196: FS.:W=F.:W by RELAT_1:129;
s=S by A183,A189,TARSKI:def 1;
then P1[S,U] by A32,A190,A191;
then A197: U c=S;
then A198: FS.:U=F.:U by RELAT_1:129;
FS is onto by A194,FUNCT_2:def 3;
then A199: FS is one-to-one by A3,A186,FINSEQ_4:63;
then A200: U c=W by A185,A192,A193,A196,A197,A198,FUNCT_1:87;
W c=U by A185,A192,A193,A195,A196,A198,A199,FUNCT_1:87;
then u=y by A184,A191,A200,XBOOLE_0:def 10;
hence thesis by TARSKI:def 1;
end;
x in {x} & [x,y] in RDY by A180,A181,RELAT_1:def 11,TARSKI:def 1;
then y in RDY.:{x} by RELAT_1:def 13;
then RDY.:{x}={y} by A187,ZFMISC_1:33;
then Im(RDY,x)={y} by RELAT_1:def 16;
hence thesis by CARD_1:30;
end;
then card RDY=card{}+`1*`card DY by A40,Th1
.=1*`card DY by CARD_2:18
.=card DY by CARD_2:21;
then A201: card R1=card card XX+`card(2*card YA) by A44,A97,A179,Th1
.=card(card XX+2*card YA) by CARD_2:38
.=card XX+2*card YA;
A202: |.BCS(k,CA).|=|.CA.| & |.CA.|=conv A by Th8,Th10;
A203: XXA c=XXa
proof
let x be object;
assume x in XXA;
then consider S be Simplex of m-1,BCS(k,CA) such that
A204: x=S and
A205: F.:S=Aa and
A206: conv@S misses Int A;
conv@S c=conv A by A202,Th5;
then consider B be Subset of V such that
A207: B c<A and
A208: conv@S c=conv B by A4,A206,RLAFFIN2:23;
A209: B c=A by A207;
then reconsider B as finite Subset of V;
card B<m+1 by A3,A207,CARD_2:48;
then A210: card B<=m by NAT_1:13;
A211: Aa c=B
proof
let y be object;
assume y in Aa;
then consider v be object such that
A212: v in dom F and
A213: v in S and
A214: F.v=y by A205,FUNCT_1:def 6;
S c=conv@S by RLAFFIN1:2;
then v in conv@S by A213;
hence thesis by A9,A208,A209,A212,A214;
end;
then card Aa<=card B by NAT_1:43;
then A215: Aa=B by A5,A210,A211,CARD_2:102,XXREAL_0:1;
A216: the topology of BCS(k,CAa)c=the topology of BCS(k,CA) by A14,
SIMPLEX0:def 13;
A217: card S=m by A95,A83,A71,A45,SIMPLEX0:def 18;
then S is non empty by A30;
then A218: (center_of_mass V).S in Int@S by RLAFFIN2:20;
Int@S c=conv@S by RLAFFIN2:5;
then (center_of_mass V).S in conv@S by A218;
then consider w be Subset of BCS(k,CAa) such that
A219: w is simplex-like and
A220: (center_of_mass V).S in conv@w by A65,A208,A215,Def3;
w in the topology of BCS(k,CAa) by A219;
then w in the topology of BCS(k,CA) by A216;
then reconsider W=w as Simplex of BCS(k,CA) by PRE_TOPC:def 2;
Int@S meets conv@W by A218,A220,XBOOLE_0:3;
then A221: S c=w by Th26;
then reconsider s=S as Subset of BCS(k,CAa) by XBOOLE_1:1;
reconsider s as Simplex of BCS(k,CAa) by A219,A221,MATROID0:1;
A222: FA.:s=Aa by A205,RELAT_1:129,SIMPLEX0:17;
s is Simplex of m-1,BCS(k,CAa) by A167,A217,SIMPLEX0:48;
hence thesis by A204,A222;
end;
A223: degree CAa=m-1 by A5,A167,SIMPLEX0:26;
XXa c=XXA
proof
A<>Aa by A3,A5;
then A224: Aa c<A by A12;
let x be object;
assume x in XXa;
then consider S be Simplex of m-1,BCS(k,CAa) such that
A225: x=S and
A226: FA.:S=Aa;
m-1<=degree BCS(k,CAa) by A7,A223,Th32;
then reconsider S1=x as Simplex of m-1,BCS(k,CA) by A14,A225,SIMPLEX0:49;
A227: FA.:S=F.:S by RELAT_1:129,SIMPLEX0:17;
conv@S c=conv Aa by A65,Th5;
then conv@S1 misses Int A by A224,A225,RLAFFIN2:7,XBOOLE_1:63;
hence thesis by A225,A226,A227;
end;
then A228: XXa=XXA by A203;
for x being object st x in DX holds card Im(RDX,x)=2
proof
let x be object;
assume A229: x in DX;
then ex y being object st[x,y] in R by XTUPLE_0:def 12;
then A230: x in Xm1 by A46;
then consider S be Simplex of m-1,BCS(k,CA) such that
A231: x=S and
A232: Aa=F.:S;
set XX={S1 where S1 is Simplex of m,BCS(k,CA):S c=S1};
not x in XXA by A229,XBOOLE_0:def 5;
then conv@S meets Int A by A231,A232;
then A233: card XX=2 by A3,Th45;
A234: RDX.:{S}c=XX
proof
let w be object;
reconsider ww=w as set by TARSKI:1;
assume w in RDX.:{S};
then consider s be object such that
A235: [s,w] in RDX and
A236: s in {S} by RELAT_1:def 13;
A237: [s,w] in R by A235,RELAT_1:def 11;
then w in Xm by A46;
then A238: ex W be Simplex of m,BCS(k,CA) st w=W;
s=S by A236,TARSKI:def 1;
then P[S,ww] by A46,A237;
then S c=ww;
hence thesis by A238;
end;
XX c=RDX.:{S}
proof
let w be object;
assume w in XX;
then consider W be Simplex of m,BCS(k,CA) such that
A239: w=W and
A240: S c=W;
W in Xm;
then [S,W] in R by A46,A230,A231,A240;
then A241: [S,W] in RDX by A229,A231,RELAT_1:def 11;
S in {S} by TARSKI:def 1;
hence thesis by A239,A241,RELAT_1:def 13;
end;
then XX=RDX.:{S} by A234;
hence thesis by A231,A233,RELAT_1:def 16;
end;
then card RDX=card(RDX|(dom RDX\DX))+`2*`card DX by Th1
.=0+`2*`card DX by A67
.=2*`card DX by CARD_2:18;
then A242: card R=2*`card DX+`1*`card XXA by A84,Th1
.=2*`card DX+`(2*n+1) by A82,A228,CARD_2:21
.=(card 2)*`card card DX+`(2*n+1)
.=card(2*card DX)+`(2*n+1) by CARD_2:39
.=card(2*card DX)+`card(2*n+1)
.=card(2*card DX+(2*n+1)) by CARD_2:38
.=2*card DX+(2*n+1);
then card XX=2*(card DX+n-card YA)+1 by A47,A201;
then 2*(card DX+n-card YA)>=-1 by INT_1:7;
then card DX+n-card YA>=(-1)/2 by XREAL_1:79;
then card DX+n-card YA>-1 by XXREAL_0:2;
then card DX+n-card YA>=0 by INT_1:8;
then reconsider cnc=card DX+n-card YA as Element of NAT by INT_1:3;
take cnc;
thus thesis by A47,A201,A242;
end;
end;
A243: P[0 qua Nat]
proof
let A be finite affinely-independent Subset of V such that
A244: card A=0;
A245: A={} by A244;
set C=Complex_of{A};
A246: |.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;
A247: k=0 or k>0;
A248: Z-1=-1 by XXREAL_3:4;
then degree C=-1 by A244,SIMPLEX0:26;
then A249: C=BCS(k,C) by A246,A247,Th16,Th22;
A250: the topology of C=bool A by SIMPLEX0:4;
A251: X c={A}
proof
let x be object such that
A252: x in X;
consider S be Simplex of card A-1,BCS(k,C) such that
A253: S=x and
F.:S=A by A252;
S in the topology of C by A249,PRE_TOPC:def 2;
then S is empty by A245,A250;
hence thesis by A245,A253,TARSKI:def 1;
end;
A in bool A by ZFMISC_1:def 1;
then reconsider A1=A as Simplex of C by A250,PRE_TOPC:def 2;
A254: F.:A1=A by A245;
A1 is Simplex of-1,C by A244,A248,SIMPLEX0:48;
then A in X by A249,A254;
then X={A} by A251,ZFMISC_1:33;
hence thesis by CARD_1:30;
end;
for k holds P[k] from NAT_1:sch 2(A243,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 being object such that
A1: x in XX;
ex S be Simplex of card Aff-1,BCS(k,Complex_of{Aff}) st x=S & F.:S=Aff by A1;
hence thesis;
end;