section\nopen classical\nexample : \xc2\xac (A \xe2\x86\x94 \xc2\xac A) :=\nhave hn : (A \xe2\x88\xa8 \xc2\xac A), from sorry,\n assume h : (A \xe2\x86\x94 \xc2\xac A),\n show false, from or.elim hn\n (assume h1 : A, h.mp h1 h1)\n (assume h2 : \xc2\xac A, h2 (h.mpr h2))\nend\n我正在阅读 Jeremy Avigad 的《逻辑与证明》一书来学习精益。问题是我只能用by_contradiction战术来应对排中法则。有人可以帮我吗？
lean ×1