:: deftheorem Def3 defines diameter SIMPLEX2:def 3 :
for M being non empty Reflexive MetrStruct
for K being SimplicialComplexStr st K is M bounded holds
for b₃ being Real holds
( ( the topology of K meets bool ([#] M) implies ( b₃ = diameter (M,K) iff ( ( for A being Subset of M st A in the topology of K holds
diameter A <= b₃ ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b₃ ) ) ) ) & ( not the topology of K meets bool ([#] M) implies ( b₃ = diameter (M,K) iff b₃ = 0 ) ) );