proof - 在精益中证明 ¬ (A ∧ B) → (A → ¬ B)

Question

我试图用精益定理证明者证明 ¬ (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 ，但是当连词被否定时，这些都不起作用。我找不到任何从否定开始证明这种暗示的例子。任何帮助将非常感激。

Answer 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