28 noviembre 2023 – Calculemus

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

PorJosé A. Alonso 28 noviembre 202315 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