Demostrar con Lean4 que si \\(a\\) y \\(b\\) n\u00fameros reales, entonces \\(\\min(a, b) = \\min(b, a)\\).<\/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 : \u211d)\r\n\r\nexample : min a b = min b a :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b>
\n<\/p>\n
Es consecuencia de la siguiente propiedad
\n\\[\\min(a, b) \\leq \\min(b, a) \\tag{1}\\]
\nEn efecto, intercambiando las variables en (1) se obtiene
\n\\[\\min(b, a) \\leq \\min(a, b) \\tag{2}\\]
\nFinalmente de (1) y (2) se obtiene
\n\\[\\min(b, a) = \\min(a, b)\\]<\/p>\n
Para demostrar (1), se observa que
\n\\begin{align}
\n \\min(a, b) &\\leq b \\\\
\n \\min(a, b) &\\leq a
\n\\end{align}
\ny, por tanto,
\n\\[\\min(a, b) \\leq \\min(b, a)\\]<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\n\r\nvariable (a b : \u211d)\r\n\r\n-- Lema auxiliar\r\n-- =============\r\n\r\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\r\n-- =================================\r\n\r\nexample : min a b \u2264 min b a :=\r\nby\r\n have h1 : min a b \u2264 b := min_le_right a b\r\n have h2 : min a b \u2264 a := min_le_left a b\r\n show min a b \u2264 min b a\r\n exact le_min h1 h2\r\n\r\n-- 2\u00aa demostraci\u00f3n del lema auxiliar\r\n-- =================================\r\n\r\nexample : min a b \u2264 min b a :=\r\nby\r\n apply le_min\r\n { apply min_le_right }\r\n { apply min_le_left }\r\n\r\n-- 3\u00aa demostraci\u00f3n del lema auxiliar\r\n-- =================================\r\n\r\nlemma aux : min a b \u2264 min b a :=\r\nby exact le_min (min_le_right a b) (min_le_left a b)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : min a b = min b a :=\r\nby\r\n apply le_antisymm\r\n { exact aux a b}\r\n { exact aux b a}\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : min a b = min b a :=\r\nle_antisymm (aux a b) (aux b a)\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : min a b = min b a :=\r\nmin_comm a b\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