29 noviembre 2023 – Calculemus

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

PorJosé A. Alonso 29 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