neqned is a duplicate of neneqad. I suggest to merge both into one, preferring the name, attributions and explanation of the older neneqad.
Wolf Am Samstag, 21. Dezember 2019 07:21:48 UTC+1 schrieb Alexander van der Vekens: > > With my latest PR, I moved the following theorems from Glauco's mathbox > into the main part of set.mm: > > - ~ neqned, ~ iffalsed, ~ iftrued, ~ rspan (renamed "rspa") > - ~ fssresd, ~ fssd, ~ resmptd, ~ dmmptid (renamed "dmmpod"), ~ > resabs1d > > I didn't move ~ ifeq123d (because it is already available as ~ ifbieq12d , > so I marked ~ ifeq123d as "discouraged") and ~ feq1dd, which maybe isn't as > useful as I thought. > > On Tuesday, December 17, 2019 at 5:50:37 PM UTC+1, Alexander van der > Vekens wrote: >> >> I had a closer look at the theorems in sections "Miscellanea" and >> "Functions" in Glauco`s Mathbox, and I think the following could be quite >> useful and should be moved to the main part as soon as possible: >> >> - "Miscellanea": >> - neqned: ( ph -> -. A = B ) => ( ph -> A =/= B ) >> - iffalsed: ( ph -> -. ch ) => iffalsed $p |- ( ph -> if ( ch , A >> , B ) = B ) >> - iftrued:( ph -> ch ) =>( ph -> if ( ch , A , B ) = A ) >> - ifeq123d.: (ph -> ( ps <-> ch ) ) & ( ph -> A = B ) & ( ph -> C >> = D ) => ( ph -> if ( ps , A , C ) = if ( ch , B , D ) ) >> - rspan: ( ( A. x e. A ph /\ x e. A ) -> ph ) (maybe to be >> renamed!) >> - "Functions": >> - feq1dd: ( ph -> F = G ) &( ph -> F : A --> B ) => ( ph -> G : A >> --> B ) (rename feq1d -> feq1bid; feq1dd -> feq1d) >> - fssresd: ( ph -> F : A --> B ) & ( ph -> C C_ A ) => ( ph -> ( F >> |` C ) : C --> B ) >> - fssd: ( ph -> F : A --> B ) & ( ph -> B C_ C ) =>( ph -> F : A >> --> C ) >> - resmptd: ( ph -> B C_ A ) => ( ph -> ( ( x e. A |-> C ) |` B ) = >> ( x e. B |-> C ) ) >> - dmmptid: A = ( x e. B |-> C ) & ( ( ph /\ x e. B ) -> C e. V ) >> => ( ph -> dom A = B ) >> - resabs1d: ( ph -> B C_ C ) => ( ph -> ( ( A |` C ) |` B ) = ( A >> |` B ) ) >> >> I have chosen these theorems especially because they are variants of >> existing theorems, but in deduction form, so they support the "deduction >> style" of set.mm. For the theorems in section "Miscellanea", I also took >> the number of usages into account, see attachment. >> >> If nobody objects, I can move these theorems before christmas :-). >> >> On Monday, December 16, 2019 at 6:53:24 AM UTC+1, Alexander van der >> Vekens wrote: >>> >>> Congratulations also from my side for proving another "Metamath 100" >>> theorem! >>> >>> I also had a look at the "general theorems". I agree that a lot of them >>> could be moved to the main part. As David (and also others) mentioned, this >>> should be done in a structured way. At the moment, these theorems are all >>> mixed up in section "Miscellanea", so maybe the first step would be to >>> structure this section (using appropriate subsections, corresponding to the >>> (sub)sections of the main part). >>> >>> As far as my latest "Metamath 100" theorem is concerned, I plan to move >>> it (and all theorems which are used by its proof) to the main part, too. >>> See issue #1314 at GitHub. >>> >>> Alexander >>> >>> On Monday, December 16, 2019 at 1:32:53 AM UTC+1, David A. Wheeler wrote: >>>> >>>> On Sun, 15 Dec 2019 13:02:33 -0800 (PST), Benoit <[email protected]> >>>> wrote: >>>> > Like FL, I think several lemmas deserve to be in the main part. >>>> >>>> I believe that all "Metamath 100" results (and thus all they depend on) >>>> should eventually move into the main body. After all, all Metamath 100 >>>> results are >>>> results that at least some others believe are important. >>>> >>>> We don't have to do that *instantly* of course. >>>> In many cases I expect there will be discussion as the dependencies >>>> are examined, possibly generalized, and then moved into the main body >>>> in groups over time. >>>> >>>> I think it's important to keep working on getting more things moved >>>> from mathboxes >>>> into the main body. Tools like mmj2 only consider items in the main >>>> body for >>>> many automated steps, and in any case I think it's far more sensible to >>>> readers if major results are properly organized in the main body. >>>> >>>> --- David A. Wheeler >>> >>> -- 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/2443ec3f-87da-4cd8-9ca5-46ec6d39834b%40googlegroups.com.
