let k be Nat; for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1
let V be RealLinearSpace; for Aff being finite affinely-independent Subset of V
for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1
let Aff be finite affinely-independent Subset of V; for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1
reconsider O = 1 as ext-real number ;
reconsider Z = 0 as ext-real number ;
defpred S1[ Nat] means for A being finite affinely-independent Subset of V st card A = $1 holds
for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat 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 being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A2:
S1[
m]
;
S1[m + 1]
let A be
finite affinely-independent Subset of
V;
( card A = m + 1 implies for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )
assume A3:
card A = m + 1
;
for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1
not
A is
empty
by A3;
then consider a being
set such that A4:
a in A
by XBOOLE_0:def 1;
reconsider a =
a as
Element of
V by A4;
A5:
card (A \ {a}) = m
by A3, A4, STIRL2_1:65;
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
(Complex_of {Aa}) = bool Aa
by SIMPLEX0:4;
then A6:
Vertices (Complex_of {Aa}) =
union (bool Aa)
by SIMPLEX0:16
.=
Aa
by ZFMISC_1:99
;
A7:
(
[#] (Complex_of {Aa}) = [#] V &
|.(Complex_of {Aa}).| c= [#] V )
;
then A8:
Vertices (Complex_of {Aa}) c= Vertices (BCS (k,(Complex_of {Aa})))
by Th24;
set CA =
Complex_of {A};
let F be
Function of
(Vertices (BCS (k,(Complex_of {A})))),
A;
( ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) implies ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )
assume A9:
for
v being
Vertex of
(BCS (k,(Complex_of {A}))) for
B being
Subset of
V st
B c= A &
v in conv B holds
F . v in B
;
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1
set XX =
{ S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ;
A10:
{ S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } c= the
topology of
(BCS (k,(Complex_of {A})))
then reconsider XX =
{ S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } as
Subset-Family of
(BCS (k,(Complex_of {A}))) by XBOOLE_1:1;
reconsider XX =
XX as
simplex-like Subset-Family of
(BCS (k,(Complex_of {A}))) by A10, SIMPLEX0:14;
A11:
(
[#] (Complex_of {A}) = [#] V &
|.(Complex_of {A}).| c= [#] V )
;
A12:
A \ {a} c= A
by XBOOLE_1:36;
for
x being
set st
x in {Aa} holds
ex
y being
set st
(
y in {A} &
x c= y )
then
{Aa} is_finer_than {A}
by SETFAM_1:def 2;
then
Complex_of {Aa} is
SubSimplicialComplex of
Complex_of {A}
by SIMPLEX0:30;
then A14:
BCS (
k,
(Complex_of {Aa})) is
SubSimplicialComplex of
BCS (
k,
(Complex_of {A}))
by A11, A7, Th23;
then A15:
Vertices (BCS (k,(Complex_of {Aa}))) c= Vertices (BCS (k,(Complex_of {A})))
by SIMPLEX0:31;
A16:
the
topology of
(Complex_of {A}) = bool A
by SIMPLEX0:4;
then A17:
Vertices (Complex_of {A}) =
union (bool A)
by SIMPLEX0:16
.=
A
by ZFMISC_1:99
;
A18:
dom F = Vertices (BCS (k,(Complex_of {A})))
by A4, FUNCT_2:def 1;
per cases
( m = 0 or m > 0 )
;
suppose A19:
m = 0
;
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1A20:
O - 1
= 0
by XXREAL_3:7;
then A21:
degree (Complex_of {A}) = 0
by A3, A19, SIMPLEX0:26;
(
k = 0 or
k > 0 )
;
then A22:
BCS (
k,
(Complex_of {A}))
= Complex_of {A}
by A11, A21, Th16, Th22;
then A23:
dom F = Vertices (Complex_of {A})
by A4, FUNCT_2:def 1;
take
0
;
card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1
A in bool A
by ZFMISC_1:def 1;
then reconsider A1 =
A as
Simplex of
(Complex_of {A}) by A16, PRE_TOPC:def 5;
A24:
A1 is
Simplex of
0 ,
Complex_of {A}
by A3, A19, A20, SIMPLEX0:48;
ex
x being
set st
A = {x}
by A3, A19, CARD_2:60;
then A25:
A = {a}
by A4, TARSKI:def 1;
then
conv A = A
by RLAFFIN1:1;
then
F . a in A
by A4, A9, A17, A22;
then A26:
F . a = a
by A25, TARSKI:def 1;
A27:
XX c= {A}
F .: A =
Im (
F,
a)
by A25, RELAT_1:def 16
.=
A
by A4, A17, A23, A25, A26, FUNCT_1:117
;
then
A in XX
by A3, A19, A24, A22;
then
XX = {A}
by A27, ZFMISC_1:39;
hence
card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1
by CARD_1:50;
verum end; suppose A30:
m > 0
;
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1defpred S2[
set ,
set ]
means $1
c= $2;
set XXA =
{ S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ;
reconsider m1 =
m - 1 as
ext-real number ;
reconsider M =
m as
ext-real number ;
reconsider cA =
card A as
ext-real number ;
set YA =
{ S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } ;
A31:
{ S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } c= the
topology of
(BCS (k,(Complex_of {A})))
then reconsider YA =
{ S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } as
Subset-Family of
(BCS (k,(Complex_of {A}))) by XBOOLE_1:1;
reconsider YA =
YA as
simplex-like Subset-Family of
(BCS (k,(Complex_of {A}))) by A31, SIMPLEX0:14;
defpred S3[
set ,
set ]
means $2
c= $1;
set Xm1 =
{ S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ;
set Xm =
{ S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } ;
consider R1 being
Relation such that A32:
for
x,
y being
set holds
(
[x,y] in R1 iff (
x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } &
y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } &
S3[
x,
y] ) )
from RELAT_1:sch 1();
set DY =
(dom R1) \ YA;
A33:
(dom R1) \ YA c= XX
proof
let x be
set ;
TARSKI:def 3 ( not x in (dom R1) \ YA or x in XX )
assume A34:
x in (dom R1) \ YA
;
x in XX
then consider y being
set such that A35:
[x,y] in R1
by RELAT_1:def 4;
x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum }
by A32, A35;
then consider S being
Simplex of
m,
BCS (
k,
(Complex_of {A}))
such that A36:
x = S
and
verum
;
not
x in YA
by A34, XBOOLE_0:def 5;
then A37:
F .: S <> Aa
by A36;
y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S }
by A32, A35;
then A38:
ex
W being
Simplex of
m - 1,
BCS (
k,
(Complex_of {A})) st
(
y = W &
Aa = F .: W )
;
y c= x
by A32, A35;
then
Aa c= F .: S
by A36, A38, RELAT_1:156;
then
Aa c< F .: S
by A37, XBOOLE_0:def 8;
then
m < card (F .: S)
by A5, CARD_2:67;
then A39:
m + 1
<= card (F .: S)
by NAT_1:13;
card (F .: S) <= m + 1
by A3, NAT_1:44;
then
F .: S = A
by A3, A39, CARD_FIN:1, XXREAL_0:1;
hence
x in XX
by A3, A36;
verum
end; set RDY =
R1 | ((dom R1) \ YA);
A40:
(R1 | ((dom R1) \ YA)) | ((dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA)) = {}
A44: 2
*` (card YA) =
(card 2) *` (card (card YA))
by Lm1
.=
card (2 * (card YA))
by CARD_2:52
;
A45:
2
* (card YA) in NAT
by ORDINAL1:def 13;
cA - 1
= (m + 1) + (- 1)
by A3, XXREAL_3:def 2;
then A46:
degree (Complex_of {A}) = m
by SIMPLEX0:26;
consider R being
Relation such that A47:
for
x,
y being
set holds
(
[x,y] in R iff (
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } &
y in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } &
S2[
x,
y] ) )
from RELAT_1:sch 1();
A48:
card R = card R1
proof
deffunc H1(
set )
-> set =
[($1 `2),($1 `1)];
A49:
for
x being
set st
x in R holds
H1(
x)
in R1
proof
let z be
set ;
( z in R implies H1(z) in R1 )
assume A50:
z in R
;
H1(z) in R1
then
ex
x,
y being
set st
z = [x,y]
by RELAT_1:def 1;
then A51:
z = [(z `1),(z `2)]
by MCART_1:8;
then A52:
z `2 in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum }
by A47, A50;
(
S2[
z `1 ,
z `2 ] &
z `1 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } )
by A47, A50, A51;
hence
H1(
z)
in R1
by A32, A52;
verum
end;
consider f being
Function of
R,
R1 such that A53:
for
x being
set st
x in R holds
f . x = H1(
x)
from FUNCT_2:sch 2(A49);
per cases
( R1 is empty or not R1 is empty )
;
suppose
not
R1 is
empty
;
card R = card R1then A55:
dom f = R
by FUNCT_2:def 1;
R1 c= rng f
proof
let z be
set ;
TARSKI:def 3 ( not z in R1 or z in rng f )
assume A56:
z in R1
;
z in rng f
then
ex
x,
y being
set st
z = [x,y]
by RELAT_1:def 1;
then A57:
z = [(z `1),(z `2)]
by MCART_1:8;
then A58:
z `2 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S }
by A32, A56;
(
S3[
z `1 ,
z `2 ] &
z `1 in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } )
by A32, A56, A57;
then A59:
[(z `2),(z `1)] in R
by A47, A58;
[(z `2),(z `1)] `1 = z `2
by MCART_1:7;
then
H1(
[(z `2),(z `1)])
= z
by A57, MCART_1:7;
then
z = f . [(z `2),(z `1)]
by A53, A59;
hence
z in rng f
by A55, A59, FUNCT_1:def 5;
verum
end; then A60:
rng f = R1
by XBOOLE_0:def 10;
now let x1,
x2 be
set ;
( x1 in R & x2 in R & f . x1 = f . x2 implies x1 = x2 )assume that A61:
x1 in R
and A62:
x2 in R
and A63:
f . x1 = f . x2
;
x1 = x2
(
f . x1 = H1(
x1) &
f . x2 = H1(
x2) )
by A53, A61, A62;
then A64:
(
x1 `2 = x2 `2 &
x1 `1 = x2 `1 )
by A63, ZFMISC_1:33;
A65:
ex
x,
y being
set st
x2 = [x,y]
by A62, RELAT_1:def 1;
ex
x,
y being
set st
x1 = [x,y]
by A61, RELAT_1:def 1;
hence x1 =
[(x2 `1),(x2 `2)]
by A64, MCART_1:8
.=
x2
by A65, MCART_1:8
;
verum end; then
f is
one-to-one
by A55, FUNCT_1:def 8;
then
R,
R1 are_equipotent
by A55, A60, WELLORD2:def 4;
hence
card R = card R1
by CARD_1:21;
verum end;
end; A66:
(
|.(BCS (k,(Complex_of {Aa}))).| = |.(Complex_of {Aa}).| &
|.(Complex_of {Aa}).| = conv Aa )
by Th8, Th10;
set DX =
(dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ;
A67:
(dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } c= the
topology of
(BCS (k,(Complex_of {A})))
proof
let x be
set ;
TARSKI:def 3 ( not x in (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } or x in the topology of (BCS (k,(Complex_of {A}))) )
assume
x in (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }
;
x in the topology of (BCS (k,(Complex_of {A})))
then
ex
y being
set st
[x,y] in R
by RELAT_1:def 4;
then
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S }
by A47;
then
ex
S being
Simplex of
m - 1,
BCS (
k,
(Complex_of {A})) st
(
S = x &
Aa = F .: S )
;
hence
x in the
topology of
(BCS (k,(Complex_of {A})))
by PRE_TOPC:def 5;
verum
end; set RDX =
R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } );
reconsider DX =
(dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } as
Subset-Family of
(BCS (k,(Complex_of {A}))) by A67, XBOOLE_1:1;
reconsider DX =
DX as
simplex-like Subset-Family of
(BCS (k,(Complex_of {A}))) by A67, SIMPLEX0:14;
A68:
(R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX) = {}
proof
assume
(R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX) <> {}
;
contradiction
then consider xy being
set such that A69:
xy in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX)
by XBOOLE_0:def 1;
consider x,
y being
set such that A70:
xy = [x,y]
by A69, RELAT_1:def 1;
A71:
x in (dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX
by A69, A70, RELAT_1:def 11;
then
(
dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) c= DX &
x in dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) )
by RELAT_1:87;
hence
contradiction
by A71, XBOOLE_0:def 5;
verum
end; A72:
m1 + 1 =
(m - 1) + 1
by XXREAL_3:def 2
.=
m
;
set FA =
F | (Vertices (BCS (k,(Complex_of {Aa}))));
A73:
dom (F | (Vertices (BCS (k,(Complex_of {Aa}))))) = Vertices (BCS (k,(Complex_of {Aa})))
by A18, A14, RELAT_1:91, SIMPLEX0:31;
A74:
not
Vertices (BCS (k,(Complex_of {Aa}))) is
empty
by A5, A6, A8, A30;
A75:
for
v being
Vertex of
(BCS (k,(Complex_of {Aa}))) for
B being
Subset of
V st
B c= Aa &
v in conv B holds
(F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B
proof
let v be
Vertex of
(BCS (k,(Complex_of {Aa})));
for B being Subset of V st B c= Aa & v in conv B holds
(F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in Blet B be
Subset of
V;
( B c= Aa & v in conv B implies (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B )
assume A76:
(
B c= Aa &
v in conv B )
;
(F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B
v in Vertices (BCS (k,(Complex_of {Aa})))
by A74;
then
F . v in B
by A9, A12, A15, A76, XBOOLE_1:1;
hence
(F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B
by A73, A74, FUNCT_1:70;
verum
end;
rng (F | (Vertices (BCS (k,(Complex_of {Aa}))))) c= Aa
proof
let y be
set ;
TARSKI:def 3 ( not y in rng (F | (Vertices (BCS (k,(Complex_of {Aa}))))) or y in Aa )
assume
y in rng (F | (Vertices (BCS (k,(Complex_of {Aa})))))
;
y in Aa
then consider x being
set such that A77:
x in dom (F | (Vertices (BCS (k,(Complex_of {Aa})))))
and A78:
(F | (Vertices (BCS (k,(Complex_of {Aa}))))) . x = y
by FUNCT_1:def 5;
reconsider v =
x as
Element of
(BCS (k,(Complex_of {Aa}))) by A73, A77;
v is
vertex-like
by A73, A77, SIMPLEX0:def 4;
then consider S being
Subset of
(BCS (k,(Complex_of {Aa}))) such that A79:
not
S is
dependent
and A80:
v in S
by SIMPLEX0:def 3;
A81:
conv (@ S) c= |.(BCS (k,(Complex_of {Aa}))).|
by A79, Th5;
S c= conv (@ S)
by RLAFFIN1:2;
then A82:
v in conv (@ S)
by A80;
x in Vertices (BCS (k,(Complex_of {Aa})))
by A18, A14, A77, RELAT_1:91, SIMPLEX0:31;
hence
y in Aa
by A66, A75, A78, A81, A82;
verum
end; then reconsider FA =
F | (Vertices (BCS (k,(Complex_of {Aa})))) as
Function of
(Vertices (BCS (k,(Complex_of {Aa})))),
Aa by A73, FUNCT_2:4;
set XXa =
{ S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } ;
consider n being
Nat such that A83:
card { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } = (2 * n) + 1
by A2, A5, A75;
A84:
(
m - 1
<= m - 0 &
- 1
<= m + (- 1) )
by XREAL_1:12, XREAL_1:33;
A85:
for
x being
set st
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } holds
card (Im (R,x)) = 1
proof
let x be
set ;
( x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } implies card (Im (R,x)) = 1 )
assume
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }
;
card (Im (R,x)) = 1
then consider S being
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
such that A86:
x = S
and A87:
F .: S = Aa
and A88:
conv (@ S) misses Int A
;
set XX =
{ S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ;
A89:
R .: {S} c= { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
proof
let w be
set ;
TARSKI:def 3 ( not w in R .: {S} or w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } )
assume
w in R .: {S}
;
w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
then consider s being
set such that A90:
[s,w] in R
and A91:
s in {S}
by RELAT_1:def 13;
w in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum }
by A47, A90;
then A92:
ex
W being
Simplex of
m,
BCS (
k,
(Complex_of {A})) st
w = W
;
(
s = S &
s c= w )
by A47, A90, A91, TARSKI:def 1;
hence
w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
by A92;
verum
end;
{ S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } c= R .: {S}
proof
let w be
set ;
TARSKI:def 3 ( not w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } or w in R .: {S} )
assume
w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
;
w in R .: {S}
then consider W being
Simplex of
m,
BCS (
k,
(Complex_of {A}))
such that A93:
w = W
and A94:
S c= W
;
(
W in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } &
S in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } )
by A87;
then
(
S in {S} &
[S,W] in R )
by A47, A94, TARSKI:def 1;
hence
w in R .: {S}
by A93, RELAT_1:def 13;
verum
end;
then A95:
R .: {S} = { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
by A89, XBOOLE_0:def 10;
card { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = 1
by A3, A88, Th45;
hence
card (Im (R,x)) = 1
by A86, A95, RELAT_1:def 16;
verum
end; A96:
degree (Complex_of {A}) = degree (BCS (k,(Complex_of {A})))
by A11, Th32;
A97:
M + 1
= m + 1
by XXREAL_3:def 2;
A98:
for
x being
set st
x in YA holds
card (Im (R1,x)) = 2
proof
let x be
set ;
( x in YA implies card (Im (R1,x)) = 2 )
assume
x in YA
;
card (Im (R1,x)) = 2
then consider S being
Simplex of
m,
BCS (
k,
(Complex_of {A}))
such that A99:
x = S
and A100:
Aa = F .: S
;
set FS =
F | S;
A101:
rng (F | S) = Aa
by A100, RELAT_1:148;
A102:
not
Aa is
empty
by A5, A30;
A103:
S in {x}
by A99, TARSKI:def 1;
A104:
dom (F | S) = S
by A18, RELAT_1:91, SIMPLEX0:17;
A105:
card S = m + 1
by A96, A46, A97, SIMPLEX0:def 18;
reconsider FS =
F | S as
Function of
S,
Aa by A101, A104, FUNCT_2:3;
FS is
onto
by A101, FUNCT_2:def 3;
then consider b being
set such that A106:
b in Aa
and A107:
card (FS " {b}) = 2
and A108:
for
x being
set st
x in Aa &
x <> b holds
card (FS " {x}) = 1
by A5, A102, A105, Th2;
consider a1,
a2 being
set such that A109:
a1 <> a2
and A110:
FS " {b} = {a1,a2}
by A107, CARD_2:79;
reconsider S1 =
S \ {a1},
S2 =
S \ {a2} as
Simplex of
(BCS (k,(Complex_of {A}))) ;
A111:
a1 in {a1,a2}
by TARSKI:def 2;
then A112:
a1 in S2
by A109, A110, ZFMISC_1:64;
A114:
card S1 = m
by A105, A110, A111, STIRL2_1:65;
A115:
a2 in {a1,a2}
by TARSKI:def 2;
then A116:
card S2 = m
by A105, A110, STIRL2_1:65;
then reconsider S1 =
S1,
S2 =
S2 as
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
by A96, A84, A72, A46, A114, SIMPLEX0:def 18;
A117:
{a1} c= S
by A110, A111, ZFMISC_1:37;
A118:
FS . a2 = F . a2
by A104, A110, A115, FUNCT_1:70;
A119:
{a2} c= S
by A110, A115, ZFMISC_1:37;
A120:
R1 .: {x} c= {S1,S2}
proof
let Y be
set ;
TARSKI:def 3 ( not Y in R1 .: {x} or Y in {S1,S2} )
assume
Y in R1 .: {x}
;
Y in {S1,S2}
then consider X being
set such that A121:
[X,Y] in R1
and A122:
X in {x}
by RELAT_1:def 13;
Y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S }
by A32, A121;
then consider W being
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
such that A123:
Y = W
and A124:
Aa = F .: W
;
X = x
by A122, TARSKI:def 1;
then
W c= S
by A32, A99, A121, A123;
then A125:
Aa = FS .: W
by A124, RELAT_1:162;
then consider w being
set such that A126:
w in dom FS
and A127:
w in W
and A128:
FS . w = b
by A106, FUNCT_1:def 12;
A129:
{w} c= W
by A127, ZFMISC_1:37;
A130:
S \ {a1,a2} c= W
proof
let s be
set ;
TARSKI:def 3 ( not s in S \ {a1,a2} or s in W )
assume A131:
s in S \ {a1,a2}
;
s in W
then A132:
s in dom FS
by A104, XBOOLE_0:def 5;
then A133:
FS . s in Aa
by A101, FUNCT_1:def 5;
then consider w being
set such that A134:
w in dom FS
and A135:
w in W
and A136:
FS . w = FS . s
by A125, FUNCT_1:def 12;
not
s in FS " {b}
by A110, A131, XBOOLE_0:def 5;
then
not
FS . s in {b}
by A132, FUNCT_1:def 13;
then
FS . s <> b
by TARSKI:def 1;
then
card (FS " {(FS . s)}) = 1
by A108, A133;
then consider z being
set such that A137:
FS " {(FS . s)} = {z}
by CARD_2:60;
A138:
FS . s in {(FS . s)}
by TARSKI:def 1;
then A139:
s in FS " {(FS . s)}
by A132, FUNCT_1:def 13;
w in FS " {(FS . s)}
by A134, A136, A138, FUNCT_1:def 13;
then
w = z
by A137, TARSKI:def 1;
hence
s in W
by A135, A137, A139, TARSKI:def 1;
verum
end;
b in {b}
by TARSKI:def 1;
then A140:
w in FS " {b}
by A126, A128, FUNCT_1:def 13;
A141:
card W = m
by A96, A84, A72, A46, SIMPLEX0:def 18;
A142:
S /\ {a1} = {a1}
by A117, XBOOLE_1:28;
A143:
S /\ {a2} = {a2}
by A119, XBOOLE_1:28;
per cases
( w = a1 or w = a2 )
by A110, A140, TARSKI:def 2;
suppose
w = a1
;
Y in {S1,S2}then (S \ {a1,a2}) \/ {w} =
S \ ({a1,a2} \ {a1})
by A142, XBOOLE_1:52
.=
S2
by A109, ZFMISC_1:23
;
then
S2 = W
by A116, A129, A130, A141, CARD_FIN:1, XBOOLE_1:8;
hence
Y in {S1,S2}
by A123, TARSKI:def 2;
verum end; suppose
w = a2
;
Y in {S1,S2}then (S \ {a1,a2}) \/ {w} =
S \ ({a1,a2} \ {a2})
by A143, XBOOLE_1:52
.=
S1
by A109, ZFMISC_1:23
;
then
S1 = W
by A114, A129, A130, A141, CARD_FIN:1, XBOOLE_1:8;
hence
Y in {S1,S2}
by A123, TARSKI:def 2;
verum end;
end;
A144:
S c= dom F
by A18, SIMPLEX0:17;
A145:
FS . a1 = F . a1
by A104, A110, A111, FUNCT_1:70;
A146:
FS . a1 in {b}
by A110, A111, FUNCT_1:def 13;
then A147:
FS . a1 = b
by TARSKI:def 1;
A148:
FS . a2 in {b}
by A110, A115, FUNCT_1:def 13;
then A149:
FS . a2 = b
by TARSKI:def 1;
A150:
(
a2 in S &
a2 in S1 )
by A109, A110, A115, ZFMISC_1:64;
A151:
Aa c= F .: S1
A158:
S in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum }
;
A159:
(
a1 in S &
a1 in S2 )
by A109, A110, A111, ZFMISC_1:64;
A160:
Aa c= F .: S2
F .: S1 c= Aa
by A100, RELAT_1:156, XBOOLE_1:36;
then
Aa = F .: S1
by A151, XBOOLE_0:def 10;
then
(
S \ {a1} c= S &
S1 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } )
by XBOOLE_1:36;
then
[S,S1] in R1
by A32, A158;
then A167:
S1 in R1 .: {x}
by A103, RELAT_1:def 13;
F .: S2 c= Aa
by A100, RELAT_1:156, XBOOLE_1:36;
then
Aa = F .: S2
by A160, XBOOLE_0:def 10;
then
(
S \ {a2} c= S &
S2 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } )
by XBOOLE_1:36;
then
[S,S2] in R1
by A32, A158;
then
S2 in R1 .: {x}
by A103, RELAT_1:def 13;
then
{S1,S2} c= R1 .: {x}
by A167, ZFMISC_1:38;
then A168:
R1 .: {x} = {S1,S2}
by A120, XBOOLE_0:def 10;
S1 <> S2
by A112, ZFMISC_1:64;
then
card (R1 .: {x}) = 2
by A168, CARD_2:76;
hence
card (Im (R1,x)) = 2
by RELAT_1:def 16;
verum
end; A169:
M - 1
= m + (- 1)
by XXREAL_3:def 2;
XX c= (dom R1) \ YA
proof
let x be
set ;
TARSKI:def 3 ( not x in XX or x in (dom R1) \ YA )
assume
x in XX
;
x in (dom R1) \ YA
then consider S being
Simplex of
m,
BCS (
k,
(Complex_of {A}))
such that A170:
x = S
and A171:
F .: S = A
by A3;
set FS =
F | S;
A172:
rng (F | S) = A
by A171, RELAT_1:148;
A173:
card A = card S
by A3, A96, A46, A97, SIMPLEX0:def 18;
A174:
dom (F | S) = S
by A18, RELAT_1:91, SIMPLEX0:17;
then reconsider FS =
F | S as
Function of
S,
A by A172, FUNCT_2:3;
consider s being
set such that A175:
(
s in dom FS &
FS . s = a )
by A4, A172, FUNCT_1:def 5;
set Ss =
S \ {s};
FS is
onto
by A172, FUNCT_2:def 3;
then A176:
FS is
one-to-one
by A173, STIRL2_1:70;
then A177:
FS .: (S \ {s}) =
(FS .: S) \ (FS .: {s})
by FUNCT_1:123
.=
A \ (FS .: {s})
by A172, A174, RELAT_1:146
.=
A \ (Im (FS,s))
by RELAT_1:def 16
.=
Aa
by A175, FUNCT_1:117
;
S \ {s},
FS .: (S \ {s}) are_equipotent
by A174, A176, CARD_1:60, XBOOLE_1:36;
then A178:
card (S \ {s}) = m
by A5, A177, CARD_1:21;
reconsider Ss =
S \ {s} as
Simplex of
(BCS (k,(Complex_of {A}))) ;
reconsider Ss =
Ss as
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
by A169, A178, SIMPLEX0:48;
FS .: Ss = F .: Ss
by RELAT_1:162, XBOOLE_1:36;
then A179:
Ss in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S }
by A177;
(
Ss c= S &
S in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } )
by XBOOLE_1:36;
then
[S,Ss] in R1
by A32, A179;
then A180:
S in dom R1
by RELAT_1:def 4;
for
W being
Simplex of
m,
BCS (
k,
(Complex_of {A})) st
S = W holds
Aa <> F .: W
by A4, A171, ZFMISC_1:64;
then
not
S in YA
;
hence
x in (dom R1) \ YA
by A170, A180, XBOOLE_0:def 5;
verum
end; then A181:
(dom R1) \ YA = XX
by A33, XBOOLE_0:def 10;
for
x being
set st
x in (dom R1) \ YA holds
card (Im ((R1 | ((dom R1) \ YA)),x)) = 1
proof
let x be
set ;
( x in (dom R1) \ YA implies card (Im ((R1 | ((dom R1) \ YA)),x)) = 1 )
assume A182:
x in (dom R1) \ YA
;
card (Im ((R1 | ((dom R1) \ YA)),x)) = 1
then consider y being
set such that A183:
[x,y] in R1
by RELAT_1:def 4;
A184:
ex
W being
Simplex of
m,
BCS (
k,
(Complex_of {A})) st
(
x = W &
F .: W = A )
by A3, A181, A182;
x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum }
by A32, A183;
then consider S being
Simplex of
m,
BCS (
k,
(Complex_of {A}))
such that A185:
x = S
and
verum
;
y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S }
by A32, A183;
then consider W being
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
such that A186:
y = W
and A187:
Aa = F .: W
;
A188:
card S = m + 1
by A96, A46, A97, SIMPLEX0:def 18;
A189:
(R1 | ((dom R1) \ YA)) .: {x} c= {y}
proof
let u be
set ;
TARSKI:def 3 ( not u in (R1 | ((dom R1) \ YA)) .: {x} or u in {y} )
set FS =
F | S;
assume
u in (R1 | ((dom R1) \ YA)) .: {x}
;
u in {y}
then consider s being
set such that A190:
[s,u] in R1 | ((dom R1) \ YA)
and A191:
s in {x}
by RELAT_1:def 13;
A192:
[s,u] in R1
by A190, RELAT_1:def 11;
then
u in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S }
by A32;
then consider U being
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
such that A193:
u = U
and A194:
Aa = F .: U
;
A195:
dom (F | S) = S
by A18, RELAT_1:91, SIMPLEX0:17;
A196:
rng (F | S) = A
by A184, A185, RELAT_1:148;
then reconsider FS =
F | S as
Function of
S,
A by A195, FUNCT_2:3;
A197:
W c= S
by A32, A183, A185, A186;
then A198:
FS .: W = F .: W
by RELAT_1:162;
s = S
by A185, A191, TARSKI:def 1;
then A199:
U c= S
by A32, A192, A193;
then A200:
FS .: U = F .: U
by RELAT_1:162;
FS is
onto
by A196, FUNCT_2:def 3;
then A201:
FS is
one-to-one
by A3, A188, STIRL2_1:70;
then A202:
U c= W
by A187, A194, A195, A198, A199, A200, FUNCT_1:157;
W c= U
by A187, A194, A195, A197, A198, A200, A201, FUNCT_1:157;
then
u = y
by A186, A193, A202, XBOOLE_0:def 10;
hence
u in {y}
by TARSKI:def 1;
verum
end;
(
x in {x} &
[x,y] in R1 | ((dom R1) \ YA) )
by A182, A183, RELAT_1:def 11, TARSKI:def 1;
then
y in (R1 | ((dom R1) \ YA)) .: {x}
by RELAT_1:def 13;
then
(R1 | ((dom R1) \ YA)) .: {x} = {y}
by A189, ZFMISC_1:39;
then
Im (
(R1 | ((dom R1) \ YA)),
x)
= {y}
by RELAT_1:def 16;
hence
card (Im ((R1 | ((dom R1) \ YA)),x)) = 1
by CARD_1:50;
verum
end; then card (R1 | ((dom R1) \ YA)) =
(card {}) +` (1 *` (card ((dom R1) \ YA)))
by A40, Th1
.=
1
*` (card ((dom R1) \ YA))
by CARD_2:29
.=
card ((dom R1) \ YA)
by CARD_2:33
;
then A203:
card R1 =
(card (card XX)) +` (card (2 * (card YA)))
by A44, A98, A181, Th1
.=
card ((card XX) + (2 * (card YA)))
by A45, CARD_2:51
.=
(card XX) + (2 * (card YA))
by Lm1
;
A204:
(
|.(BCS (k,(Complex_of {A}))).| = |.(Complex_of {A}).| &
|.(Complex_of {A}).| = conv A )
by Th8, Th10;
A205:
{ S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } c= { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa }
proof
let x be
set ;
TARSKI:def 3 ( not x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } or x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } )
assume
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }
;
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa }
then consider S being
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
such that A206:
x = S
and A207:
F .: S = Aa
and A208:
conv (@ S) misses Int A
;
A209:
dom (F | S) = S
by A18, RELAT_1:91, SIMPLEX0:17;
conv (@ S) c= conv A
by A204, Th5;
then consider B being
Subset of
V such that A210:
B c< A
and A211:
conv (@ S) c= conv B
by A4, A208, RLAFFIN2:23;
A212:
B c= A
by A210, XBOOLE_0:def 8;
then reconsider B =
B as
finite Subset of
V ;
card B < m + 1
by A3, A210, CARD_2:67;
then A213:
card B <= m
by NAT_1:13;
A214:
Aa c= B
then
card Aa <= card B
by NAT_1:44;
then A218:
Aa = B
by A5, A213, A214, CARD_FIN:1, XXREAL_0:1;
A219:
the
topology of
(BCS (k,(Complex_of {Aa}))) c= the
topology of
(BCS (k,(Complex_of {A})))
by A14, SIMPLEX0:def 13;
A220:
card S = m
by A96, A84, A72, A46, SIMPLEX0:def 18;
then
not
S is
empty
by A30;
then A221:
(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 A221;
then consider w being
Subset of
(BCS (k,(Complex_of {Aa}))) such that A222:
not
w is
dependent
and A223:
(center_of_mass V) . S in conv (@ w)
by A66, A211, A218, Def3;
w in the
topology of
(BCS (k,(Complex_of {Aa})))
by A222, PRE_TOPC:def 5;
then
w in the
topology of
(BCS (k,(Complex_of {A})))
by A219;
then reconsider W =
w as
Simplex of
(BCS (k,(Complex_of {A}))) by PRE_TOPC:def 5;
Int (@ S) meets conv (@ W)
by A221, A223, XBOOLE_0:3;
then A224:
S c= w
by Th26;
then reconsider s =
S as
Subset of
(BCS (k,(Complex_of {Aa}))) by XBOOLE_1:1;
reconsider s =
s as
Simplex of
(BCS (k,(Complex_of {Aa}))) by A222, A224, MATROID0:1;
A225:
FA .: s = Aa
by A207, RELAT_1:162, SIMPLEX0:17;
s is
Simplex of
m - 1,
BCS (
k,
(Complex_of {Aa}))
by A169, A220, SIMPLEX0:48;
hence
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa }
by A206, A225;
verum
end; A226:
degree (Complex_of {Aa}) = m - 1
by A5, A169, SIMPLEX0:26;
{ S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } c= { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }
proof
A <> Aa
by A3, A5;
then A227:
Aa c< A
by A12, XBOOLE_0:def 8;
let x be
set ;
TARSKI:def 3 ( not x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } or x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )
assume
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa }
;
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }
then consider S being
Simplex of
m - 1,
BCS (
k,
(Complex_of {Aa}))
such that A228:
x = S
and A229:
FA .: S = Aa
;
m - 1
<= degree (BCS (k,(Complex_of {Aa})))
by A7, A226, Th32;
then reconsider S1 =
x as
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
by A14, A228, SIMPLEX0:49;
A230:
FA .: S = F .: S
by RELAT_1:162, SIMPLEX0:17;
conv (@ S) c= conv Aa
by A66, Th5;
then
conv (@ S1) misses Int A
by A227, A228, RLAFFIN2:7, XBOOLE_1:63;
hence
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }
by A228, A229, A230;
verum
end; then A231:
{ S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } = { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }
by A205, XBOOLE_0:def 10;
A232:
(
(2 * n) + 1
in NAT & 2
* (card DX) in NAT )
by ORDINAL1:def 13;
for
x being
set st
x in DX holds
card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2
proof
let x be
set ;
( x in DX implies card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2 )
assume A233:
x in DX
;
card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2
then
ex
y being
set st
[x,y] in R
by RELAT_1:def 4;
then A234:
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S }
by A47;
then consider S being
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
such that A235:
x = S
and A236:
Aa = F .: S
;
set XX =
{ S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ;
not
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }
by A233, XBOOLE_0:def 5;
then
conv (@ S) meets Int A
by A235, A236;
then A237:
card { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = 2
by A3, Th45;
A238:
(R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} c= { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
proof
let w be
set ;
TARSKI:def 3 ( not w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} or w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } )
assume
w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}
;
w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
then consider s being
set such that A239:
[s,w] in R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )
and A240:
s in {S}
by RELAT_1:def 13;
A241:
[s,w] in R
by A239, RELAT_1:def 11;
then
w in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum }
by A47;
then A242:
ex
W being
Simplex of
m,
BCS (
k,
(Complex_of {A})) st
w = W
;
s = S
by A240, TARSKI:def 1;
then
S c= w
by A47, A241;
hence
w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
by A242;
verum
end;
{ S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } c= (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}
proof
let w be
set ;
TARSKI:def 3 ( not w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } or w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} )
assume
w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
;
w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}
then consider W being
Simplex of
m,
BCS (
k,
(Complex_of {A}))
such that A243:
w = W
and A244:
S c= W
;
W in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum }
;
then
[S,W] in R
by A47, A234, A235, A244;
then A245:
[S,W] in R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )
by A233, A235, RELAT_1:def 11;
S in {S}
by TARSKI:def 1;
hence
w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}
by A243, A245, RELAT_1:def 13;
verum
end;
then
{ S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}
by A238, XBOOLE_0:def 10;
hence
card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2
by A235, A237, RELAT_1:def 16;
verum
end; then card (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) =
(card ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX))) +` (2 *` (card DX))
by Th1
.=
0 +` (2 *` (card DX))
by A68
.=
2
*` (card DX)
by CARD_2:29
;
then A246:
card R =
(2 *` (card DX)) +` (1 *` (card { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))
by A85, Th1
.=
(2 *` (card DX)) +` ((2 * n) + 1)
by A83, A231, CARD_2:33
.=
((card 2) *` (card (card DX))) +` ((2 * n) + 1)
by Lm1
.=
(card (2 * (card DX))) +` ((2 * n) + 1)
by CARD_2:52
.=
(card (2 * (card DX))) +` (card ((2 * n) + 1))
by Lm1
.=
card ((2 * (card DX)) + ((2 * n) + 1))
by A232, CARD_2:51
.=
(2 * (card DX)) + ((2 * n) + 1)
by Lm1
;
then
card XX = (2 * (((card DX) + n) - (card YA))) + 1
by A48, A203;
then
2
* (((card DX) + n) - (card YA)) >= - 1
by INT_1:20;
then
((card DX) + n) - (card YA) >= (- 1) / 2
by XREAL_1:81;
then
((card DX) + n) - (card YA) > - 1
by XXREAL_0:2;
then
((card DX) + n) - (card YA) >= 0
by INT_1:21;
then reconsider cnc =
((card DX) + n) - (card YA) as
Element of
NAT by INT_1:16;
take
cnc
;
card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * cnc) + 1thus
card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * cnc) + 1
by A48, A203, A246;
verum end;
end;
A247:
S1[ 0 ]
proof
let A be
finite affinely-independent Subset of
V;
( card A = 0 implies for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )
assume A248:
card A = 0
;
for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1
A249:
A = {}
by A248;
set C =
Complex_of {A};
A250:
(
|.(Complex_of {A}).| c= [#] V &
[#] (Complex_of {A}) = [#] V )
;
let F be
Function of
(Vertices (BCS (k,(Complex_of {A})))),
A;
( ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) implies ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )
assume
for
v being
Vertex of
(BCS (k,(Complex_of {A}))) for
B being
Subset of
V st
B c= A &
v in conv B holds
F . v in B
;
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1
set X =
{ S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ;
take
0
;
card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1
A251:
(
k = 0 or
k > 0 )
;
A252:
Z - 1
= - 1
by XXREAL_3:4;
then
degree (Complex_of {A}) = - 1
by A248, SIMPLEX0:26;
then A253:
Complex_of {A} = BCS (
k,
(Complex_of {A}))
by A250, A251, Th16, Th22;
A254:
the
topology of
(Complex_of {A}) = bool A
by SIMPLEX0:4;
A255:
{ S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } c= {A}
proof
let x be
set ;
TARSKI:def 3 ( not x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } or x in {A} )
assume A256:
x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A }
;
x in {A}
consider S being
Simplex of
(card A) - 1,
BCS (
k,
(Complex_of {A}))
such that A257:
S = x
and
F .: S = A
by A256;
S in the
topology of
(Complex_of {A})
by A253, PRE_TOPC:def 5;
then
S is
empty
by A249, A254;
hence
x in {A}
by A249, A257, TARSKI:def 1;
verum
end;
A in bool A
by ZFMISC_1:def 1;
then reconsider A1 =
A as
Simplex of
(Complex_of {A}) by A254, PRE_TOPC:def 5;
A258:
F .: A1 = A
by A249;
A1 is
Simplex of
- 1,
Complex_of {A}
by A248, A252, SIMPLEX0:48;
then
A in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A }
by A248, A253, A258;
then
{ S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = {A}
by A255, ZFMISC_1:39;
hence
card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1
by CARD_1:50;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A247, A1);
hence
for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1
; verum