:: deftheorem Def4 defines diameter SIMPLEX2:def 4 :
for M being non empty Reflexive MetrStruct
for K being non void subset-closed b₁ bounded SimplicialComplexStr
for b₃ being Real holds
( b₃ = diameter (M,K) iff ( ( for A being Subset of M st A is Simplex of K holds
diameter A <= b₃ ) & ( for r being Real st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= b₃ ) ) );