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 |
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 |
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 |
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 |
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 |
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 |