On Monday, June 10, 2019 at 7:41:30 AM UTC-4, Thierry Arnoux wrote:
>
> Actually, in this case, you can just skip your steps 78 and 79:
>
> 80:77:ss2abdv |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
> -> { x | ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) }
> C_ { x | x e. ( B [,] B ) } )
>
> Note that bnj1153 is discouraged!
>
I guess you have to revert to using elin directly.
>
It sounds like mmj2 is allowing matches to discouraged theorems, which
ideally shouldn't happen. But I'm not sure to what extent the recognition
of discouraged tags has been implemented in mmj2.
A few years ago I moved the useful bnj* theorems that I found to main and
added discouraged tags to the rest. It seems I missed bnj1153, which is
very useful. I renamed it to elind and moved it to main, so you can use it
now. It minimized 187 proofs out of the 597 that originally used elin,
reducing set.mm by 4500 bytes.
Norm
--
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/f9b32a13-6ddb-46d2-9695-ee92297c1574%40googlegroups.com.
