{"id":8008,"date":"2023-08-27T17:42:49","date_gmt":"2023-08-27T15:42:49","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8008"},"modified":"2023-08-27T17:42:49","modified_gmt":"2023-08-27T15:42:49","slug":"26-ago-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/26-ago-23\/","title":{"rendered":"La semana en Calculemus (26 de agosto de 2023)"},"content":{"rendered":"\n<p>Esta semana he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. Si G es un grupo y a, b \u2208 G, tales que ab = 1 entonces a\u207b\u00b9 = b<\/a><\/li>\n<li><a href=\"#ej2\">2. Si G es un grupo y a, b \u2208 G, entonces (ab)\u207b\u00b9 = b\u207b\u00b9a\u207b\u00b9<\/a><\/li>\n<li><a href=\"#ej3\">3. En \u211d, si a \u2264 b, b &lt; c, c \u2264 d y d &lt; e, entonces a &lt; e<\/a><\/li>\n<li><a href=\"#ej4\">4. En \u211d, si 2a \u2264 3b, 1 \u2264 a y c = 2, entonces c + a \u2264 5b<\/a><\/li>\n<li><a href=\"#ej5\">5. En \u211d, si 1 \u2264 a y b \u2264 d, entonces 2 + a + e\u1d47 \u2264 3a + e\u1d48<\/a><\/li>\n<\/ul>\n<p>A continuaci\u00f3n se muestran las soluciones.<br \/>\n<!--more--><br \/>\n<a name=\"ej1\"><\/a><\/p>\n<h3>1. Si G es un grupo y a, b \u2208 G, tales que ab = 1 entonces a\u207b\u00b9 = b<\/h3>\n<p>Demostrar con Lean4 que si &#92;(G&#92;) es un grupo y &#92;(a, b &#92;in G&#92;) tales que &#92;(ab = 1&#92;) entonces &#92;(a^{-1} = b&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Defs\n\nvariable {G : Type _} [Group G]\nvariable (a b : G)\n\nexample\n  (h : a * b = 1)\n  : a\u207b\u00b9 = b :=\nsorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se tiene a partir de la siguente cadena de igualdades<br \/>\n&#92;begin{align}<br \/>\n   a\u207b\u00b9 &amp;= a\u207b\u00b9\u00b71         &amp;&amp;&#92;text{[por producto por uno]} &#92;&#92;<br \/>\n       &amp;= a\u207b\u00b9\u00b7(a\u00b7b)     &amp;&amp;&#92;text{[por hip\u00f3tesis]} &#92;&#92;<br \/>\n       &amp;= (a\u207b\u00b9\u00b7a)\u00b7b     &amp;&amp;&#92;text{[por asociativa]} &#92;&#92;<br \/>\n       &amp;= 1\u00b7b           &amp;&amp;&#92;text{[por producto con inverso]} &#92;&#92;<br \/>\n       &amp;= b             &amp;&amp;&#92;text{[por producto por uno]}<br \/>\n&#92;end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Defs\n\nvariable {G : Type _} [Group G]\nvariable (a b : G)\n\n-- 1\u00ba demostraci\u00f3n\nexample\n  (h : a * b = 1)\n  : a\u207b\u00b9 = b :=\ncalc\n  a\u207b\u00b9 = a\u207b\u00b9 * 1       := by rw [mul_one]\n    _ = a\u207b\u00b9 * (a * b) := by rw [h]\n    _ = (a\u207b\u00b9 * a) * b := by rw [mul_assoc]\n    _ = 1 * b         := by rw [mul_left_inv]\n    _ = b             := by rw [one_mul]\n\n-- 2\u00ba demostraci\u00f3n\nexample\n  (h : a * b = 1)\n  : a\u207b\u00b9 = b :=\ncalc\n  a\u207b\u00b9 = a\u207b\u00b9 * 1       := by simp\n    _ = a\u207b\u00b9 * (a * b) := by simp [h]\n    _ = (a\u207b\u00b9 * a) * b := by simp\n    _ = 1 * b         := by simp\n    _ = b             := by simp\n\n-- 3\u00ba demostraci\u00f3n\nexample\n  (h : a * b = 1)\n  : a\u207b\u00b9 = b :=\ncalc\n  a\u207b\u00b9 =  a\u207b\u00b9 * (a * b) := by simp [h]\n    _ =  b             := by simp\n\n-- 4\u00ba demostraci\u00f3n\nexample\n  (h : a * b = 1)\n  : a\u207b\u00b9 = b :=\nby exact inv_eq_of_mul_eq_one_right h\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/CS_de_inverso.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 12.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. Si G es un grupo y a, b \u2208 G, entonces (ab)\u207b\u00b9 = b\u207b\u00b9a\u207b\u00b9<\/h3>\n<p>Demostrar con Lean4 que si &#92;(G&#92;) es un grupo y &#92;(a, b &#92;in G&#92;), entonces &#92;((ab)^{-1} = b^{-1}a^{-1}&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Defs\n\nvariable {G : Type _} [Group G]\nvariable (a b : G)\n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nsorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Teniendo en cuenta la propiedad<br \/>\n   &#92;[\u2200 a&#92; b \u2208 R, ab = 1 \u2192 a\u207b\u00b9 = b,&#92;]<br \/>\nbasta demostrar que<br \/>\n   &#92;[(a\u00b7b)\u00b7(b\u207b\u00b9\u00b7a\u207b\u00b9) = 1.&#92;]<br \/>\nLa identidad anterior se demuestra mediante la siguiente cadena de igualdades<br \/>\n&#92;begin{align}<br \/>\n   (a\u00b7b)\u00b7(b\u207b\u00b9\u00b7a\u207b\u00b9) &amp;= a\u00b7(b\u00b7(b\u207b\u00b9\u00b7a\u207b\u00b9))   &amp;&amp;&#92;text{[por la asociativa]} &#92;&#92;<br \/>\n                   &amp;= a\u00b7((b\u00b7b\u207b\u00b9)\u00b7a\u207b\u00b9)   &amp;&amp;&#92;text{[por la asociativa]} &#92;&#92;<br \/>\n                   &amp;= a\u00b7(1\u00b7a\u207b\u00b9)         &amp;&amp;&#92;text{[por producto con inverso]} &#92;&#92;<br \/>\n                   &amp;= a\u00b7a\u207b\u00b9             &amp;&amp;&#92;text{[por producto con uno]} &#92;&#92;<br \/>\n                   &amp;= 1                 &amp;&amp;&#92;text{[por producto con<br \/>\n                   inverso]}<br \/>\n&#92;end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Defs\n\nvariable {G : Type _} [Group G]\nvariable (a b : G)\n\nlemma aux : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\ncalc\n  (a * b) * (b\u207b\u00b9 * a\u207b\u00b9)\n    = a * (b * (b\u207b\u00b9 * a\u207b\u00b9)) := by rw [mul_assoc]\n  _ = a * ((b * b\u207b\u00b9) * a\u207b\u00b9) := by rw [mul_assoc]\n  _ = a * (1 * a\u207b\u00b9)         := by rw [mul_right_inv]\n  _ = a * a\u207b\u00b9               := by rw [one_mul]\n  _ = 1                     := by rw [mul_right_inv]\n\n-- 1\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n  have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\n    aux a b\n  show (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9\n  exact inv_eq_of_mul_eq_one_right h1\n\n-- 3\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n  have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\n    aux a b\n  show (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9\n  simp [h1]\n\n-- 4\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n  have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\n    aux a b\n  simp [h1]\n\n-- 5\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n  apply inv_eq_of_mul_eq_one_right\n  rw [aux]\n\n-- 6\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby exact mul_inv_rev a b\n\n-- 7\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby simp\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Inverso_del_producto.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 12.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. En \u211d, si a \u2264 b, b &lt; c, c \u2264 d y d &lt; e, entonces a &lt; e<\/h3>\n<p>Demostrar con Lean4 que si &#92;(a&#92;), &#92;(b&#92;), &#92;(c&#92;), &#92;(d&#92;) y &#92;(e&#92;) son n\u00fameros reales tales  &#92;(a &#92;leq b&#92;), &#92;(b &lt; c&#92;), &#92;(c &#92;leq d&#92;) y &#92;(d &lt; e&#92;), entonces &#92;(a &lt; e&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (a b c d e : \u211d)\n\nexample\n  (h1 : a \u2264 b)\n  (h2 : b < c)\n  (h3 : c \u2264 d)\n  (h4 : d < e) :\n  a < e :=\nsorry\n<\/pre>\n<p><b>Demostraciones en lenguaje natural (LN)<\/b><\/p>\n<p><b>1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>Por la siguiente cadena de desigualdades<br \/>\n&#92;begin{align}<br \/>\n   a &amp;&#92;leq b    &amp;&amp;&#92;text{[por la hip\u00f3tesis 1 (&#92;(a &#92;leq b&#92;))]} &#92;&#92;<br \/>\n     &amp;&lt; c       &amp;&amp;&#92;text{[por la hip\u00f3tesis 2 (&#92;(b &lt; c&#92;))]} &#92;&#92;<br \/>\n     &amp;&#92;leq d    &amp;&amp;&#92;text{[por la hip\u00f3tesis 3 (&#92;(c &#92;leq d&#92;))]} &#92;&#92;<br \/>\n     &amp;&lt; e       &amp;&amp;&#92;text{[por la hip\u00f3tesis 4 (&#92;(d &lt; e&#92;))]}<br \/>\n&#92;end{align}<\/p>\n<p><b>2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>A partir de las hip\u00f3tesis 1 (&#92;(a &#92;leq b&#92;)) y 2 (&#92;(b &lt; c&#92;)) se tiene<br \/>\n&#92;[a &lt; c&#92;]<br \/>\nque, junto la hip\u00f3tesis 3 (&#92;(c &#92;leq d&#92;)) da<br \/>\n&#92;[a &lt; d&#92;]<br \/>\nque, junto la hip\u00f3tesis 4 (&#92;(d &lt; e&#92;)) da<br \/>\n&#92;[a &lt; e.&#92;]<\/p>\n<p><b>3\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>Demostrar &#92;(a &lt; e&#92;), por la hip\u00f3tesis 1 (&#92;(a &#92;leq b&#92;)) se reduce a<br \/>\n&#92;[b &lt; e&#92;]<br \/>\nque, por la hip\u00f3tesis 2 (&#92;(b &lt; c&#92;)), se reduce a<br \/>\n&#92;[c &lt; e&#92;]<br \/>\nque, por la hip\u00f3tesis 3 (&#92;(c &#92;leq d&#92;)), se reduce a<br \/>\n&#92;[d &lt; e&#92;]<br \/>\nque es cierto, por la hip\u00f3tesis 4.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (a b c d e : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : a \u2264 b)\n  (h2 : b < c)\n  (h3 : c \u2264 d)\n  (h4 : d < e) :\n  a < e :=\ncalc\n  a \u2264 b := h1\n  _ < c := h2\n  _ \u2264 d := h3\n  _ < e := h4\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : a \u2264 b)\n  (h2 : b < c)\n  (h3 : c \u2264 d)\n  (h4 : d < e) :\n  a < e :=\nby\n  have h5 : a < c := lt_of_le_of_lt h1 h2\n  have h6 : a < d := lt_of_lt_of_le h5 h3\n  show a < e\n  exact lt_trans h6 h4\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : a \u2264 b)\n  (h2 : b < c)\n  (h3 : c \u2264 d)\n  (h4 : d < e) :\n  a < e :=\nby\n  apply lt_of_le_of_lt h1\n  apply lt_trans h2\n  apply lt_of_le_of_lt h3\n  exact h4\n\n-- El desarrollo de la prueba es\n--\n--    a b c d e : \u211d,\n--    h1 : a \u2264 b,\n--    h2 : b < c,\n--    h3 : c \u2264 d,\n--    h4 : d < e\n--    \u22a2 a < e\n-- apply lt_of_le_of_lt h1,\n--    \u22a2 b < e\n-- apply lt_trans h2,\n--    \u22a2 c < e\n-- apply lt_of_le_of_lt h3,\n--    \u22a2 d < e\n-- exact h4,\n--    no goals\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : a \u2264 b)\n  (h2 : b < c)\n  (h3 : c \u2264 d)\n  (h4 : d < e) :\n  a < e :=\nby linarith\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Cadena_de_desigualdades.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 14.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. En \u211d, si 2a \u2264 3b, 1 \u2264 a y c = 2, entonces c + a \u2264 5b<\/h3>\n<p>Demostrar con Lean4 que si &#92;(a&#92;), &#92;(b&#92;) y &#92;(c&#92;) son n\u00fameros reales tales que &#92;(2a &#92;leq 3b&#92;), &#92;(1 &#92;leq a&#92;) y &#92;(c = 2&#92;), entonces &#92;(c + a &#92;leq 5b&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (a b c : \u211d)\n\nexample\n  (h1 : 2 * a \u2264 3 * b)\n  (h2 : 1 \u2264 a)\n  (h3 : c = 2)\n  : c + a \u2264 5 * b :=\nsorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Por la siguiente cadena de desigualdades<br \/>\n&#92;begin{align}<br \/>\n   c + a &amp;= 2 + a         &amp;&amp;&#92;text{[por la hip\u00f3tesis 3 (&#92;(c = 2&#92;))]} &#92;&#92;<br \/>\n         &amp;&#92;leq 2\u00b7a + a    &amp;&amp;&#92;text{[por la hip\u00f3tesis 2 (&#92;(1 &#92;leq a&#92;))]} &#92;&#92;<br \/>\n         &amp;= 3\u00b7a           &#92;&#92;<br \/>\n         &amp;&#92;leq 9\/2\u00b7b      &amp;&amp;&#92;text{[por la hip\u00f3tesis 1 (&#92;(2\u00b7a &#92;leq 3\u00b7b&#92;))]} &#92;&#92;<br \/>\n         &amp;&#92;leq 5\u00b7b<br \/>\n&#92;end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (a b c : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : 2 * a \u2264 3 * b)\n  (h2 : 1 \u2264 a)\n  (h3 : c = 2)\n  : c + a \u2264 5 * b :=\ncalc\n  c + a = 2 + a     := by rw [h3]\n      _ \u2264 2 * a + a := by linarith only [h2]\n      _ = 3 * a     := by linarith only []\n      _ \u2264 9\/2 * b   := by linarith only [h1]\n      _ \u2264 5 * b     := by linarith\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : 2 * a \u2264 3 * b)\n  (h2 : 1 \u2264 a)\n  (h3 : c = 2)\n  : c + a \u2264 5 * b :=\nby linarith\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Inecuaciones.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 14.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. En \u211d, si 1 \u2264 a y b \u2264 d, entonces 2 + a + e\u1d47 \u2264 3a + e\u1d48<\/h3>\n<p>Demostrar con Lean4 que si &#92;(a&#92;), &#92;(b&#92;) y &#92;(d&#92;) n\u00fameros reales tales que &#92;(1 &#92;leq a&#92;) y &#92;(b &#92;leq d&#92;), entonces &#92;(2 + a + e^b &#92;leq 3a + e^d&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\n\nopen Real\n\nvariable (a b d : \u211d)\n\nexample\n  (h1 : 1 \u2264 a)\n  (h2 : b \u2264 d)\n  : 2 + a + exp b \u2264 3 * a + exp d :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>De la primera hip\u00f3tesis (&#92;(1 &#92;leq a&#92;)), multiplicando por &#92;(2&#92;), se obtiene<br \/>\n&#92;[2 &#92;leq 2a&#92;]<br \/>\ny, sumando a ambos lados, se tiene<br \/>\n&#92;[2 + a &#92;leq 3a &#92;tag{1}&#92;]<\/p>\n<p>De la hip\u00f3tesis 2 (&#92;(b &#92;leq d&#92;)) y de la monoton\u00eda de la funci\u00f3n exponencial se tiene<br \/>\n&#92;[e^b &#92;leq e^d &#92;tag{2} &#92;]<\/p>\n<p>Finalmente, de (1) y (2) se tiene<br \/>\n&#92;[2 + a + e^b &#92;leq 3a + e^d&#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\n\nopen Real\n\nvariable (a b d : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : 1 \u2264 a)\n  (h2 : b \u2264 d)\n  : 2 + a + exp b \u2264 3 * a + exp d :=\nby\n  have h3 : 2 + a \u2264 3 * a := calc\n    2 + a = 2 * 1 + a := by linarith only []\n        _ \u2264 2 * a + a := by linarith only [h1]\n        _ \u2264 3 * a     := by linarith only []\n  have h4 : exp b \u2264 exp d := by\n    linarith only [exp_le_exp.mpr h2]\n  show 2 + a + exp b \u2264 3 * a + exp d\n  exact add_le_add h3 h4\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : 1 \u2264 a)\n  (h2 : b \u2264 d)\n  : 2 + a + exp b \u2264 3 * a + exp d :=\ncalc\n  2 + a + exp b\n    \u2264 3 * a + exp b := by linarith only [h1]\n  _ \u2264 3 * a + exp d := by linarith only [exp_le_exp.mpr h2]\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : 1 \u2264 a)\n  (h2 : b \u2264 d)\n  : 2 + a + exp b \u2264 3 * a + exp d :=\nby linarith [exp_le_exp.mpr h2]\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Inecuaciones_con_exponenciales.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 15.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. Si G es un grupo y a, b \u2208 G, tales que ab = 1 entonces a\u207b\u00b9 = b 2. Si G es un grupo y a, b \u2208 G, entonces (ab)\u207b\u00b9 = b\u207b\u00b9a\u207b\u00b9 3. En \u211d, si a \u2264&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[335],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8008"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=8008"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8008\/revisions"}],"predecessor-version":[{"id":8009,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8008\/revisions\/8009"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8008"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8008"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8008"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}