Demostrar con Lean4 que \\(a\\), \\(b\\) y \\(c\\) n\u00fameros reales, entonces \\(\\min(\\min(a, b), c) = \\min(a, \\min(b, c))\\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\n\r\nvariable {a b c : \u211d}\r\n\r\nexample :\r\n min (min a b) c = min a (min b c) :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nPor la propiedad antisim\u00e9trica, la igualdad es consecuencia de las siguientes desigualdades
\n\\begin{align}
\n \\min(\\min(a, b), c) &\\leq \\min(a, \\min(b, c)) \\tag{1} \\\\
\n \\min(a, \\min(b, c)) &\\leq \\min(\\min(a, b), c) \\tag{2}
\n\\end{align}<\/p>\n
La (1) es consecuencia de las siguientes desigualdades
\n\\begin{align}
\n \\min(\\min(a, b), c) &\\leq a \\tag{1a} \\\\
\n \\min(\\min(a, b), c) &\\leq b \\tag{1b} \\\\
\n \\min(\\min(a, b), c) &\\leq c \\tag{1c}
\n\\end{align}
\nEn efecto, de (1b) y (1c) se obtiene
\n\\[ \\min(\\min(a, b), c) \\leq \\min(b,c) \\]
\nque, junto con (1a) da (1).<\/p>\n
La (2) es consecuencia de las siguientes desigualdades
\n\\begin{align}
\n \\min(a, \\min(b, c)) &\\leq a \\tag{2a} \\\\
\n \\min(a, \\min(b, c)) &\\leq b \\tag{2b} \\\\
\n \\min(a, \\min(b, c)) &\\leq c \\tag{2c}
\n\\end{align}
\nEn efecto, de (2a) y (2b) se obtiene
\n\\[ \\min(a, \\min(b, c)) \\leq \\min(a, b) \\]
\nque, junto con (2c) da (2).<\/p>\n
La demostraci\u00f3n de (1a) es
\n\\[ \\min(\\min(a, b), c) \\leq \\min(a, b) \\leq a \\]
\nLa demostraci\u00f3n de (1b) es
\n\\[ \\min(\\min(a, b), c) \\leq \\min(a, b) \\leq b \\]
\nLa demostraci\u00f3n de (2b) es
\n\\[ \\min(a, \\min(b, c)) \\leq \\min(b, c) \\leq b \\]
\nLa demostraci\u00f3n de (2c) es
\n\\[ \\min(a, \\min(b, c)) \\leq \\min(b, c) \\leq c \\]
\nLa (1c) y (2a) son inmediatas.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\n\r\nvariable {a b c : \u211d}\r\n\r\n-- Lemas auxiliares\r\n-- ================\r\n\r\nlemma aux1a : min (min a b) c \u2264 a :=\r\ncalc min (min a b) c\r\n \u2264 min a b := by exact min_le_left (min a b) c\r\n _ \u2264 a := min_le_left a b\r\n\r\nlemma aux1b : min (min a b) c \u2264 b :=\r\ncalc min (min a b) c\r\n \u2264 min a b := by exact min_le_left (min a b) c\r\n _ \u2264 b := min_le_right a b\r\n\r\nlemma aux1c : min (min a b) c \u2264 c :=\r\nby exact min_le_right (min a b) c\r\n\r\n-- 1\u00aa demostraci\u00f3n del lema aux1\r\nlemma aux1 : min (min a b) c \u2264 min a (min b c) :=\r\nby\r\n apply le_min\r\n { show min (min a b) c \u2264 a\r\n exact aux1a }\r\n { show min (min a b) c \u2264 min b c\r\n apply le_min\r\n { show min (min a b) c \u2264 b\r\n exact aux1b }\r\n { show min (min a b) c \u2264 c\r\n exact aux1c }}\r\n\r\n-- 2\u00aa demostraci\u00f3n del lema aux1\r\nlemma aux1' : min (min a b) c \u2264 min a (min b c) :=\r\nle_min aux1a (le_min aux1b aux1c)\r\n\r\nlemma aux2a : min a (min b c) \u2264 a :=\r\nby exact min_le_left a (min b c)\r\n\r\nlemma aux2b : min a (min b c) \u2264 b :=\r\ncalc min a (min b c)\r\n \u2264 min b c := by exact min_le_right a (min b c)\r\n _ \u2264 b := min_le_left b c\r\n\r\nlemma aux2c : min a (min b c) \u2264 c :=\r\ncalc min a (min b c)\r\n \u2264 min b c := by exact min_le_right a (min b c)\r\n _ \u2264 c := min_le_right b c\r\n\r\n-- 1\u00aa demostraci\u00f3n del lema aux2\r\nlemma aux2 : min a (min b c) \u2264 min (min a b) c :=\r\nby\r\n apply le_min\r\n { show min a (min b c) \u2264 min a b\r\n apply le_min\r\n { show min a (min b c) \u2264 a\r\n exact aux2a }\r\n { show min a (min b c) \u2264 b\r\n exact aux2b }}\r\n { show min a (min b c) \u2264 c\r\n exact aux2c }\r\n\r\n-- 2\u00aa demostraci\u00f3n del lema aux2\r\nlemma aux2' : min a (min b c) \u2264 min (min a b) c :=\r\nle_min (le_min aux2a aux2b) aux2c\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample :\r\n min (min a b) c = min a (min b c) :=\r\nby\r\n apply le_antisymm\r\n { show min (min a b) c \u2264 min a (min b c)\r\n exact aux1 }\r\n { show min a (min b c) \u2264 min (min a b) c\r\n exact aux2 }\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : min (min a b) c = min a (min b c) :=\r\nby\r\n apply le_antisymm\r\n { exact aux1 }\r\n { exact aux2 }\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : min (min a b) c = min a (min b c) :=\r\nle_antisymm aux1 aux2\r\n\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : min (min a b) c = min a (min b c) :=\r\nmin_assoc a b c\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n