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/44942778-1524-4e85-a488-13ec76166cdc%40googlegroups.com.
