eqsb3lem vs eqsb3v

56 views
Skip to first unread message

Zheng Fan

unread,
May 2, 2023, 4:08:52 PM5/2/23
to Metamath
Why do we have these two identical lemmas in the database, none of which has any discouragement tag? 

David A. Wheeler

unread,
May 2, 2023, 6:22:07 PM5/2/23
to Metamath Mailing List


> On May 2, 2023, at 4:08 PM, Zheng Fan <fanzhe...@outlook.com> wrote:
>
> Why do we have these two identical lemmas in the database, none of which has any discouragement tag?

Probably because no one noticed.

--- David A. Wheeler

Zheng Fan

unread,
May 3, 2023, 1:21:57 PM5/3/23
to Metamath
Looking at them again I guess things are not that simple, because they are touched by the same person on two consecutive days.

Alexander van der Vekens

unread,
May 12, 2023, 4:16:43 PM5/12/23
to Metamath
The differnce is that ~eqsb3lem requires x and y to be distinct (because of `$d x y $.`), whereas ~eqsb3 does not have this restriction (x and y may be replaced by the same setvar variable z: `( [ z / z ] z = A <-> z = A )` also holds, see also ~sbid).
Reply all
Reply to author
Forward
0 new messages