文章/答案/技术大牛

发布

社区首页 >问答首页 >在精益生产中证明(A∧B)→(A→？B)

问在精益生产中证明(A∧B)→(A→？B)
EN

Stack Overflow用户

提问于 2020-09-24 05:18:42

回答 1查看 274关注 0票数 1

我试着用精益定理证明器证明(A∧B)→(A→- B)。我这样设置它。

example : ¬ (A ∧ B) → (A → ¬ B) :=
assume h1: ¬ (A ∧ B),
assume h2: A,
show ¬ B, from sorry

我尝试过对h1使用and.left和and.right，但当合取被否定时，这些都不起作用。我找不到任何例子来证明像这样从否定开始的含义。任何帮助都将不胜感激。

发布于 2020-09-24 05:25:45

¬ 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

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/64036383

复制

相似问题

问在精益生产中证明(A∧B)→(A→？B)EN