:: deftheorem Def1 defines Lebesgue_number SIMPLEX2:def 1 :
for M being non empty MetrSpace st TopSpaceMetr M is compact holds
for F being Subset-Family of (TopSpaceMetr M) st F is open & F is Cover of (TopSpaceMetr M) holds
for b₃ being positive Real holds
( b₃ is Lebesgue_number of F iff for p being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (p,b₃) c= A ) );