{"id":1112,"date":"2022-10-03T06:00:21","date_gmt":"2022-10-03T04:00:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1112"},"modified":"2022-09-16T16:51:19","modified_gmt":"2022-09-16T14:51:19","slug":"si-a-b-c-%e2%88%88-%e2%84%9d-entonces-minminabc-minaminbc","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/si-a-b-c-%e2%88%88-%e2%84%9d-entonces-minminabc-minaminbc\/","title":{"rendered":"Si a, b, c \u2208 \u211d, entonces min(min(a,b),c) = min(a,min(b,c))"},"content":{"rendered":"

Sean a, b y c n\u00fameros reales. Demostrar que<\/p>\n

\n   min (min a b) c = min a (min b c)\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.real.basic tactic\nvariables a b c : \u211d\n\nexample :\n  min (min a b) c = min a (min b c) :=\nsorry\n<\/pre>\n
<\/p>\n
Soluciones con Lean<\/b><\/p>\n
\nimport data.real.basic tactic\n\nvariables a b c : \u211d\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\n-- Se usar\u00e1 el siguiente lema auxilar.\nlemma aux1 : min (min a b) c \u2264 min a (min b c) :=\nbegin\n  apply le_min,\n  { show min (min a b) c \u2264 a,\n      calc min (min a b) c\n           \u2264 min a b : min_le_left (min a b) c\n       ... \u2264 a       : min_le_left a b },\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        calc min (min a b) c\n             \u2264 min a b  : min_le_left (min a b) c\n         ... \u2264 b        : min_le_right a b },\n    { show min (min a b) c \u2264 c,\n      { by exact min_le_right (min a b) c }}},\nend\n\nexample :\n  min (min a b) c = min a (min b c) :=\nbegin\n  apply le_antisymm,\n  { show min (min a b) c \u2264 min a (min b c),\n      by exact aux1 a b c },\n  { show min a (min b c) \u2264 min (min a b) c,\n      calc min a (min b c)\n           = min (min b c) a : by apply min_comm\n       ... = min (min c b) a : by {congr' 1, apply min_comm}\n       ... \u2264 min c (min b a) : by apply aux1\n       ... = min c (min a b) : by {congr' 1, apply min_comm}\n       ... = min (min a b) c : by apply min_comm },\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\n-- Se usar\u00e1 el siguiente lema auxilar.\nlemma aux2 : min (min a b) c \u2264 min a (min b c) :=\nbegin\n  apply le_min,\n  { calc min (min a b) c\n         \u2264 min a b : by simp [min_le_left]\n     ... \u2264 a       : by simp [min_le_left] },\n  { apply le_min,\n    { calc min (min a b) c\n           \u2264 min a b  : by simp [min_le_left]\n       ... \u2264 b        : by simp [min_le_right] },\n    { simp [min_le_right] }},\nend\n\nexample : min (min a b) c = min a (min b c) :=\nbegin\n  apply le_antisymm,\n  { by exact aux2 a b c },\n  { calc min a (min b c)\n         = min (min b c) a : by simp [min_comm]\n     ... = min (min c b) a : by simp [min_comm]\n     ... \u2264 min c (min b a) : by simp [aux2]\n     ... = min c (min a b) : by simp [min_comm]\n     ... = min (min a b) c : by simp [min_comm] },\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : min (min a b) c = min a (min b c) :=\nbegin\n  apply le_antisymm,\n  { by exact aux2 a b c },\n  { calc min a (min b c)\n         = min (min c b) a : by simp [min_comm]\n     ... \u2264 min c (min b a) : by simp [aux2]\n     ... = min (min a b) c : by simp [min_comm] },\nend\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
Referencias<\/b><\/p>\n