Definition talk:Saturation (Equivalence Relation)

From ProofWiki
Jump to navigation Jump to search

Not sure if $\overline T := \operatorname{pr}_1(\sim\cap\operatorname{pr}_2^{-1}(T))$ should be a definition or a theorem. --barto (talk) 18:59, 16 March 2017 (EDT)

The rule of thumb that we have been using is: if it can be found in a published text, specifically used in that text as a definition for the concept, then enter it as a definition. Otherwise introduce it as an equivalence proof.
Ultimately: if it can be used practically as a definition, then there is a case for it to be introduced as a definition. If not, then probably not.
None of this is cast in stone. There is always room for refactoring. But, if in doubt, then I advise not to set up as a definition if you don't know whether to or not, as it can be unwieldy carrying round a lot of equivalent definitions -- the equivalence proofs got very complicated and difficult to manage. --prime mover (talk) 19:35, 16 March 2017 (EDT)
Okay, makes sense. I was thinking more or less the same. I put it at Saturation Under Equivalence Relation in Terms of Graph --barto (talk) 15:04, 17 March 2017 (EDT)