Norm once told me (several years ago!) that the threshold value is 7 theorems: If the introduction of a convenience theorem affects this many or more theorems, its value outperforms the downside of having more theorems..
Wolf Lammen [email protected] schrieb am Montag, 6. September 2021 um 01:12:20 UTC+2: > As with things like 1cnd I think it is a matter of whether the convenience > theorem would get used enough times to justify having it. > On 9/5/21 7:22 AM, Glauco wrote: > > A theorem like > > |- ( ph -> ( F ` A ) e. _V ) > > would clearly be "redundant". > > But it would save a LOT of a1i (and shorten many proofs, I guess) > > And the autocomplete feature of mmj2 would take advantage of it (as far as > I can tell, the current version doesn't add an a1i automagically). > > Comments? > > > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/756da4ff-316a-4861-bbaf-b100e108cdc8n%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/756da4ff-316a-4861-bbaf-b100e108cdc8n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/799660b9-fcaa-4f0e-a016-ce2c3ba959b8n%40googlegroups.com.
