En ℝ, si 1 < a, entonces a < aa
Demostrar con Lean4 que en \(ℝ\), si \(1 < a\), entonces \(a < aa\)
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {a : ℝ} example (h : 1 < a) : a < a * a := by sorry |
1. Demostración en lenguaje natural
Se usarán los siguientes lemas
\begin{align}
&0 < 1 \tag{L1} \\
&(∀ a ∈ ℝ[1a = a] \tag{L2} \\
&(∀ a, b, c ∈ ℝ)[0 < a → (ba < ca ↔ b < c)] \tag{L3}
\end{align}
En primer lugar, tenemos que
\[ 0 < a \tag{1} \]
ya que
\begin{align}
0 &< 1 &&\text{[por L1]} \\
&< a &&\text{[por la hipótesis]}
\end{align}
Entonces,
\begin{align}
a &= 1a &&\text{[por L2]} \\
&< aa &&\text{[por L3, (1) y la hipótesis]}
\end{align}
2. 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 |
import Mathlib.Data.Real.Basic variable {a : ℝ} -- 1ª demostración -- =============== example (h : 1 < a) : a < a * a := by have h1 : 0 < a := calc 0 < 1 := zero_lt_one _ < a := h show a < a * a calc a = 1 * a := (one_mul a).symm _ < a * a := (mul_lt_mul_right h1).mpr h -- Comentarios: La táctica (convert e) genera nuevos subojetivos cuya -- conclusiones son las diferencias entre el tipo de e y la conclusión. -- 2ª demostración -- =============== example (h : 1 < a) : a < a * a := by convert (mul_lt_mul_right _).2 h . -- ⊢ a = 1 * a rw [one_mul] . -- ⊢ 0 < a exact lt_trans zero_lt_one h -- Lemas usados -- ============ -- variables (a b c : ℝ) -- #check (mul_lt_mul_right : 0 < a → (b * a < c * a ↔ b < c)) -- #check (one_mul a : 1 * a = a) -- #check (lt_trans : a < b → b < c → a < c) -- #check (zero_lt_one : 0 < 1) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 41.
