:: deftheorem defines -fine COUSIN:def 4 :
for I being non empty closed_interval Subset of REAL
for jauge being positive-yielding Function of I,REAL
for TD being tagged_division of I holds
( TD is jauge -fine iff ex D being Division of I ex T being Element of set_of_tagged_Division D st
( TD = [D,T] & ( for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge . (T . i) ) ) );