let n be Nat; for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
Vertices Kv c= Vertices (BCS n,Kv)
let V be RealLinearSpace; for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
Vertices Kv c= Vertices (BCS n,Kv)
let Kv be non void SimplicialComplex of V; ( |.Kv.| c= [#] Kv implies Vertices Kv c= Vertices (BCS n,Kv) )
set S = Skeleton_of Kv,0 ;
assume A1:
|.Kv.| c= [#] Kv
; Vertices Kv c= Vertices (BCS n,Kv)
per cases
( n = 0 or n > 0 )
;
suppose A2:
n > 0
;
Vertices Kv c= Vertices (BCS n,Kv)
the
topology of
(Skeleton_of Kv,0 ) c= the
topology of
Kv
by SIMPLEX0:def 13;
then
|.(Skeleton_of Kv,0 ).| c= |.Kv.|
by Th4;
then A3:
|.(Skeleton_of Kv,0 ).| c= [#] (Skeleton_of Kv,0 )
by A1, XBOOLE_1:1;
then
(
degree (Skeleton_of Kv,0 ) <= 0 &
BCS n,
(Skeleton_of Kv,0 ) is
SubSimplicialComplex of
BCS n,
Kv )
by A1, Th23, SIMPLEX0:44;
then
Skeleton_of Kv,
0 is
SubSimplicialComplex of
BCS n,
Kv
by A2, A3, Th22;
then A4:
Vertices (Skeleton_of Kv,0 ) c= Vertices (BCS n,Kv)
by SIMPLEX0:31;
let x be
set ;
TARSKI:def 3 ( not x in Vertices Kv or x in Vertices (BCS n,Kv) )assume A5:
x in Vertices Kv
;
x in Vertices (BCS n,Kv)then reconsider v =
x as
Element of
Kv ;
v is
vertex-like
by A5, SIMPLEX0:def 4;
then consider A being
Subset of
Kv such that A6:
not
A is
dependent
and A7:
v in A
by SIMPLEX0:def 3;
reconsider vv =
{v} as
Subset of
Kv by A7, ZFMISC_1:37;
{v} c= A
by A7, ZFMISC_1:37;
then
not
vv is
dependent
by A6, MATROID0:1;
then A8:
vv in the
topology of
Kv
by PRE_TOPC:def 5;
(
card vv = 1 &
card 1
= 1 )
by Lm1, CARD_1:50;
then
vv in the_subsets_with_limited_card 1,the
topology of
Kv
by A8, SIMPLEX0:def 2;
then
vv in the
topology of
(Skeleton_of Kv,0 )
by SIMPLEX0:2;
then reconsider vv =
vv as
Simplex of
(Skeleton_of Kv,0 ) by PRE_TOPC:def 5;
A9:
v in vv
by TARSKI:def 1;
reconsider v =
v as
Element of
(Skeleton_of Kv,0 ) ;
v is
vertex-like
by A9, SIMPLEX0:def 3;
then
v in Vertices (Skeleton_of Kv,0 )
by SIMPLEX0:def 4;
hence
x in Vertices (BCS n,Kv)
by A4;
verum