Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] More complete theory?

Email Gateway (Aug 18 2022 at 13:12):

From: Victor Porton <porton@narod.ru>
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.?

Last updated: Nov 21 2024 at 12:39 UTC