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
Sea \(y\) un elemento cualquiera. Tenemos que demostrar \(¬P(y)\). Para ello, supongamos que \(P(y)\). Entonces, \((∃x)P(x)\) que es una contradicción con la hipótesis,
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 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) -- 1ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by intros y h1 -- y : α -- h1 : P x -- ⊢ False apply h -- ⊢ ∃ x, P x existsi y -- ⊢ P y exact h1 -- 2ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by intros y h1 -- y : α -- h1 : P x -- ⊢ False apply h -- ⊢ ∃ x, P x use y -- ⊢ P y exact h1 -- 3ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by intros y h1 -- y : α -- h1 : P x -- ⊢ False apply h -- ⊢ ∃ x, P x exact ⟨y, h1⟩ -- 4ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by intros y h1 -- y : α -- h1 : P x -- ⊢ False exact h ⟨y, h1⟩ -- 5ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := fun y h1 ↦ h ⟨y, h1⟩ -- 6ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by push_neg at h exact h -- 7ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := not_exists.mp h -- 8ª demostración -- =============== example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := by aesop -- Lemas usados -- ============ -- #check (not_exists : (¬∃ x, P x) ↔ ∀ (x : α), ¬P x) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 33.
