how can I prove (∀ x, ¬ A x) → ¬ ∃ x, A x from principles in lean?

user_17029571 0
Viewed 223

I know that to prove : (¬ ∀ x, p x) → (∃ x, ¬ p x) the proof is:

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

But I have no idea how to prove: (∀ x, ¬ A x) → ¬ ∃ x, A x

set-theory lean logic
1 Answers

¬ p x is defined to be p x → false. This means that using intro works when your goal is ¬.

so for example, the following works

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

end

You can use the cases tactic to eliminate a proof of ∃ x, A x into an x and a proof of A x. So cases h₂ with x hx works as the next line of the above proof. You should hopefully be able to fill in the remainder of the proof yourself after that.

user_109423810
Related