{"id":1637,"date":"2023-10-05T06:00:13","date_gmt":"2023-10-05T04:00:13","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1637"},"modified":"2023-09-16T18:48:13","modified_gmt":"2023-09-16T16:48:13","slug":"05-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/05-oct-23\/","title":{"rendered":"La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g"},"content":{"rendered":"

Demostrar con Lean4 que si \\(f\\) y \\(g\\) son funciones de \\(\u211d\\) en \\(\u211d\\), entonces la suma de una cota inferior de \\(f\\) y una cota inferior de \\(g\\) es una cota inferior de \\(f+g\\).<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\r\nimport Mathlib.Data.Real.Basic\r\n\r\n-- (CotaInferior f a) expresa que a es una cota inferior de f.\r\ndef CotaInferior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\r\n  \u2200 x, a \u2264 f x\r\n\r\nvariable (f g : \u211d \u2192 \u211d)\r\nvariable (a b : \u211d)\r\n\r\nexample\r\n  (hfa : CotaInferior f a)\r\n  (hgb : CotaInferior g b)\r\n  : CotaInferior (f + g) (a + b) :=\r\nby sorry\r\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nSe usar\u00e1 el siguiente lema
\n\\[ a \u2264 b \u2192 c \u2264 d \u2192 a + c \u2264 b + d \\tag{L1} \\]<\/p>\n
Por la definici\u00f3n de cota inferior, hay que demostrar que
\n\\[ (\u2200 x \u2208 \u211d) [a + b \u2264 f(x) + g(x)] \\tag{1} \\]
\nPara ello, sea \\(x \u2208 R\\). Puesto que es \\(a\\) es una cota inferior de \\(f\\), se tiene que
\n\\[ a \u2264 f(x) \\tag{2} \\]
\ny, puesto que \\(b\\) es una cota inferior de \\(g\\), se tiene que
\n\\[ b \u2264 g(x) \\tag{3} \\]
\nDe (2) y (3), por L1, se tiene que
\n\\[ a + b \u2264 f(x) + g(x) \\]
\nque es lo que hab\u00eda que demostrar.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\n\r\n-- (CotaInferior f a) expresa que a es una cota inferior de f.\r\ndef CotaInferior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\r\n  \u2200 x, a \u2264 f x\r\n\r\nvariable (f g : \u211d \u2192 \u211d)\r\nvariable (a b : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  (hfa : CotaInferior f a)\r\n  (hgb : CotaInferior g b)\r\n  : CotaInferior (f + g) (a + b) :=\r\nby\r\n  have h1 : \u2200 x, a + b \u2264 f x + g x\r\n  { intro x\r\n    have h1a : a \u2264 f x := hfa x\r\n    have h1b : b \u2264 g x := hgb x\r\n    show a + b \u2264 f x + g x\r\n    exact add_le_add h1a h1b }\r\n  show CotaInferior (f + g) (a + b)\r\n  exact h1\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (hfa : CotaInferior f a)\r\n  (hgb : CotaInferior g b)\r\n  : CotaInferior (f + g) (a + b) :=\r\nby\r\n  have h1 : \u2200 x, a + b \u2264 f x + g x\r\n  { intro x\r\n    show a + b \u2264 f x + g x\r\n    exact add_le_add (hfa x) (hgb x) }\r\n  show CotaInferior (f + g) (a + b)\r\n  exact h1\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n  (hfa : CotaInferior f a)\r\n  (hgb : CotaInferior g b)\r\n  : CotaInferior (f + g) (a + b) :=\r\nby\r\n  intro x\r\n  dsimp\r\n  apply add_le_add\r\n  . apply hfa\r\n  . apply hgb\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n  (hfa : CotaInferior f a)\r\n  (hgb : CotaInferior g b)\r\n  : CotaInferior (f + g) (a + b) :=\r\n\u03bb x \u21a6 add_le_add (hfa x) (hgb x)\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- variable (c d : \u211d)\r\n-- #check (add_le_add : a \u2264 b \u2192 c \u2264 d \u2192 a + c \u2264 b + d)\r\n<\/pre>\n
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n