29. No witness means never

MediumProofAcademy Pass20 points

Prove that “there is no x with P x” and “every x fails P” say the same thing. Both directions are constructive.

Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.

Solution.lean

1theorem solution (α : Type) (P : α → Prop) : (¬ ∃ x, P x) ↔ ∀ x, ¬ P x := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

α:Type

P:α → Prop

⊢(¬ ∃ x, P x) ↔ ∀ x, ¬ P x

ReadyLn 1, Col 1Lean 4

Draft saved in this browser