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: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
(Complex_of {Aa}) = bool Aa
by SIMPLEX0:4;
then A6:
Vertices (Complex_of {Aa}) =
union (bool Aa)
by SIMPLEX0:16
.=
Aa
by ZFMISC_1:81
;
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:81
;
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 2;
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: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}
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
card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1
by CARD_1:30;
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:123;
then
Aa c< F .: S
by A37, XBOOLE_0:def 8;
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_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:39
;
A45:
2
* (card YA) in NAT
by ORDINAL1:def 12;
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 3;
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:27;
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 4;
then
R,
R1 are_equipotent
by A55, A60, WELLORD2:def 4;
hence
card R = card R1
by CARD_1:5;
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 2;
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:58;
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:62, 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:47;
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 3;
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:62, 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:2;
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:10, XREAL_1:31;
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:115;
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:62, 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:1;
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:60;
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:56;
A113:
card S1 = m
by A105, A110, A111, STIRL2_1:55;
A114:
a2 in {a1,a2}
by TARSKI:def 2;
then A115:
card S2 = m
by A105, A110, STIRL2_1:55;
then reconsider S1 =
S1,
S2 =
S2 as
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
by A96, A84, A72, A46, A113, SIMPLEX0:def 18;
A116:
{a1} c= S
by A110, A111, ZFMISC_1:31;
A117:
FS . a2 = F . a2
by A104, A110, A114, FUNCT_1:47;
A118:
{a2} c= S
by A110, A114, ZFMISC_1:31;
A119:
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 A120:
[X,Y] in R1
and A121:
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, A120;
then consider W being
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
such that A122:
Y = W
and A123:
Aa = F .: W
;
X = x
by A121, TARSKI:def 1;
then
W c= S
by A32, A99, A120, A122;
then A124:
Aa = FS .: W
by A123, RELAT_1:129;
then consider w being
set such that A125:
w in dom FS
and A126:
w in W
and A127:
FS . w = b
by A106, FUNCT_1:def 6;
A128:
{w} c= W
by A126, ZFMISC_1:31;
A129:
S \ {a1,a2} c= W
proof
let s be
set ;
TARSKI:def 3 ( not s in S \ {a1,a2} or s in W )
assume A130:
s in S \ {a1,a2}
;
s in W
then A131:
s in dom FS
by A104, XBOOLE_0:def 5;
then A132:
FS . s in Aa
by A101, FUNCT_1:def 3;
then consider w being
set such that A133:
w in dom FS
and A134:
w in W
and A135:
FS . w = FS . s
by A124, FUNCT_1:def 6;
not
s in FS " {b}
by A110, A130, XBOOLE_0:def 5;
then
not
FS . s in {b}
by A131, FUNCT_1:def 7;
then
FS . s <> b
by TARSKI:def 1;
then
card (FS " {(FS . s)}) = 1
by A108, A132;
then consider z being
set such that A136:
FS " {(FS . s)} = {z}
by CARD_2:42;
A137:
FS . s in {(FS . s)}
by TARSKI:def 1;
then A138:
s in FS " {(FS . s)}
by A131, FUNCT_1:def 7;
w in FS " {(FS . s)}
by A133, A135, A137, FUNCT_1:def 7;
then
w = z
by A136, TARSKI:def 1;
hence
s in W
by A134, A136, A138, TARSKI:def 1;
verum
end;
b in {b}
by TARSKI:def 1;
then A139:
w in FS " {b}
by A125, A127, FUNCT_1:def 7;
A140:
card W = m
by A96, A84, A72, A46, SIMPLEX0:def 18;
A141:
S /\ {a1} = {a1}
by A116, XBOOLE_1:28;
A142:
S /\ {a2} = {a2}
by A118, XBOOLE_1:28;
per cases
( w = a1 or w = a2 )
by A110, A139, TARSKI:def 2;
suppose
w = a1
;
Y in {S1,S2}then (S \ {a1,a2}) \/ {w} =
S \ ({a1,a2} \ {a1})
by A141, XBOOLE_1:52
.=
S2
by A109, ZFMISC_1:17
;
then
S2 = W
by A115, A128, A129, A140, CARD_FIN:1, XBOOLE_1:8;
hence
Y in {S1,S2}
by A122, TARSKI:def 2;
verum end; suppose
w = a2
;
Y in {S1,S2}then (S \ {a1,a2}) \/ {w} =
S \ ({a1,a2} \ {a2})
by A142, XBOOLE_1:52
.=
S1
by A109, ZFMISC_1:17
;
then
S1 = W
by A113, A128, A129, A140, CARD_FIN:1, XBOOLE_1:8;
hence
Y in {S1,S2}
by A122, TARSKI:def 2;
verum end;
end;
A143:
S c= dom F
by A18, SIMPLEX0:17;
A144:
FS . a1 = F . a1
by A104, A110, A111, FUNCT_1:47;
A145:
FS . a1 in {b}
by A110, A111, FUNCT_1:def 7;
then A146:
FS . a1 = b
by TARSKI:def 1;
A147:
FS . a2 in {b}
by A110, A114, FUNCT_1:def 7;
then A148:
FS . a2 = b
by TARSKI:def 1;
A149:
(
a2 in S &
a2 in S1 )
by A109, A110, A114, ZFMISC_1:56;
A150:
Aa c= F .: S1
A157:
S in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum }
;
A158:
(
a1 in S &
a1 in S2 )
by A109, A110, A111, ZFMISC_1:56;
A159:
Aa c= F .: S2
F .: S1 c= Aa
by A100, RELAT_1:123, XBOOLE_1:36;
then
Aa = F .: S1
by A150, 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, A157;
then A166:
S1 in R1 .: {x}
by A103, RELAT_1:def 13;
F .: S2 c= Aa
by A100, RELAT_1:123, XBOOLE_1:36;
then
Aa = F .: S2
by A159, 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, A157;
then
S2 in R1 .: {x}
by A103, RELAT_1:def 13;
then
{S1,S2} c= R1 .: {x}
by A166, ZFMISC_1:32;
then A167:
R1 .: {x} = {S1,S2}
by A119, XBOOLE_0:def 10;
S1 <> S2
by A112, ZFMISC_1:56;
then
card (R1 .: {x}) = 2
by A167, CARD_2:57;
hence
card (Im (R1,x)) = 2
by RELAT_1:def 16;
verum
end; A168:
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 A169:
x = S
and A170:
F .: S = A
by A3;
set FS =
F | S;
A171:
rng (F | S) = A
by A170, RELAT_1:115;
A172:
card A = card S
by A3, A96, A46, A97, SIMPLEX0:def 18;
A173:
dom (F | S) = S
by A18, RELAT_1:62, SIMPLEX0:17;
then reconsider FS =
F | S as
Function of
S,
A by A171, FUNCT_2:1;
consider s being
set such that A174:
(
s in dom FS &
FS . s = a )
by A4, A171, FUNCT_1:def 3;
set Ss =
S \ {s};
FS is
onto
by A171, FUNCT_2:def 3;
then A175:
FS is
one-to-one
by A172, STIRL2_1:60;
then A176:
FS .: (S \ {s}) =
(FS .: S) \ (FS .: {s})
by FUNCT_1:64
.=
A \ (FS .: {s})
by A171, A173, RELAT_1:113
.=
A \ (Im (FS,s))
by RELAT_1:def 16
.=
Aa
by A174, FUNCT_1:59
;
S \ {s},
FS .: (S \ {s}) are_equipotent
by A173, A175, CARD_1:33, XBOOLE_1:36;
then A177:
card (S \ {s}) = m
by A5, A176, CARD_1:5;
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 A168, A177, SIMPLEX0:48;
FS .: Ss = F .: Ss
by RELAT_1:129, XBOOLE_1:36;
then A178:
Ss in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S }
by A176;
(
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, A178;
then A179:
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, A170, ZFMISC_1:56;
then
not
S in YA
;
hence
x in (dom R1) \ YA
by A169, A179, XBOOLE_0:def 5;
verum
end; then A180:
(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 A181:
x in (dom R1) \ YA
;
card (Im ((R1 | ((dom R1) \ YA)),x)) = 1
then consider y being
set such that A182:
[x,y] in R1
by RELAT_1:def 4;
A183:
ex
W being
Simplex of
m,
BCS (
k,
(Complex_of {A})) st
(
x = W &
F .: W = A )
by A3, A180, A181;
x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum }
by A32, A182;
then consider S being
Simplex of
m,
BCS (
k,
(Complex_of {A}))
such that A184:
x = S
and
verum
;
y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S }
by A32, A182;
then consider W being
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
such that A185:
y = W
and A186:
Aa = F .: W
;
A187:
card S = m + 1
by A96, A46, A97, SIMPLEX0:def 18;
A188:
(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 A189:
[s,u] in R1 | ((dom R1) \ YA)
and A190:
s in {x}
by RELAT_1:def 13;
A191:
[s,u] in R1
by A189, 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 A192:
u = U
and A193:
Aa = F .: U
;
A194:
dom (F | S) = S
by A18, RELAT_1:62, SIMPLEX0:17;
A195:
rng (F | S) = A
by A183, A184, RELAT_1:115;
then reconsider FS =
F | S as
Function of
S,
A by A194, FUNCT_2:1;
A196:
W c= S
by A32, A182, A184, A185;
then A197:
FS .: W = F .: W
by RELAT_1:129;
s = S
by A184, A190, TARSKI:def 1;
then A198:
U c= S
by A32, A191, A192;
then A199:
FS .: U = F .: U
by RELAT_1:129;
FS is
onto
by A195, FUNCT_2:def 3;
then A200:
FS is
one-to-one
by A3, A187, STIRL2_1:60;
then A201:
U c= W
by A186, A193, A194, A197, A198, A199, FUNCT_1:87;
W c= U
by A186, A193, A194, A196, A197, A199, A200, FUNCT_1:87;
then
u = y
by A185, A192, A201, 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 A181, A182, 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 A188, ZFMISC_1:33;
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:30;
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:18
.=
card ((dom R1) \ YA)
by CARD_2:21
;
then A202:
card R1 =
(card (card XX)) +` (card (2 * (card YA)))
by A44, A98, A180, Th1
.=
card ((card XX) + (2 * (card YA)))
by A45, CARD_2:38
.=
(card XX) + (2 * (card YA))
by Lm1
;
A203:
(
|.(BCS (k,(Complex_of {A}))).| = |.(Complex_of {A}).| &
|.(Complex_of {A}).| = conv A )
by Th8, Th10;
A204:
{ 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 A205:
x = S
and A206:
F .: S = Aa
and A207:
conv (@ S) misses Int A
;
conv (@ S) c= conv A
by A203, Th5;
then consider B being
Subset of
V such that A209:
B c< A
and A210:
conv (@ S) c= conv B
by A4, A207, RLAFFIN2:23;
A211:
B c= A
by A209, XBOOLE_0:def 8;
then reconsider B =
B as
finite Subset of
V ;
card B < m + 1
by A3, A209, CARD_2:48;
then A212:
card B <= m
by NAT_1:13;
A213:
Aa c= B
then
card Aa <= card B
by NAT_1:43;
then A217:
Aa = B
by A5, A212, A213, CARD_FIN:1, XXREAL_0:1;
A218:
the
topology of
(BCS (k,(Complex_of {Aa}))) c= the
topology of
(BCS (k,(Complex_of {A})))
by A14, SIMPLEX0:def 13;
A219:
card S = m
by A96, A84, A72, A46, SIMPLEX0:def 18;
then
not
S is
empty
by A30;
then A220:
(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 A220;
then consider w being
Subset of
(BCS (k,(Complex_of {Aa}))) such that A221:
not
w is
dependent
and A222:
(center_of_mass V) . S in conv (@ w)
by A66, A210, A217, Def3;
w in the
topology of
(BCS (k,(Complex_of {Aa})))
by A221, PRE_TOPC:def 2;
then
w in the
topology of
(BCS (k,(Complex_of {A})))
by A218;
then reconsider W =
w as
Simplex of
(BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2;
Int (@ S) meets conv (@ W)
by A220, A222, XBOOLE_0:3;
then A223:
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 A221, A223, MATROID0:1;
A224:
FA .: s = Aa
by A206, RELAT_1:129, SIMPLEX0:17;
s is
Simplex of
m - 1,
BCS (
k,
(Complex_of {Aa}))
by A168, A219, SIMPLEX0:48;
hence
x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa }
by A205, A224;
verum
end; A225:
degree (Complex_of {Aa}) = m - 1
by A5, A168, 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 A226:
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 A227:
x = S
and A228:
FA .: S = Aa
;
m - 1
<= degree (BCS (k,(Complex_of {Aa})))
by A7, A225, Th32;
then reconsider S1 =
x as
Simplex of
m - 1,
BCS (
k,
(Complex_of {A}))
by A14, A227, SIMPLEX0:49;
A229:
FA .: S = F .: S
by RELAT_1:129, SIMPLEX0:17;
conv (@ S) c= conv Aa
by A66, Th5;
then
conv (@ S1) misses Int A
by A226, A227, 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 A227, A228, A229;
verum
end; then A230:
{ 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 A204, XBOOLE_0:def 10;
A231:
(
(2 * n) + 1
in NAT & 2
* (card DX) in NAT )
by ORDINAL1:def 12;
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 A232:
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 A233:
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 A234:
x = S
and A235:
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 A232, XBOOLE_0:def 5;
then
conv (@ S) meets Int A
by A234, A235;
then A236:
card { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = 2
by A3, Th45;
A237:
(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 A238:
[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 A239:
s in {S}
by RELAT_1:def 13;
A240:
[s,w] in R
by A238, RELAT_1:def 11;
then
w in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum }
by A47;
then A241:
ex
W being
Simplex of
m,
BCS (
k,
(Complex_of {A})) st
w = W
;
s = S
by A239, TARSKI:def 1;
then
S c= w
by A47, A240;
hence
w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
by A241;
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 A242:
w = W
and A243:
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, A233, A234, A243;
then A244:
[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 A232, A234, 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 A242, A244, 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 A237, 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 A234, A236, 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:18
;
then A245:
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, A230, CARD_2:21
.=
((card 2) *` (card (card DX))) +` ((2 * n) + 1)
by Lm1
.=
(card (2 * (card DX))) +` ((2 * n) + 1)
by CARD_2:39
.=
(card (2 * (card DX))) +` (card ((2 * n) + 1))
by Lm1
.=
card ((2 * (card DX)) + ((2 * n) + 1))
by A231, CARD_2:38
.=
(2 * (card DX)) + ((2 * n) + 1)
by Lm1
;
then
card XX = (2 * (((card DX) + n) - (card YA))) + 1
by A48, A202;
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
;
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, A202, A245;
verum end;
end;
A246:
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 A247:
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
A248:
A = {}
by A247;
set C =
Complex_of {A};
A249:
(
|.(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
A250:
(
k = 0 or
k > 0 )
;
A251:
Z - 1
= - 1
by XXREAL_3:4;
then
degree (Complex_of {A}) = - 1
by A247, SIMPLEX0:26;
then A252:
Complex_of {A} = BCS (
k,
(Complex_of {A}))
by A249, A250, Th16, Th22;
A253:
the
topology of
(Complex_of {A}) = bool A
by SIMPLEX0:4;
A254:
{ 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 A255:
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 A256:
S = x
and
F .: S = A
by A255;
S in the
topology of
(Complex_of {A})
by A252, PRE_TOPC:def 2;
then
S is
empty
by A248, A253;
hence
x in {A}
by A248, A256, 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 A253, PRE_TOPC:def 2;
A257:
F .: A1 = A
by A248;
A1 is
Simplex of
- 1,
Complex_of {A}
by A247, A251, SIMPLEX0:48;
then
A in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A }
by A247, A252, A257;
then
{ S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = {A}
by A254, ZFMISC_1:33;
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:30;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A246, 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