{"id":1736,"date":"2023-10-30T06:00:00","date_gmt":"2023-10-30T04:00:00","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1736"},"modified":"2023-10-23T16:41:12","modified_gmt":"2023-10-23T14:41:12","slug":"30-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/30-oct-23\/","title":{"rendered":"La suma de dos funciones acotadas superiormente tambi\u00e9n lo est\u00e1"},"content":{"rendered":"

Demostrar con Lean4 que la suma de dos funciones acotadas superiormente tambi\u00e9n lo est\u00e1.<\/p>\n

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

\nimport src.Suma_de_cotas_superiores\nvariable {f g : \u211d \u2192 \u211d}\n\n-- (acotadaSup f) afirma que f tiene cota superior.\ndef acotadaSup (f : \u211d \u2192 \u211d) :=\n  \u2203 a, CotaSuperior f a\n\nexample\n  (hf : acotadaSup f)\n  (hg : acotadaSup g)\n  : acotadaSup (f + g) :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n\n
Del ejercicio La suma de una cota superior de f y una cota superior de g es una cota superior de f+g<\/a> usaremos la definici\u00f3n de cota superior (CotaSuperior<\/code>) y el lema sumaCotaSup<\/code>.<\/p>\n
Puesto que \(f\) est\u00e1 acotada superiormente, tiene una cota superior. Sea \(a\) una de dichas cotas. An\u00e1logamentte, puesto que \(g\) est\u00e1 acotada superiormente, tiene una cota superior. Sea \(b\) una de dichas cotas. Por el lema sumaCotaSup, \(a+b\) es una cota superior de \(f+g\). Por consiguiente, \(f+g\) est\u00e1 acotada superiormente.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport src.Suma_de_cotas_superiores\n\nvariable {f g : \u211d \u2192 \u211d}\n\n-- (acotadaSup f) afirma que f tiene cota superior.\ndef acotadaSup (f : \u211d \u2192 \u211d) :=\n  \u2203 a, CotaSuperior f a\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (hf : acotadaSup f)\n  (hg : acotadaSup g)\n  : acotadaSup (f + g) :=\nby\n  cases' hf with a ha\n  -- a : \u211d\n  -- ha : CotaSuperior f a\n  cases' hg with b hb\n  -- b : \u211d\n  -- hb : CotaSuperior g b\n  have h1 : CotaSuperior (f + g) (a + b) :=\n    sumaCotaSup ha hb\n  have h2 : \u2203 z, CotaSuperior (f+g) z :=\n    Exists.intro (a + b) h1\n  show acotadaSup (f + g)\n  exact h2\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (hf : acotadaSup f)\n  (hg : acotadaSup g)\n  : acotadaSup (f + g) :=\nby\n  cases' hf with a ha\n  -- a : \u211d\n  -- ha : FnUb f a\n  cases' hg with b hb\n  -- b : \u211d\n  -- hb : FnUb g b\n  use a + b\n  apply sumaCotaSup ha hb\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (hf : acotadaSup f)\n  (hg : acotadaSup g)\n  : acotadaSup (f + g) :=\nby\n  rcases hf with \u27e8a, ha\u27e9\n  rcases hg with \u27e8b, hb\u27e9\n  exact \u27e8a + b, sumaCotaSup ha hb\u27e9\n\n-- 5\u00aa demostraci\u00f3n\nexample :\n  acotadaSup f \u2192 acotadaSup g \u2192 acotadaSup (f + g) :=\nby\n  rintro \u27e8a, ha\u27e9 \u27e8b, hb\u27e9\n  exact \u27e8a + b, sumaCotaSup ha hb\u27e9\n\n-- 6\u00aa demostraci\u00f3n\nexample :\n  acotadaSup f \u2192 acotadaSup g \u2192 acotadaSup (f + g) :=\nfun \u27e8a, ha\u27e9 \u27e8b, hb\u27e9 \u21a6 \u27e8a + b, sumaCotaSup ha hb\u27e9\n\n-- Lemas usados\n-- ============\n\n-- #check (sumaCotaSup : CotaSuperior f a \u2192 CotaSuperior g b \u2192 CotaSuperior (f + g) (a + b))\n<\/pre>\n
Referencias<\/b><\/p>\n