Add the ad4ant* and ad5ant* ones to iset.mm too if you have the time (if
not, no worries, it can happen whenever someone gets around to it).
The supadd and inisegn0 ones wouldn't work in iset.mm.
On 8/15/20 6:17 AM, 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 [email protected]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/e9fd83fb-4d2b-424b-b31a-0a6e6c65664co%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/e9fd83fb-4d2b-424b-b31a-0a6e6c65664co%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/c46b999d-2aa7-d3f3-7512-9efee7fb2d76%40panix.com.
