En ℝ, si x ≠ 0 entonces x < 0 ó x > 0
Demostrar con Lean4 que en ℝ, si \(x ≠ 0\) entonces \(x < 0\) ó \(x > 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {x : ℝ} example (h : x ≠ 0) : x < 0 ∨ x > 0 := by sorry |
Demostración en lenguaje natural
Usando el siguiente lema
\[ (∀ x, y ∈ ℝ)[x < y ∨ x = y ∨ y < x] \]
se demuestra distinguiendo tres casos.
Caso 1: Supongamos que \(x < 0\). Entonces, se verifica la disyunción ya
que se verifica su primera parte.
Caso 2: Supongamos que \(x = 0\). Entonces, se tiene una contradicción
con la hipótesis.
Caso 3: Supongamos que \(x > 0\). Entonces, se verifica la disyunción ya
que se verifica su segunda parte.
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 |
import Mathlib.Data.Real.Basic variable {x : ℝ} -- 1ª demostración -- =============== example (h : x ≠ 0) : x < 0 ∨ x > 0 := by rcases lt_trichotomy x 0 with hx1 | hx2 | hx3 . -- hx1 : x < 0 left -- ⊢ x < 0 exact hx1 . -- hx2 : x = 0 contradiction . -- hx3 : 0 < x right -- ⊢ x > 0 exact hx3 -- 2ª demostración -- =============== example (h : x ≠ 0) : x < 0 ∨ x > 0 := Ne.lt_or_lt h -- 3ª demostración -- =============== example (h : x ≠ 0) : x < 0 ∨ x > 0 := by aesop -- Lemas usados -- ============ -- variable (y : ℝ) -- #check (lt_trichotomy x y : x < y ∨ x = y ∨ y < x) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 39.
En Isabelle/HOL
|
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 |
theory Eliminacion_de_la_disyuncion_con_rcases imports Main HOL.Real begin (* 1ª demostración *) lemma fixes x :: real assumes "x ≠ 0" shows "x < 0 ∨ x > 0" proof (cases "x < 0") case True then show ?thesis by simp next case False then have "x ≥ 0" by simp with `x ≠ 0` have "x > 0" by simp then show ?thesis by simp qed (* 2ª demostración *) lemma fixes x :: real assumes "x ≠ 0" shows "x < 0 ∨ x > 0" proof (rule classical) assume "¬ (x < 0 ∨ x > 0)" then have "¬ (x < 0) ∧ ¬ (x > 0)" by simp then have "x ≥ 0 ∧ x ≤ 0" by simp then have "x = 0" by arith with `x ≠ 0` show ?thesis by simp qed (* 3ª demostración *) lemma fixes x :: real assumes "x ≠ 0" shows "x < 0 ∨ x > 0" proof (rule classical) assume "¬ (x < 0 ∨ x > 0)" then have "x = 0" by simp with `x ≠ 0` show ?thesis by simp qed (* 4ª demostración *) lemma fixes x :: real assumes "x ≠ 0" shows "x < 0 ∨ x > 0" using assms by auto end |
