Hello,
The logical hypothesis for theorem oveq2i has the same name as that for oveq1i.
This tripped me up, but is the naming intentional?
In particular, I was writing up my own proof of 2p2e4 when I noticed the clash.
In fact, the proof of 2p2e4 exhibits the same exact issue: the first
Excellent. So I just happened to stumble upon a nice method used to organize
related deductions. Much appreciated.
On Fri, Oct 25, 2019 at 06:24:40AM -0700, Jim Kingdon wrote:
> This is relatively common when people want related theorems to have the same
> hypothesis.
>
> If you look at set.mm,
This is relatively common when people want related theorems to have the
same hypothesis.
If you look at set.mm, you'll see that oveq1i.1 only appears once, but
in a ${ $} block which includes both oveq1i and oveq2i .
On 10/25/19 2:51 AM, heiphoh...@wilsonb.com wrote:
Hello,
The logical
Hello,
The logical hypothesis for theorem oveq2i has the same name as that for oveq1i.
This tripped me up, but is the naming intentional?
In particular, I was writing up my own proof of 2p2e4 when I noticed the clash.
In fact, the proof of 2p2e4 exhibits the same exact issue: the first
