(This topic was discussed in the comments for Github PR #2344:
https://github.com/metamath/set.mm/pull/2344)
I'am also often uncertain which of these variants to use. ~isxxx1 is more
powerful because it is a biconditional, but ~isxxx2 is easier to
use/understand. Maybe we can agree on a fixed order if both variants are
available. I would prefer to have ~isxxx1 first, followed by ~isxxx2 which
is proven by using ~isxxx1 and ~biadan2 . The first theorem (~isxxx1 )
should be named isxxxb ("b" for "biconditional" - see conventions for
Suffixes"), the second theorem (~isxxx2) should be named isxxx. The comment
of ~isxxx1 (resp. ~isxxxb) shoud be in the form "The predicate "is a
...". ", and the comment of ~isxxx2 (resp. ~isxxx) "The predicate "is a
..." for a set.".
I would prefer the prefix "is" over "el", because it is more general. For
example ~iswlk has the form " .. -> ( F ( Walks ` G ) P <-> ..", which does
not contain an ` e. ` ("is element of"). But I don't want to hide that you
can write this theorem in the form " .. -> ( <. F , P >. e. ( Walks ` G )
<-> .." ...
On Thursday, December 2, 2021 at 8:30:53 PM UTC+1 Scott Fenton wrote:
> I've generally gone with el* in my mathbox (see, eg., elno). I've seen is*
> around, but I feel el* has better compatibility with el*ab*.
>
> On Thu, Dec 2, 2021 at 2:23 PM Benoit <[email protected]> wrote:
>
>> Many theorems in set.mm are characterizations of elements of a defined
>> class. For instance: ~isgrp , ~ istopg . More precisely, if we have a
>> definition
>> df-xxx $a |- Class = { x | Phi } $.
>> Then there is typically in set.mm a theorem isxxx. If Phi(A) does not
>> imply that A is a set, then there are two possible forms:
>> isxxx1 $p |- ( A e. Class <-> ( A e. _V /\ Phi(A) ) )
>> isxxx2 $p |- ( A e. V -> ( A e. Class <-> Phi(A) ) )
>> It is easy to go back and forth (using biadan2 and baib).
>> Is there a preferred form ? Is it ok to have both in set.mm ? It seems
>> to me that isxxx1 is closer to a real characterization (while isxxx2 is a
>> characterization among sets), but after a quick look, it seems that isxxx2
>> is often (majoritarily?) used in set.mm, for instance by looking at the
>> number of usages of elab2g versus elab4g.
>>
>> Benoît
>>
>> --
>> 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/f8248f4c-ea12-4b44-b6e7-dee1e5db3feen%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/metamath/f8248f4c-ea12-4b44-b6e7-dee1e5db3feen%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/458b598b-4aee-46a5-aa16-68be59c25ab2n%40googlegroups.com.
