You have my approval. Norm On Saturday, August 15, 2020 at 9:17:56 AM UTC-4, Glauco wrote: > > I've taken advantage of some theorems, still in mathboxes. Can I set up a > PR for moving them to the main body? > > Here's the list: > > - supadd from Brendan Leahy's mathbox : sup distributes over addition (we > already have supmul in the main part, that's "the same" for multiplication) > > - inisegn0 from Stefan O'Rear's Mathbox : the comment says "Nonemptyness > of an initial segment in terms of range" but it looks like it's more > general than that, it's a nice and simple characterization of being > an element of a range > > - ad4ant* and ad5ant* from Alan Sare's Mathbox : these theorems allow to > simplify complex antecedents; for instance, ad5ant245 selects three > conditions out of five and saves three lines w.r.t > syl3anc or syl21anc that would be an alternative solution. In the past, > I've always refactored my proofs to avoid using these theorems, since they > are not in the main body, but they would > really shorten many of my proofs (and I'm pretty sure they could also > shorten many other proofs in set.mm) > > It there's consensus, I will submit a PR for promoting these theorems to > the main part. > > Glauco >
-- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6fd658eb-9744-49cb-9b4f-8ddf9666d2abo%40googlegroups.com.
