I agree, except maybe for the suffix "b", which should not be automatic as soon as a statement is a biconditional. A characterization is by definition a biconditional. If there is only one form of isxxx in set.mm, then use that default label, and if both forms are in set.mm, then maybe use "isxxx" and "isxxxs" (for "isxxx for sets") ?
On Sunday, December 5, 2021 at 11:38:48 AM UTC+1 Alexander van der Vekens wrote: > (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/5672bb26-aa77-43a6-9fdd-2bbdfed5cfe8n%40googlegroups.com.
