27 noviembre 2023 – Calculemus

Si ¬(∃x)P(x), entonces (∀x)¬P(x)

PorJosé A. Alonso 27 noviembre 202314 noviembre 2023

Demostrar con Lean4 que si \(¬(∃x)P(x)\), entonces \((∀x)¬P(x)\).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable {α : Type _}
variable (P : α → Prop)

example
  (h : ¬ ∃ x, P x)
  : ∀ x, ¬ P x :=
by sorry

import Mathlib.Tactic

variable {α : Type _}

variable (P : α → Prop)

example

(h : ¬ ∃ x, P x)

: ∀ x, ¬ P x :=

by sorry