Deprecated in https://github.com/metamath/set.mm/pull/2816
Benoît On Tuesday, September 6, 2022 at 6:58:35 AM UTC+2 Alexander van der Vekens wrote: > It is really a strange theorem: both sides of the biconditional are wrong > ( x=y is wrong, because 0 <_ x and y < 0; and 2x = -2y+1would mean that an > even number is equal to an odd number. > > Therefore, this theorem can be deprecated and removed later. > > On Thursday, September 1, 2022 at 6:13:11 PM UTC+2 Benoit wrote: > >> Good catch. I vote for removing (that is, deprecating) >> https://us.metamath.org/mpeuni/znnenlem.html >> >> Benoît >> >> >> On Thursday, September 1, 2022 at 5:43:32 PM UTC+2 [email protected] >> wrote: >> >>> Should znnenlem be removed from set.mm or moved to a mathbox? It claims >>> to be a lemma for znnen, but it's no longer used, and while lines 16 and 28 >>> prove moderately interesting things, it then turns A -> B and C -> D into >>> (A /\ B) -> (C <-> D). So maybe splittable into three theorems? >>> >> -- 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/0d48f67b-c8d9-4efa-95a4-229e894750afn%40googlegroups.com.
