30 noviembre 2023 – Calculemus

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

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