{"id":1632,"date":"2023-10-04T06:00:59","date_gmt":"2023-10-04T04:00:59","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1632"},"modified":"2023-09-13T18:27:19","modified_gmt":"2023-09-13T16:27:19","slug":"04-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/04-oct-23\/","title":{"rendered":"La suma de una cota superior de f y una cota superior de g es una cota superior 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 superior de \\(f\\) y una cota superior de \\(g\\) es una cota superior 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-- (CotaSuperior f a) se verifica si a es una cota superior de f.\r\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\r\n  \u2200 x, f x \u2264 a\r\n\r\nvariable (f g : \u211d \u2192 \u211d)\r\nvariable (a b : \u211d)\r\n\r\nexample\r\n  (hfa : CotaSuperior f a)\r\n  (hgb : CotaSuperior g b)\r\n  : CotaSuperior (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, c \u2264 d\\} \\vdash a + c \u2264 b + d \\tag{L1} \\]<\/p>\n
Por la definici\u00f3n de cota superior, hay que demostrar que
\n\\[ (\u2200 x \u2208 \u211d) [f(x) + g(x) \u2264 a + b] \\tag{1} \\]
\nPara ello, sea \\(x \u2208 R\\). Puesto que \\(a\\) es una cota superior de \\(f\\), se tiene que
\n\\[ f(x) \u2264 a \\tag{2} \\]
\ny, puesto que \\(b\\) es una cota superior de \\(g\\), se tiene que
\n\\[ g(x) \u2264 b \\tag{3} \\]
\nDe (2) y (3), por L1, se tiene que
\n\\[ f(x) + g(x) \u2264 a + b \\]
\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-- (CotaSuperior f a) se verifica si a es una cota superior de f.\r\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\r\n  \u2200 x, f x \u2264 a\r\n\r\nvariable (f g : \u211d \u2192 \u211d)\r\nvariable (a b : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (hfa : CotaSuperior f a)\r\n  (hgb : CotaSuperior g b)\r\n  : CotaSuperior (f + g) (a + b) :=\r\nby\r\n  have h1 : \u2200 x, (f + g) x  \u2264 a + b := by\r\n  { intro x\r\n    have h2 : f x \u2264 a := hfa x\r\n    have h3 : g x \u2264 b := hgb x\r\n    show (f + g) x \u2264 a + b\r\n    exact add_le_add h2 h3 }\r\n  show CotaSuperior (f + g) (a + b)\r\n  exact h1\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (hfa : CotaSuperior f a)\r\n  (hgb : CotaSuperior g b)\r\n  : CotaSuperior (f + g) (a + b) :=\r\nby\r\n  have h1 : \u2200 x, (f + g) x \u2264 a + b := by\r\n  { intro x\r\n    show (f + g) x \u2264 a + b\r\n    exact add_le_add (hfa x) (hgb x) }\r\n  show CotaSuperior (f + g) (a + b)\r\n  exact h1\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (hfa : CotaSuperior f a)\r\n  (hgb : CotaSuperior g b)\r\n  : CotaSuperior (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\n-- ===============\r\n\r\nexample\r\n  (hfa : CotaSuperior f a)\r\n  (hgb : CotaSuperior g b)\r\n  : CotaSuperior (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