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
Por reducción al absurdo, supongamos que \(¬(∃x)¬P(x)\). Para obtener contradicción, demostraremos la negación de la hipótesis; es que \((∀x)P(x)\). Para ello, sea \(y\) un elemento cualquiera y tenemos que demostrar \(P(y)\). De nuevo, lo haremos por reducción al absurdo: Para ello, supongamos que \(¬P(y)\). Entonces, se tiene que \((∃x)¬P(x)\) en contradicción con nuestro primer supuesto de \(¬(∃x)¬P(x)\).
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 |
import Mathlib.Tactic variable {α : Type _} variable (P : α → Prop) -- 1ª demostración -- =============== example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := by by_contra h1 -- h1 : ¬∃ x, ¬P x -- ⊢ False apply h -- ⊢ ∀ (x : α), P x intro y -- y : α -- ⊢ P y show P y by_contra h2 -- h2 : ¬P y -- ⊢ False exact h1 ⟨y, h2⟩ -- 2ª demostración -- =============== example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := not_forall.mp h -- 3ª demostración -- =============== example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := by aesop -- Lemas usados -- ============ -- #check (not_forall : (¬∀ 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.
