Si ¬(∃x)P(x), entonces (∀x)¬P(x)
Demostrar con Lean4 que si \(¬(∃x)P(x)\), entonces \((∀x)¬P(x)\).
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by sorry |