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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e9fd83fb-4d2b-424b-b31a-0a6e6c65664co%40googlegroups.com.
