let X be set ; for M being non empty Reflexive MetrStruct
for K being subset-closed b1 bounded SimplicialComplexStr of X
for i being dim-like number holds diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)
let M be non empty Reflexive MetrStruct ; for K being subset-closed M bounded SimplicialComplexStr of X
for i being dim-like number holds diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)
set r = the Real;
let K be subset-closed M bounded SimplicialComplexStr of X; for i being dim-like number holds diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)
let i be dim-like number ; diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)
set SK = Skeleton_of (K,i);
A1:
the topology of (Skeleton_of (K,i)) c= the topology of K
by SIMPLEX0:def 13;
per cases
( the topology of (Skeleton_of (K,i)) meets bool ([#] M) or the topology of (Skeleton_of (K,i)) misses bool ([#] M) )
;
suppose A2:
the
topology of
(Skeleton_of (K,i)) meets bool ([#] M)
;
diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)then A3:
the
topology of
K meets bool ([#] M)
by A1, XBOOLE_1:63;
now for A being Subset of M st A in the topology of (Skeleton_of (K,i)) holds
diameter A <= diameter (M,K)let A be
Subset of
M;
( A in the topology of (Skeleton_of (K,i)) implies diameter A <= diameter (M,K) )
the_family_of K is
subset-closed
by MATROID0:def 3;
then A4:
the
topology of
K is
subset-closed
by MATROID0:def 1;
assume
A in the
topology of
(Skeleton_of (K,i))
;
diameter A <= diameter (M,K)then consider w being
set such that A5:
A c= w
and A6:
w in the_subsets_with_limited_card (
(i + 1), the
topology of
K)
by SIMPLEX0:2;
reconsider w =
w as
Subset of
K by A6;
w in the
topology of
K
by A6, SIMPLEX0:def 2;
then
A in the
topology of
K
by A4, A5, CLASSES1:def 1;
hence
diameter A <= diameter (
M,
K)
by A3, Def3;
verum end; hence
diameter (
M,
(Skeleton_of (K,i)))
<= diameter (
M,
K)
by A2, Def3;
verum end;