Demostrar con Lean4 que si \\(a\\), \\(b\\) y \\(c\\) n\u00fameros reales, entonces
\n\\[\\min(a,b)+c = \\min(a+c,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 a b + c = min (a + c) (b + c) :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraciones en lenguaje natural (LN)<\/b><\/p>\n
\n1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Aplicando la propiedad antisim\u00e9trica a las siguientes desigualdades
\n\\begin{align}
\n \\min(a, b) + c \\leq \\min(a + c, b + c) \\tag{1} \\\\
\n \\min(a + c, b + c) \\leq \\min(a, b) + c \\tag{2}
\n\\end{align}<\/p>\n
Para demostrar (1) basta demostrar que se verifican las siguientes desigualdades
\n\\begin{align}
\n \\min(a, b) + c &\\leq a + c \\tag{1a} \\\\
\n \\min(a, b) + c &\\leq b + c \\tag{1b}
\n\\end{align}
\nque se tienen porque se verifican las siguientes desigualdades
\n\\begin{align}
\n \\min(a, b) &\\leq a \\\\
\n \\min(a, b) &\\leq b
\n\\end{align}<\/p>\n
Para demostrar (2) basta demostrar que se verifica
\n\\[ \\min(a + c, b + c) – c \\leq \\min(a, b) \\]
\nque se demuestra usando (1); en efecto,
\n\\begin{align}
\n \\min(a + c, b + c) – c &\\leq \\min(a + c – c, b + c – c) &&\\text{[por (1)]}\\\\
\n &= \\min(a, b)
\n\\end{align}<\/p>\n
2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Por casos seg\u00fan \\(a \\leq b\\).<\/p>\n
1\u00ba caso: Supongamos que \\(a \\leq b\\). Entonces,
\n\\begin{align}
\n \\min(a, b) + c &= a + c \\\\
\n &= \\min(a + c, b + c)
\n\\end{align}<\/p>\n
2\u00ba caso: Supongamos que \\(a \\nleq b\\). Entonces,
\n\\begin{align}
\n \\min(a, b) + c &= b + c \\\\
\n &= \\min(a + c, b + c)
\n\\end{align}<\/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-- En las demostraciones se usar\u00e1n los siguientes lemas auxiliares\r\n-- aux1 : min a b + c \u2264 min (a + c) (b + c)\r\n-- aux2 : min (a + c) (b + c) \u2264 min a b + c\r\n-- cuyas demostraciones se exponen a continuaci\u00f3n.\r\n\r\n-- 1\u00aa demostraci\u00f3n de aux1\r\nlemma aux1 :\r\n min a b + c \u2264 min (a + c) (b + c) :=\r\nby\r\n have h1 : min a b \u2264 a :=\r\n min_le_left a b\r\n have h2 : min a b + c \u2264 a + c :=\r\n add_le_add_right h1 c\r\n have h3 : min a b \u2264 b :=\r\n min_le_right a b\r\n have h4 : min a b + c \u2264 b + c :=\r\n add_le_add_right h3 c\r\n show min a b + c \u2264 min (a + c) (b + c)\r\n exact le_min h2 h4\r\n\r\n-- 2\u00aa demostraci\u00f3n de aux1\r\nexample :\r\n min a b + c \u2264 min (a + c) (b + c) :=\r\nby\r\n apply le_min\r\n { apply add_le_add_right\r\n exact min_le_left a b }\r\n { apply add_le_add_right\r\n exact min_le_right a b }\r\n\r\n-- 3\u00aa demostraci\u00f3n de aux1\r\nexample :\r\n min a b + c \u2264 min (a + c) (b + c) :=\r\nle_min (add_le_add_right (min_le_left a b) c)\r\n (add_le_add_right (min_le_right a b) c)\r\n\r\n-- 1\u00aa demostraci\u00f3n de aux2\r\nlemma aux2 :\r\n min (a + c) (b + c) \u2264 min a b + c :=\r\nby\r\n have h1 : min (a + c) (b + c) + -c \u2264 min a b\r\n { calc min (a + c) (b + c) + -c\r\n \u2264 min (a + c + -c) (b + c + -c) := aux1\r\n _ = min a b := by ring_nf }\r\n show min (a + c) (b + c) \u2264 min a b + c\r\n exact add_neg_le_iff_le_add.mp h1\r\n\r\n-- 1\u00aa demostraci\u00f3n del ejercicio\r\nexample :\r\n min a b + c = min (a + c) (b + c) :=\r\nby\r\n have h1 : min a b + c \u2264 min (a + c) (b + c) := aux1\r\n have h2 : min (a + c) (b + c) \u2264 min a b + c := aux2\r\n show min a b + c = min (a + c) (b + c)\r\n exact le_antisymm h1 h2\r\n\r\n-- 2\u00aa demostraci\u00f3n del ejercicio\r\nexample :\r\n min a b + c = min (a + c) (b + c) :=\r\nby\r\n apply le_antisymm\r\n { show min a b + c \u2264 min (a + c) (b + c)\r\n exact aux1 }\r\n { show min (a + c) (b + c) \u2264 min a b + c\r\n exact aux2 }\r\n\r\n-- 3\u00aa demostraci\u00f3n del ejercicio\r\nexample :\r\n min a b + c = min (a + c) (b + c) :=\r\nby\r\n apply le_antisymm\r\n { exact aux1 }\r\n { exact aux2 }\r\n\r\n-- 4\u00aa demostraci\u00f3n del ejercicio\r\nexample :\r\n min a b + c = min (a + c) (b + c) :=\r\nle_antisymm aux1 aux2\r\n\r\n-- 5\u00aa demostraci\u00f3n del ejercicio\r\nexample : min a b + c = min (a + c) (b + c) :=\r\nby\r\n by_cases h : a \u2264 b\r\n { have h1 : a + c \u2264 b + c := add_le_add_right h c\r\n calc min a b + c = a + c := by simp [min_eq_left h]\r\n _ = min (a + c) (b + c) := by simp [min_eq_left h1]}\r\n { have h2: b \u2264 a := le_of_not_le h\r\n have h3 : b + c \u2264 a + c := add_le_add_right h2 c\r\n calc min a b + c = b + c := by simp [min_eq_right h2]\r\n _ = min (a + c) (b + c) := by simp [min_eq_right h3]}\r\n\r\n-- 6\u00aa demostraci\u00f3n del ejercicio\r\nexample : min a b + c = min (a + c) (b + c) :=\r\n(min_add_add_right a b c).symm\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