[isabelle] More complete theory?

Developing a theory, should I dive into gory details?

For example I have the theorem "move: bij(big, newbig)". Should I also
publish its consequences such that "move: inj(big, newbig)"? Or even
that "move: big->newbig"? that "range(move) = newbig", etc.?

Victor Porton - http://portonvictor.org

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.