From 149f8921c2bd7be539e41d6fea81ab2194afedc7 Mon Sep 17 00:00:00 2001 From: avekens Date: Sat, 18 Nov 2023 13:42:25 +0100 Subject: [PATCH] elnanel revised --- discouraged | 2 ++ set.mm | 6 ++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/discouraged b/discouraged index e2eb9e9c07..4d8a367283 100755 --- a/discouraged +++ b/discouraged @@ -5649,6 +5649,7 @@ "ellnop" is used by "lnopl". "ellnop" is used by "lnopmi". "ellnop" is used by "unoplin". +"elnanel" is used by "elnanelprv". "elni" is used by "0npi". "elni" is used by "1pi". "elni" is used by "addclpi". @@ -15075,6 +15076,7 @@ New usage of "elimphu" is discouraged (3 uses). New usage of "elissetOLD" is discouraged (0 uses). New usage of "ellnfn" is discouraged (5 uses). New usage of "ellnop" is discouraged (9 uses). +New usage of "elnanel" is discouraged (1 uses). New usage of "elni" is discouraged (7 uses). New usage of "elni2" is discouraged (7 uses). New usage of "elnlfn" is discouraged (4 uses). diff --git a/set.mm b/set.mm index 411beb7c63..38ea86ff7a 100644 --- a/set.mm +++ b/set.mm @@ -91095,8 +91095,10 @@ is that it denies the existence of a set containing itself ( ~ elirrv ). ( cvv wcel wa wn cep wfr zfregfr efrn2lp mpan elex anim12i con3i pm2.61i ) ACDZBCDZEZABDZBADZEZFZCGHRUBCICABJKUARSPTQABLBALMNO $. - $( Two classes are not elements of each other simultaneously. (Contributed - by AV, 5-Nov-2023.) $) + $( Two classes are not elements of each other simultaneously. This is just a + rewriting of ~ en2lp and serves as an example in the context of Godel + codes, see ~ elnanelprv . (Contributed by AV, 5-Nov-2023.) + (New usage is discouraged.) $) elnanel $p |- ( A e. B -/\ B e. A ) $= ( wcel wnan wa wn en2lp df-nan mpbir ) ABCZBACZDJKEFABGJKHI $.