如何从精益原则证明 (∀ x, ¬ A x) → ¬ ∃ x, A x？

【问题标题】：how can I prove (∀ x, ¬ A x) → ¬ ∃ x, A x from principles in lean?如何从精益原则证明 (∀ x, ¬ A x) → ¬ ∃ x, A x？
【发布时间】：2021-11-20 22:25:34
【问题描述】：

我知道要证明：(¬ ∀ 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

【问题讨论】：

你尝试了什么？你能把证据显示到你卡住的地方吗？
请求家庭作业帮助的问题必须包括您迄今为止为解决问题所做的工作的总结，以及您在解决问题时遇到的困难的描述。请阅读How to ask homework questions 和edit 您的帖子。如果您花一些时间在tour 和阅读help center 页面以了解该网站的运作方式以及我们的期望，然后再开始发布，您会发现您在这里的体验会好得多。
你知道如何解决的问题似乎比你不知道的问题更难。你明白你能解决的证明吗？

标签： logic set-theory lean

【解决方案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 和A x 的证明。所以cases h₂ with x hx 作为上述证明的下一行。之后，您应该能够自己填写证明的其余部分。

【讨论】：