:: deftheorem Def12 defines degree SIMPLEX0:def 12 :
for K being SimplicialComplexStr
for b₂ being ExtReal holds
( ( not K is void & K is finite-degree implies ( b₂ = degree K iff ( ( for S being finite Subset of K st S is simplex-like holds
card S <= b₂ + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b₂ + 1 ) ) ) ) & ( K is void implies ( b₂ = degree K iff b₂ = - 1 ) ) & ( ( K is void or not K is finite-degree ) & not K is void implies ( b₂ = degree K iff b₂ = +infty ) ) );