Menu Close

Autor: José A. Alonso

P → ¬¬P

Demostrar con Lean4 que \(P → ¬¬P\).

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

import Mathlib.Tactic
variable (P : Prop)
 
example
  (h : P)
  : ¬¬P :=
by sorry

¬¬P → P

Demostrar con Lean4 que \(¬¬P → P\).

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

import Mathlib.Tactic
variable (P : Prop)
 
example
  (h : ¬¬P)
  : P :=
by sorry

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:

import Mathlib.Tactic
variable {α : Type _}
variable (P : α  Prop)
 
example
  (h :  x, ¬ P x)
  : ¬  x, P x :=
by sorry

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:

import Mathlib.Tactic
variable {α : Type _}
variable (P : α  Prop)
 
example
  (h : ¬  x, P x)
  :  x, ¬ P x :=
by sorry

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:

import Mathlib.Tactic
variable {α : Type _}
variable (P : α  Prop)
 
example
  (h :  x, ¬ P x)
  : ¬  x, P x :=
by sorry