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:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := by sorry |
Demostración en lenguaje natural
Supongamos que \((∃x)P(x)\). Sea \(y\) tal que \(P(y)\). Puesto que \((∀x)¬P(x)\), se tiene que \(¬P(y)\) que es una contradicción con \(P(y)\).
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) -- 1ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := by intro h1 -- h1 : ∃ x, P x -- ⊢ False rcases h1 with ⟨y, hy : P y⟩ have h2 : ¬P y := h y exact h2 hy -- 2ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := by intro h1 -- h1 : ∃ x, P x -- ⊢ False rcases h1 with ⟨y, hy : P y⟩ exact (h y) hy -- 3ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := by rintro ⟨y, hy : P y⟩ exact (h y) hy -- 4ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := fun ⟨y, hy⟩ ↦ (h y) hy -- 5ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := not_exists_of_forall_not h -- 6ª demostración -- =============== example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := by aesop -- Lemas usados -- ============ -- variable (q : Prop) -- #check (not_exists_of_forall_not : (∀ x, P x → q) → (∃ x, P x) → q) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 33.
