La semana en Calculemus (13 de enero de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. En ℝ, y > x² ⊢ y > 0 ∨ y < -1
- 2. En ℝ, -y > x² + 1 ⊢ y > 0 ∨ y < -1
- 3. En ℝ, si x < |y|, entonces x < y ó x < -y
- 4. En ℝ, x ≤ |x|
- 5. En ℝ, -x ≤ |x|
A continuación se muestran las soluciones.
1. En ℝ, y > x² ⊢ y > 0 ∨ y < -1
Demostrar con Lean4 que en \(ℝ\), \(y > x^2 ⊢ y > 0 ∨ y < -1\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : y > x^2) : y > 0 ∨ y < -1 := by sorry |
Demostración en lenguaje natural
Usando el lema
\[ (∀ x ∈ ℝ)[x² ≥ 0] \]
se tiene que
\begin{align}
y &> x² &&\text{[por hipótesis]} \\
&≥ 0 &&\text{[por el lema]}
\end{align}
Por tanto, \(y > 0\) y, al verificar la primera parte de la diyunción, se verifica la disyunción.
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 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example (h : y > x^2) : y > 0 ∨ y < -1 := by have h1 : y > 0 := by calc y > x^2 := h _ ≥ 0 := pow_two_nonneg x show y > 0 ∨ y < -1 exact Or.inl h1 -- 2ª demostración -- =============== example (h : y > x^2) : y > 0 ∨ y < -1 := by left -- ⊢ y > 0 calc y > x^2 := h _ ≥ 0 := pow_two_nonneg x -- 3ª demostración -- =============== example (h : y > x^2) : y > 0 ∨ y < -1 := by left -- ⊢ y > 0 linarith [pow_two_nonneg x] -- 4ª demostración -- =============== example (h : y > x^2) : y > 0 ∨ y < -1 := by { left ; linarith [pow_two_nonneg x] } -- Lema usado -- ========== -- #check (pow_two_nonneg x : 0 ≤ x ^ 2) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 38.
2. En ℝ, -y > x² + 1 ⊢ y > 0 ∨ y < -1
Demostrar con Lean4 que en \(ℝ\),
\[ -y > x² + 1 ⊢ y > 0 ∨ y < -1 \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by sorry |
Demostración en lenguaje natural
Usaremos los siguientes lemas
\begin{align}
&(∀ b, c ∈ ℝ)[b ≤ c → ∀ (a : ℝ), b + a ≤ c + a)] \tag{L1} \\
&(∀ a ∈ ℝ)[0 ≤ a²] \tag{L2} \\
&(∀ a ∈ ℝ)[0 + a = a] \tag{L3} \\
&(∀ a, b ∈ ℝ)[a < -b ↔ b < -a] \tag{L4}
\end{align}
Se tiene
\begin{align}
-y &> x^2 + 1 &&\text{[por la hipótesis]} \\
&≥ 0 + 1 &&\text{[por L1 y L2]} \\
&= 1 &&\text{[por L3]}
\end{align}
Por tanto,
\[ -y > 1 \]
y, aplicando el lema L4, se tiene
\[ y < -1 \]
Como se verifica la segunda parte de la disyunción, se verifica la disyunción.
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 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by have h1 : -y > 1 := by calc -y > x^2 + 1 := by exact h _ ≥ 0 + 1 := add_le_add_right (pow_two_nonneg x) 1 _ = 1 := zero_add 1 have h2: y < -1 := lt_neg.mp h1 show y > 0 ∨ y < -1 exact Or.inr h2 -- 2ª demostración -- =============== example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by have h1 : -y > 1 := by linarith [pow_two_nonneg x] have h2: y < -1 := lt_neg.mp h1 show y > 0 ∨ y < -1 exact Or.inr h2 -- 3ª demostración -- =============== example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by have h1: y < -1 := by linarith [pow_two_nonneg x] show y > 0 ∨ y < -1 exact Or.inr h1 -- 4ª demostración -- =============== example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by right -- ⊢ y < -1 linarith [pow_two_nonneg x] -- 5ª demostración -- =============== example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by { right ; linarith [pow_two_nonneg x] } -- Lemas usados -- ============ -- variable (a b c : ℝ) -- #check (add_le_add_right : b ≤ c → ∀ (a : ℝ), b + a ≤ c + a) -- #check (lt_neg : a < -b ↔ b < -a) -- #check (pow_two_nonneg a : 0 ≤ a ^ 2) -- #check (zero_add a : 0 + a = a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 39.
3. En ℝ, si x < |y|, entonces x < y ó x < -y
Demostrar con Lean4 que en \(ℝ\), si \(x < |y|\), entonces \(x < y\) ó \(x < -y\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example : x < |y| → x < y ∨ x < -y := by sorry |
Demostración en lenguaje natural
Se demostrará por casos según \(y ≥ 0\).
Primer caso: Supongamos que \(y ≥ 0\). Entonces, \(|y| = y\) y, por tanto, \(x < y\).
Segundo caso: Supongamos que \(y < 0\). Entonces, \(|y| = -y\) y, por tanto, \(x < -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 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example : x < |y| → x < y ∨ x < -y := by intro h1 -- h1 : x < |y| -- ⊢ x < y ∨ x < -y cases' le_or_gt 0 y with h2 h3 . -- h2 : 0 ≤ y left -- ⊢ x < y rwa [abs_of_nonneg h2] at h1 . -- h3 : 0 > y right -- ⊢ x < -y rwa [abs_of_neg h3] at h1 -- 2ª demostración -- =============== example : x < |y| → x < y ∨ x < -y := lt_abs.mp -- Lemas usados -- ============ -- #check (le_or_gt x y : x ≤ y ∨ x > y) -- #check (abs_of_nonneg : 0 ≤ x → abs x = x) -- #check (abs_of_neg : x < 0 → abs x = -x) -- #check (lt_abs : x < |y| ↔ x < y ∨ x < -y) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 38.
4. En ℝ, x ≤ |x|
Demostrar con Lean4 que en \(ℝ\), \(x ≤ |x|\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x : ℝ} example : x ≤ |x| := by sorry |
Demostración en lenguaje natural
Se usarán los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)[0 ≤ x → |x| = x] \tag{L1} \\
&(∀ x, y ∈ ℝ)[x < y → x ≤ y] \tag{L2} \\
&(∀ x ∈ ℝ)[x ≤ 0 → x ≤ -x] \tag{L3} \\
&(∀ x ∈ ℝ)[x < 0 → |x| = -x] \tag{L4}
\end{align}
Se demostrará por casos según \(x ≥ 0\):
Primer caso: Supongamos que \(x ≥ 0\). Entonces,
\begin{align}
x &≤ x \\
&= |x| &&\text{[por L1]}
\end{align}
Segundo caso: Supongamos que \(x < 0\). Entonces, por el L2, se tiene
\[ x ≤ 0 \tag{1} \]
Por tanto,
\begin{align}
x &≤ -x &&\text{[por L3 y (1)]} \\
&= |x| &&\text{[por L4]}
\end{align}
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 |
import Mathlib.Data.Real.Basic variable {x : ℝ} -- 1ª demostración -- =============== example : x ≤ |x| := by cases' le_or_gt 0 x with h1 h2 . -- h1 : 0 ≤ x show x ≤ |x| calc x ≤ x := le_refl x _ = |x| := (abs_of_nonneg h1).symm . -- h2 : 0 > x have h3 : x ≤ 0 := le_of_lt h2 show x ≤ |x| calc x ≤ -x := le_neg_self_iff.mpr h3 _ = |x| := (abs_of_neg h2).symm -- 2ª demostración -- =============== example : x ≤ |x| := by cases' le_or_gt 0 x with h1 h2 . -- h1 : 0 ≤ x rw [abs_of_nonneg h1] . -- h2 : 0 > x rw [abs_of_neg h2] -- ⊢ x ≤ -x apply Left.self_le_neg -- ⊢ x ≤ 0 exact le_of_lt h2 -- 3ª demostración -- =============== example : x ≤ |x| := by rcases (le_or_gt 0 x) with h1 | h2 . -- h1 : 0 ≤ x rw [abs_of_nonneg h1] . -- h1 : 0 ≤ x rw [abs_of_neg h2] linarith -- 4ª demostración -- =============== example : x ≤ |x| := le_abs_self x -- Lemas usados -- ============ -- variable (y : ℝ) -- #check (Left.self_le_neg : x ≤ 0 → x ≤ -x) -- #check (abs_of_neg : x < 0 → |x| = -x) -- #check (abs_of_nonneg : 0 ≤ x → |x| = x) -- #check (le_abs_self x : x ≤ |x|) -- #check (le_neg_self_iff : x ≤ -x ↔ x ≤ 0) -- #check (le_of_lt : x < y → x ≤ y) -- #check (le_or_gt x y : x ≤ y ∨ x > y) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 38.
5. En ℝ, -x ≤ |x|
Demostrar con Lean4 que en \(ℝ\), \(-x ≤ |x|\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x : ℝ} example : -x ≤ |x| := by sorry |
Demostración en lenguaje natural
Se usarán los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)[0 ≤ x → -x ≤ x] \tag{L1} \\
&(∀ x ∈ ℝ)[0 ≤ x → |x| = x] \tag{L2} \\
&(∀ x ∈ ℝ)[x ≤ x] \tag{L3} \\
&(∀ x ∈ ℝ)[x < 0 → |x| = -x] \tag{L4}
\end{align}
Se demostrará por casos según \(x ≥ 0\):
Primer caso: Supongamos que \(x ≥ 0\). Entonces,
\begin{align}
-x &≤ x &&\text{[por L1]} \\
&= |x| &&\text{[por L2]}
\end{align}
Segundo caso: Supongamos que \(x < 0\). Entonces,
\begin{align}
-x &≤ -x &&\text{[por L3]} \\
&= |x| &&\text{[por L4]}
\end{align}
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 |
import Mathlib.Data.Real.Basic variable {x : ℝ} -- 1ª demostración -- =============== example : -x ≤ |x| := by cases' (le_or_gt 0 x) with h1 h2 . -- h1 : 0 ≤ x show -x ≤ |x| calc -x ≤ x := by exact neg_le_self h1 _ = |x| := (abs_of_nonneg h1).symm . -- h2 : 0 > x show -x ≤ |x| calc -x ≤ -x := by exact le_refl (-x) _ = |x| := (abs_of_neg h2).symm -- 2ª demostración -- =============== example : -x ≤ |x| := by cases' (le_or_gt 0 x) with h1 h2 . -- h1 : 0 ≤ x rw [abs_of_nonneg h1] -- ⊢ -x ≤ x exact neg_le_self h1 . -- h2 : 0 > x rw [abs_of_neg h2] -- 3ª demostración -- =============== example : -x ≤ |x| := by rcases (le_or_gt 0 x) with h1 | h2 . -- h1 : 0 ≤ x rw [abs_of_nonneg h1] -- ⊢ -x ≤ x linarith . -- h2 : 0 > x rw [abs_of_neg h2] -- 4ª demostración -- =============== example : -x ≤ |x| := neg_le_abs_self x -- Lemas usados -- ============ -- variable (y : ℝ) -- #check (abs_of_neg : x < 0 → |x| = -x) -- #check (abs_of_nonneg : 0 ≤ x → |x| = x) -- #check (le_or_gt x y : x ≤ y ∨ x > y) -- #check (le_refl x : x ≤ x) -- #check (neg_le_abs_self x : -x ≤ |x|) -- #check (neg_le_self : 0 ≤ x → -x ≤ x) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 38.