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;
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
object ;
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:
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
(Skeleton_of (Kv,0))
by SIMPLEX0:2;
then reconsider vv =
vv as
Simplex of
(Skeleton_of (Kv,0)) by PRE_TOPC:def 2;
A9:
v in vv
by TARSKI:def 1;
reconsider v =
v as
Element of
(Skeleton_of (Kv,0)) ;
v is
vertex-like
by A9;
then
v in Vertices (Skeleton_of (Kv,0))
by SIMPLEX0:def 4;
hence
x in Vertices (BCS (n,Kv))
by A4;
verum