{"id":8015,"date":"2023-09-10T08:20:43","date_gmt":"2023-09-10T06:20:43","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8015"},"modified":"2023-09-10T08:20:43","modified_gmt":"2023-09-10T06:20:43","slug":"09-sep-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/09-sep-23\/","title":{"rendered":"La semana en Calculemus (9 de septiembre 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. En \u211d, |ab| \u2264 (a\u00b2+b\u00b2)\/2<\/a><\/li>\n<li><a href=\"#ej2\">2. En \u211d, min(a,b) = min(b,a)<\/a><\/li>\n<li><a href=\"#ej3\">3. En \u211d, max(a,b) = max(b,a)<\/a><\/li>\n<li><a href=\"#ej4\">4. En \u211d, min(min(a,b),c) = min(a,min(b,c))<\/a><\/li>\n<li><a href=\"#ej5\">5. En \u211d, min(a,b)+c = min(a+c,b+c)<\/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. En \u211d, |ab| \u2264 (a\u00b2+b\u00b2)\/2<\/h3>\n<p>Sean &#92;(a&#92;) y &#92;(b&#92;) n\u00fameros reales. Demostrar con Lean4 que<br \/>\n&#92;[|ab| &#92;leq &#92;frac{a^2 + b^2}{2}&#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 : \u211d)\n\nexample : |a * b| \\\\leq (a ^ 2 + b ^ 2) \/ 2 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Para demostrar<br \/>\n&#92;[|ab| &#92;leq &#92;frac{a^2 + b^2}{2}&#92;]<br \/>\nbasta demostrar estas dos desigualdades<br \/>\n&#92;begin{align}<br \/>\n   ab    &amp;&#92;leq &#92;frac{a^2 + b^2}{2} &#92;tag{1} &#92;&#92;<br \/>\n   -(ab) &amp;&#92;leq &#92;frac{a^2 + b^2}{2} &#92;tag{2}<br \/>\n&#92;end{align}<\/p>\n<p>Para demostrar (1) basta demostrar que<br \/>\n&#92;[2ab &#92;leq a^2 + b^2&#92;]<br \/>\nque se prueba como sigue. En primer lugar, como los cuadrados son no negativos, se tiene<br \/>\n&#92;[(a &#8211; b)^2 &#92;geq 0&#92;]<br \/>\nDesarrollando el cuandrado,<br \/>\n&#92;[a^2 &#8211; 2ab + b^2 &#92;geq 0&#92;]<br \/>\nSumando &#92;(2ab&#92;),<br \/>\n&#92;[a^2 + b^2 &#92;geq 2ab&#92;]<\/p>\n<p>Para demostrar (2) basta demostrar que<br \/>\n&#92;[-2ab &#92;leq a^2 + b^2&#92;]<br \/>\nque se prueba como sigue. En primer lugar, como los cuadrados son no<br \/>\nnegativos, se tiene<br \/>\n&#92;[(a + b)^2 &#92;geq 0&#92;]<br \/>\nDesarrollando el cuandrado,<br \/>\n&#92;[a^2 + 2ab + b^2 &#92;geq 0&#92;]<br \/>\nRestando &#92;(2ab&#92;),<br \/>\n&#92;[a^2 + b^2 &#92;geq -2ab&#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (a b : \u211d)\n\n-- Lemas auxiliares\n-- ================\n\nlemma aux1 : a * b * 2 \u2264 a ^ 2 + b ^ 2 := by\n  have h : 0 \u2264 a ^ 2 - 2 * a * b + b ^ 2\n  calc\n    a ^ 2 - 2 * a * b + b ^ 2\n      = (a - b) ^ 2            := by ring\n    _ \u2265 0                      := pow_two_nonneg (a - b)\n  linarith only [h]\n\nlemma aux2 : -(a * b) * 2 \u2264 a ^ 2 + b ^ 2 := by\n  have h : 0 \u2264 a ^ 2 + 2 * a * b + b ^ 2\n  calc\n    a ^ 2 + 2 * a * b + b ^ 2\n      = (a + b) ^ 2            := by ring\n    _ \u2265 0                      := pow_two_nonneg (a + b)\n  linarith only [h]\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : |a * b| \u2264 (a ^ 2 + b ^ 2) \/ 2 := by\n  have h : (0 : \u211d) < 2 := by norm_num\n  apply abs_le'.mpr\n  constructor\n  { have h1 : a * b * 2 \u2264 a ^ 2 + b ^ 2 := aux1 a b\n    show a * b \u2264 (a ^ 2 + b ^ 2) \/ 2\n    exact (le_div_iff h).mpr h1 }\n  { have h2 : -(a * b) * 2 \u2264 a ^ 2 + b ^ 2 := aux2 a b\n    show -(a * b) \u2264 (a ^ 2 + b ^ 2) \/ 2\n    exact (le_div_iff h).mpr h2 }\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : |a * b| \u2264 (a ^ 2 + b ^ 2) \/ 2 := by\n  have h : (0 : \u211d) < 2 := by norm_num\n  apply abs_le'.mpr\n  constructor\n  { exact (le_div_iff h).mpr (aux1 a b) }\n  { exact (le_div_iff h).mpr (aux2 a b) }\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : |a * b| \u2264 (a ^ 2 + b ^ 2) \/ 2 := by\n  have h : (0 : \u211d) < 2 := by norm_num\n  apply abs_le'.mpr\n  constructor\n  { rw [le_div_iff h]\n    apply aux1 }\n  { rw [le_div_iff h]\n    apply aux2 }\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\/Ejercicio_desigualdades_absolutas.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. 16.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. En \u211d, min(a,b) = min(b,a)<\/h3>\n<p>Demostrar con Lean4 que si &#92;(a&#92;) y &#92;(b&#92;) n\u00fameros reales, entonces &#92;(&#92;min(a, b) = &#92;min(b, a)&#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 : \u211d)\n\nexample : min a b = min b a :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Es consecuencia de la siguiente propiedad<br \/>\n&#92;[&#92;min(a, b) &#92;leq &#92;min(b, a) &#92;tag{1}&#92;]<br \/>\nEn efecto, intercambiando las variables en (1) se obtiene<br \/>\n&#92;[&#92;min(b, a) &#92;leq &#92;min(a, b) &#92;tag{2}&#92;]<br \/>\nFinalmente de (1) y (2) se obtiene<br \/>\n&#92;[&#92;min(b, a) = &#92;min(a, b)&#92;]<\/p>\n<p>Para demostrar (1), se observa que<br \/>\n&#92;begin{align}<br \/>\n   &#92;min(a, b) &amp;&#92;leq b &#92;&#92;<br \/>\n   &#92;min(a, b) &amp;&#92;leq a<br \/>\n&#92;end{align}<br \/>\ny, por tanto,<br \/>\n&#92;[&#92;min(a, b) &#92;leq &#92;min(b, a)&#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (a b : \u211d)\n\n-- Lema auxiliar\n-- =============\n\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\n-- =================================\n\nexample : min a b \u2264 min b a :=\nby\n  have h1 : min a b \u2264 b := min_le_right a b\n  have h2 : min a b \u2264 a := min_le_left a b\n  show min a b \u2264 min b a\n  exact le_min h1 h2\n\n-- 2\u00aa demostraci\u00f3n del lema auxiliar\n-- =================================\n\nexample : min a b \u2264 min b a :=\nby\n  apply le_min\n  { apply min_le_right }\n  { apply min_le_left }\n\n-- 3\u00aa demostraci\u00f3n del lema auxiliar\n-- =================================\n\nlemma aux : min a b \u2264 min b a :=\nby exact le_min (min_le_right a b) (min_le_left a b)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : min a b = min b a :=\nby\n  apply le_antisymm\n  { exact aux a b}\n  { exact aux b a}\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : min a b = min b a :=\nle_antisymm (aux a b) (aux b a)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : min a b = min b a :=\nmin_comm a b\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\/Conmutatividad_del_minimo.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. 17.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. En \u211d, max(a,b) = max(b,a)<\/h3>\n<p>Demostrar con Lean4 que si &#92;(a&#92;) y &#92;(b&#92;) son n\u00fameros reales,  entonces &#92;(&#92;max(a, b) = &#92;max(b, a)&#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 : \u211d)\n\nexample : max a b = max b a :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Es consecuencia de la siguiente propiedad<br \/>\n&#92;[&#92;max(a, b) &#92;leq &#92;max(b, a) &#92;tag{1}&#92;]<br \/>\nEn efecto, intercambiando las variables en (1) se obtiene<br \/>\n&#92;[&#92;max(b, a) &#92;leq &#92;max(a, b) &#92;tag{2}&#92;]<br \/>\nFinalmente de (1) y (2) se obtiene<br \/>\n&#92;[&#92;max(b, a) = &#92;max(a, b)&#92;]<\/p>\n<p>Para demostrar (1), se observa que<br \/>\n&#92;begin{align}<br \/>\n   a &amp;&#92;leq &#92;max(b, a) &#92;&#92;<br \/>\n   b &amp;&#92;leq &#92;max(b, a)<br \/>\n&#92;end{align}<br \/>\ny, por tanto,<br \/>\n&#92;[&#92;max(a, b) &#92;leq &#92;max(b, a)&#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (a b : \u211d)\n\n-- Lema auxiliar\n-- =============\n\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\n-- =================================\n\nexample : max a b \u2264 max b a :=\nby\n  have h1 : a \u2264 max b a := le_max_right b a\n  have h2 : b \u2264 max b a := le_max_left b a\n  show max a b \u2264 max b a\n  exact max_le h1 h2\n\n-- 2\u00aa demostraci\u00f3n del lema auxiliar\n-- =================================\n\nexample : max a b \u2264 max b a :=\nby\n  apply max_le\n  { apply le_max_right }\n  { apply le_max_left }\n\n-- 3\u00aa demostraci\u00f3n del lema auxiliar\n-- =================================\n\nlemma aux : max a b \u2264 max b a :=\nby exact max_le (le_max_right b a) (le_max_left b a)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : max a b = max b a :=\nby\n  apply le_antisymm\n  { exact aux a b}\n  { exact aux b a}\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : max a b = max b a :=\nle_antisymm (aux a b) (aux b a)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : max a b = max b a :=\nmax_comm a b\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\/Conmutatividad_del_maximo.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. 17.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. En \u211d, min(min(a,b),c) = min(a,min(b,c))<\/h3>\n<p>Demostrar con Lean4 que &#92;(a&#92;), &#92;(b&#92;) y &#92;(c&#92;) n\u00fameros reales, entonces &#92;(&#92;min(&#92;min(a, b), c) = &#92;min(a, &#92;min(b, c))&#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  min (min a b) c = min a (min b c) :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Por la propiedad antisim\u00e9trica, la igualdad es consecuencia de las siguientes desigualdades<br \/>\n&#92;begin{align}<br \/>\n   &#92;min(&#92;min(a, b), c) &amp;&#92;leq &#92;min(a, &#92;min(b, c)) &#92;tag{1} &#92;&#92;<br \/>\n   &#92;min(a, &#92;min(b, c)) &amp;&#92;leq &#92;min(&#92;min(a, b), c) &#92;tag{2}<br \/>\n&#92;end{align}<\/p>\n<p>La (1) es consecuencia de las siguientes desigualdades<br \/>\n&#92;begin{align}<br \/>\n   &#92;min(&#92;min(a, b), c) &amp;&#92;leq a &#92;tag{1a} &#92;&#92;<br \/>\n   &#92;min(&#92;min(a, b), c) &amp;&#92;leq b &#92;tag{1b} &#92;&#92;<br \/>\n   &#92;min(&#92;min(a, b), c) &amp;&#92;leq c &#92;tag{1c}<br \/>\n&#92;end{align}<br \/>\nEn efecto, de (1b) y (1c) se obtiene<br \/>\n&#92;[ &#92;min(&#92;min(a, b), c) &#92;leq &#92;min(b,c) &#92;]<br \/>\nque, junto con (1a) da (1).<\/p>\n<p>La (2) es consecuencia de las siguientes desigualdades<br \/>\n&#92;begin{align}<br \/>\n   &#92;min(a, &#92;min(b, c)) &amp;&#92;leq a &#92;tag{2a} &#92;&#92;<br \/>\n   &#92;min(a, &#92;min(b, c)) &amp;&#92;leq b &#92;tag{2b} &#92;&#92;<br \/>\n   &#92;min(a, &#92;min(b, c)) &amp;&#92;leq c &#92;tag{2c}<br \/>\n&#92;end{align}<br \/>\nEn efecto, de (2a) y (2b) se obtiene<br \/>\n&#92;[ &#92;min(a, &#92;min(b, c)) &#92;leq &#92;min(a, b) &#92;]<br \/>\nque, junto con (2c) da (2).<\/p>\n<p>La demostraci\u00f3n de (1a) es<br \/>\n&#92;[ &#92;min(&#92;min(a, b), c) &#92;leq &#92;min(a, b) &#92;leq a &#92;]<br \/>\nLa demostraci\u00f3n de (1b) es<br \/>\n&#92;[ &#92;min(&#92;min(a, b), c) &#92;leq &#92;min(a, b) &#92;leq b &#92;]<br \/>\nLa demostraci\u00f3n de (2b) es<br \/>\n&#92;[ &#92;min(a, &#92;min(b, c)) &#92;leq &#92;min(b, c) &#92;leq b &#92;]<br \/>\nLa demostraci\u00f3n de (2c) es<br \/>\n&#92;[ &#92;min(a, &#92;min(b, c)) &#92;leq &#92;min(b, c) &#92;leq c &#92;]<br \/>\nLa (1c) y (2a) son inmediatas.<\/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-- Lemas auxiliares\n-- ================\n\nlemma aux1a : min (min a b) c \u2264 a :=\ncalc min (min a b) c\n     \u2264 min a b := by exact min_le_left (min a b) c\n   _ \u2264 a       := min_le_left a b\n\nlemma aux1b : min (min a b) c \u2264 b :=\ncalc min (min a b) c\n     \u2264 min a b := by exact min_le_left (min a b) c\n   _ \u2264 b       := min_le_right a b\n\nlemma aux1c : min (min a b) c \u2264 c :=\nby exact min_le_right (min a b) c\n\n-- 1\u00aa demostraci\u00f3n del lema aux1\nlemma aux1 : min (min a b) c \u2264 min a (min b c) :=\nby\n  apply le_min\n  { show min (min a b) c \u2264 a\n    exact aux1a }\n  { show min (min a b) c \u2264 min b c\n    apply le_min\n    { show min (min a b) c \u2264 b\n      exact aux1b }\n    { show min (min a b) c \u2264 c\n      exact aux1c }}\n\n-- 2\u00aa demostraci\u00f3n del lema aux1\nlemma aux1' : min (min a b) c \u2264 min a (min b c) :=\nle_min aux1a (le_min aux1b aux1c)\n\nlemma aux2a : min a (min b c) \u2264 a :=\nby exact min_le_left a (min b c)\n\nlemma aux2b : min a (min b c) \u2264 b :=\ncalc min a (min b c)\n     \u2264 min b c        := by exact min_le_right a (min b c)\n   _ \u2264 b              := min_le_left b c\n\nlemma aux2c : min a (min b c) \u2264 c :=\ncalc min a (min b c)\n     \u2264 min b c        := by exact min_le_right a (min b c)\n   _ \u2264 c              := min_le_right b c\n\n-- 1\u00aa demostraci\u00f3n del lema aux2\nlemma aux2 : min a (min b c) \u2264 min (min a b) c :=\nby\n  apply le_min\n  { show min a (min b c) \u2264 min a b\n    apply le_min\n    { show min a (min b c) \u2264 a\n      exact aux2a }\n    { show min a (min b c) \u2264 b\n      exact aux2b }}\n  { show min a (min b c) \u2264 c\n    exact aux2c }\n\n-- 2\u00aa demostraci\u00f3n del lema aux2\nlemma aux2' : min a (min b c) \u2264 min (min a b) c :=\nle_min (le_min aux2a aux2b) aux2c\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  min (min a b) c = min a (min b c) :=\nby\n  apply le_antisymm\n  { show min (min a b) c \u2264 min a (min b c)\n    exact aux1 }\n  { show min a (min b c) \u2264 min (min a b) c\n    exact aux2 }\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : min (min a b) c = min a (min b c) :=\nby\n  apply le_antisymm\n  { exact aux1 }\n  { exact aux2 }\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : min (min a b) c = min a (min b c) :=\nle_antisymm aux1 aux2\n\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : min (min a b) c = min a (min b c) :=\nmin_assoc a b c\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\/Asociatividad_del_minimo.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. 18.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. En \u211d, min(a,b)+c = min(a+c,b+c)<\/h3>\n<p>Demostrar con Lean4 que si &#92;(a&#92;), &#92;(b&#92;) y &#92;(c&#92;) n\u00fameros reales, entonces<br \/>\n&#92;[&#92;min(a,b)+c = &#92;min(a+c,b+c)&#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  min a b + c = min (a + c) (b + c) :=\nby sorry\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>Aplicando la propiedad antisim\u00e9trica a las siguientes desigualdades<br \/>\n&#92;begin{align}<br \/>\n   &#92;min(a, b) + c &#92;leq &#92;min(a + c, b + c) &#92;tag{1} &#92;&#92;<br \/>\n   &#92;min(a + c, b + c) &#92;leq &#92;min(a, b) + c &#92;tag{2}<br \/>\n&#92;end{align}<\/p>\n<p>Para demostrar (1) basta demostrar que se verifican las siguientes desigualdades<br \/>\n&#92;begin{align}<br \/>\n   &#92;min(a, b) + c &amp;&#92;leq a + c &#92;tag{1a} &#92;&#92;<br \/>\n   &#92;min(a, b) + c &amp;&#92;leq b + c &#92;tag{1b}<br \/>\n&#92;end{align}<br \/>\nque se tienen porque se verifican las siguientes desigualdades<br \/>\n&#92;begin{align}<br \/>\n   &#92;min(a, b) &amp;&#92;leq a &#92;&#92;<br \/>\n   &#92;min(a, b) &amp;&#92;leq b<br \/>\n&#92;end{align}<\/p>\n<p>Para demostrar (2) basta demostrar que se verifica<br \/>\n&#92;[ &#92;min(a + c, b + c) - c &#92;leq &#92;min(a, b) &#92;]<br \/>\nque se demuestra usando (1); en efecto,<br \/>\n&#92;begin{align}<br \/>\n   &#92;min(a + c, b + c) - c &amp;&#92;leq &#92;min(a + c - c, b + c - c)    &amp;&amp;&#92;text{[por (1)]}&#92;&#92;<br \/>\n                          &amp;= &#92;min(a, b)<br \/>\n&#92;end{align}<\/p>\n<p><b>2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>Por casos seg\u00fan &#92;(a &#92;leq b&#92;).<\/p>\n<p>1\u00ba caso: Supongamos que &#92;(a &#92;leq b&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   &#92;min(a, b) + c &amp;= a + c              &#92;&#92;<br \/>\n                  &amp;= &#92;min(a + c, b + c)<br \/>\n&#92;end{align}<\/p>\n<p>2\u00ba caso: Supongamos que &#92;(a &#92;nleq b&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   &#92;min(a, b) + c &amp;= b + c                &#92;&#92;<br \/>\n                  &amp;= &#92;min(a + c, b + c)<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-- En las demostraciones se usar\u00e1n los siguientes lemas auxiliares\n--    aux1 : min a b + c \u2264 min (a + c) (b + c)\n--    aux2 : min (a + c) (b + c) \u2264 min a b + c\n-- cuyas demostraciones se exponen a continuaci\u00f3n.\n\n-- 1\u00aa demostraci\u00f3n de aux1\nlemma aux1 :\n  min a b + c \u2264 min (a + c) (b + c) :=\nby\n  have h1 : min a b \u2264 a :=\n    min_le_left a b\n  have h2 : min a b + c \u2264 a + c :=\n    add_le_add_right h1 c\n  have h3 : min a b  \u2264 b :=\n    min_le_right a b\n  have h4 : min a b + c \u2264 b + c :=\n    add_le_add_right h3 c\n  show min a b + c \u2264 min (a + c) (b + c)\n  exact le_min h2 h4\n\n-- 2\u00aa demostraci\u00f3n de aux1\nexample :\n  min a b + c \u2264 min (a + c) (b + c) :=\nby\n  apply le_min\n  { apply add_le_add_right\n    exact min_le_left a b }\n  { apply add_le_add_right\n    exact min_le_right a b }\n\n-- 3\u00aa demostraci\u00f3n de aux1\nexample :\n  min a b + c \u2264 min (a + c) (b + c) :=\nle_min (add_le_add_right (min_le_left a b) c)\n       (add_le_add_right (min_le_right a b) c)\n\n-- 1\u00aa demostraci\u00f3n de aux2\nlemma aux2 :\n  min (a + c) (b + c) \u2264 min a b + c :=\nby\n  have h1 : min (a + c) (b + c) + -c \u2264 min a b\n  { calc min (a + c) (b + c) + -c\n         \u2264 min (a + c + -c) (b + c + -c) := aux1\n       _ = min a b                       := by ring_nf }\n  show min (a + c) (b + c) \u2264 min a b + c\n  exact add_neg_le_iff_le_add.mp h1\n\n-- 1\u00aa demostraci\u00f3n del ejercicio\nexample :\n  min a b + c = min (a + c) (b + c) :=\nby\n  have h1 : min a b + c \u2264 min (a + c) (b + c) := aux1\n  have h2 : min (a + c) (b + c) \u2264 min a b + c := aux2\n  show min a b + c = min (a + c) (b + c)\n  exact le_antisymm h1 h2\n\n-- 2\u00aa demostraci\u00f3n del ejercicio\nexample :\n  min a b + c = min (a + c) (b + c) :=\nby\n  apply le_antisymm\n  { show min a b + c \u2264 min (a + c) (b + c)\n    exact aux1 }\n  { show min (a + c) (b + c) \u2264 min a b + c\n    exact aux2 }\n\n-- 3\u00aa demostraci\u00f3n del ejercicio\nexample :\n  min a b + c = min (a + c) (b + c) :=\nby\n  apply le_antisymm\n  { exact aux1 }\n  { exact aux2 }\n\n-- 4\u00aa demostraci\u00f3n del ejercicio\nexample :\n  min a b + c = min (a + c) (b + c) :=\nle_antisymm aux1 aux2\n\n-- 5\u00aa demostraci\u00f3n del ejercicio\nexample : min a b + c = min (a + c) (b + c) :=\nby\n  by_cases h : a \u2264 b\n  { have h1 : a + c \u2264 b + c := add_le_add_right h c\n    calc min a b + c = a + c               := by simp [min_eq_left h]\n                   _ = min (a + c) (b + c) := by simp [min_eq_left h1]}\n  { have h2: b \u2264 a := le_of_not_le h\n    have h3 : b + c \u2264 a + c := add_le_add_right h2 c\n    calc min a b + c = b + c               := by simp [min_eq_right h2]\n                   _ = min (a + c) (b + c) := by simp [min_eq_right h3]}\n\n-- 6\u00aa demostraci\u00f3n del ejercicio\nexample : min a b + c = min (a + c) (b + c) :=\n(min_add_add_right a b c).symm\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\/Minimo_de_suma.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. 18.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. En \u211d, |ab| \u2264 (a\u00b2+b\u00b2)\/2 2. En \u211d, min(a,b) = min(b,a) 3. En \u211d, max(a,b) = max(b,a) 4. En \u211d, min(min(a,b),c) = min(a,min(b,c)) 5. En \u211d, min(a,b)+c = min(a+c,b+c) A continuaci\u00f3n se muestran las soluciones.<\/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\/8015"}],"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=8015"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8015\/revisions"}],"predecessor-version":[{"id":8016,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8015\/revisions\/8016"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8015"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8015"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8015"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}