logic - 我如何根据精益原则证明 (∀ x, ¬ A x) → ¬ ∃ x, A x？

Question

我知道要证明 : (¬ ∀ x, p x) → (∃ x, ¬ p x) 证明是:

theorem : (¬ ∀ x, p x) → (∃ x, ¬ p x) := 
begin
    intro nAxpx, 
    by_contradiction nExnpx,
    apply nAxpx,
    assume a,
    by_contradiction hnpa,
    apply nExnpx,
    existsi a,
    exact hnpa,
end

但我不知道如何证明:(∀ x, ¬ A x) → ¬ ∃ x, A x

Answer 1

¬ p x 被定义为 p x → false。这意味着当您的目标是 ¬ 时，使用 intro 是可行的。

例如，下面的作品

example {α : Type} {A : α → Prop} : (∀ x, ¬ A x) → ¬ ∃ x, A x :=
begin
  intros h₁ h₂,

end

您可以使用 cases 策略将 ∃ x, A x 的证明消除为 x 和 的证明一个 x。所以 cases h2 with x hx 用作上述证明的下一行。之后您应该能够自己填写证明的其余部分。