如何解决在精益中证明¬A∧B→A→¬B
我正在尝试用精益定理证明者来证明¬（A∧B）→（A→¬B）。我已经像这样设置了。
example : ¬ (A ∧ B) → (A → ¬ B) :=
assume h1: ¬ (A ∧ B),assume h2: A,show ¬ B,from sorry
我已经尝试过将h.1和and.left和and.right一起使用，但是当否定合取时，这些命令不起作用。从否定开始，我找不到任何证明这种含义的例子。任何帮助将不胜感激。
解决方法
¬ B被定义为B -> false，所以您可以从
example (A B : Prop): ¬ (A ∧ B) → (A → ¬ B) :=
assume h1: ¬ (A ∧ B),assume h2: A,assume h3: B,show false,from sorry
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
