Demostrar con Lean4 que en \(\u211d\), si \(1 < a\), entonces \(a < aa\)<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable {a : \u211d}\n\nexample\n (h : 1 < a)\n : a < a * a :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Se usar\u00e1n los siguientes lemas
\n\begin{align}
\n &0 < 1 \tag{L1} \\
\n &(\u2200 a \u2208 \u211d[1a = a] \tag{L2} \\
\n &(\u2200 a, b, c \u2208 \u211d)[0 < a \u2192 (ba < ca \u2194 b < c)] \tag{L3}
\n\end{align}<\/p>\n
En primer lugar, tenemos que
\n\[ 0 < a \tag{1} \]
\nya que
\n\begin{align}
\n 0 &< 1 &&\text{[por L1]} \\
\n &< a &&\text{[por la hip\u00f3tesis]}
\n\end{align}
\nEntonces,
\n\begin{align}
\n a &= 1a &&\text{[por L2]} \\
\n &< aa &&\text{[por L3, (1) y la hip\u00f3tesis]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Real.Basic\nvariable {a : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : 1 < a)\n : a < a * a :=\nby\n have h1 : 0 < a := calc\n 0 < 1 := zero_lt_one\n _ < a := h\n show a < a * a\n calc a = 1 * a := (one_mul a).symm\n _ < a * a := (mul_lt_mul_right h1).mpr h\n\n-- Comentarios: La t\u00e1ctica (convert e) genera nuevos subojetivos cuya\n-- conclusiones son las diferencias entre el tipo de e y la conclusi\u00f3n.\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : 1 < a)\n : a < a * a :=\nby\n convert (mul_lt_mul_right _).2 h\n . -- \u22a2 a = 1 * a\n rw [one_mul]\n . -- \u22a2 0 < a\n exact lt_trans zero_lt_one h\n\n-- Lemas usados\n-- ============\n\n-- variables (a b c : \u211d)\n-- #check (mul_lt_mul_right : 0 < a \u2192 (b * a < c * a \u2194 b < c))\n-- #check (one_mul a : 1 * a = a)\n-- #check (lt_trans : a < b \u2192 b < c \u2192 a < c)\n-- #check (zero_lt_one : 0 < 1)\n<\/pre>\nSe puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/h3>\n