在精益中证明 ¬ (A ∧ B) → (A → ¬ B)答案

【问题标题】：Proving ¬ (A ∧ B) → (A → ¬ B) in Lean在精益中证明 ¬ (A ∧ B) → (A → ¬ B)
【发布时间】：2020-09-23 21:18:42
【问题描述】：

我正在尝试用精益定理证明器证明 ¬ (A ∧ B) → (A → ¬ B)。我已经这样设置了。

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

我尝试将 and.left 和 and.right 用于 h1，但是当连词被否定时，这些都不起作用。我找不到任何从否定开始证明这种暗示的例子。任何帮助将不胜感激。

【问题讨论】：

【解决方案1】：

¬ 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

【讨论】：