{"id":1747,"date":"2023-11-02T06:00:57","date_gmt":"2023-11-02T04:00:57","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1747"},"modified":"2023-10-26T12:15:31","modified_gmt":"2023-10-26T10:15:31","slug":"02-nov-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/02-nov-23\/","title":{"rendered":"Si c \u2265 0 y f est\u00e1 acotada superiormente, entonces c\u00b7f tambi\u00e9n lo est\u00e1"},"content":{"rendered":"

Demostrar con Lean4 que si \(c \u2265 0\) y \(f\) est\u00e1 acotada superiormente, entonces \(c\u00b7f\) tambi\u00e9n lo est\u00e1.<\/p>\n

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

\nimport src.Cota_superior_de_producto_por_escalar\n\nvariable {f : \u211d \u2192 \u211d}\nvariable {c : \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  (hc : c \u2265 0)\n  : acotadaSup (fun x \u21a6 c * f x) :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nUsaremos el siguiente lema:
\n\begin{align}
\n\u00ab\text{Si } a \text{ es cota superior de } f \text{ y } c \u2265 0\text{, entonces } c\u00b7a \text{ es cota superior de } c\u00b7f\u00bb
\n\end{align}<\/p>\n
Puesto que \(f\) est\u00e1 acotada superiormente, tiene una cota superior. Sea \(a\) una de dichas cotas. Entonces, por el lema, \(c\u00b7a\) es una cota superior de \(c\u00b7f\). Por consiguiente, \(c\u00b7f\) est\u00e1 acotada superiormente.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport src.Cota_superior_de_producto_por_escalar\n\nvariable {f : \u211d \u2192 \u211d}\nvariable {c : \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  (hc : c \u2265 0)\n  : acotadaSup (fun x \u21a6 c * f x) :=\nby\n  cases' hf with a ha\n  -- a : \u211d\n  -- ha : CotaSuperior f a\n  have h1 : CotaSuperior (fun x \u21a6 c * f x) (c * a) :=\n    CotaSuperior_mul ha hc\n  have h2 : \u2203 z, \u2200 x, (fun x \u21a6 c * f x) x \u2264 z :=\n    Exists.intro (c * a) h1\n  show acotadaSup (fun x \u21a6 c * f x)\n  exact h2\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (hf : acotadaSup f)\n  (hc : c \u2265 0)\n  : acotadaSup (fun x \u21a6 c * f x) :=\nby\n  cases' hf with a ha\n  -- a : \u211d\n  -- ha : CotaSuperior f a\n  use c * a\n  -- \u22a2 CotaSuperior (fun x => c * f x) (c * a)\n  apply CotaSuperior_mul ha hc\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (hf : acotadaSup f)\n  (hc : c \u2265 0)\n  : acotadaSup (fun x \u21a6 c * f x) :=\nby\n  rcases hf with \u27e8a, ha\u27e9\n  -- a : \u211d\n  -- ha : CotaSuperior f a\n  exact \u27e8c * a, CotaSuperior_mul ha hc\u27e9\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (hc : c \u2265 0)\n  : acotadaSup f \u2192 acotadaSup (fun x \u21a6 c * f x) :=\nby\n  rintro \u27e8a, ha\u27e9\n  -- a : \u211d\n  -- ha : CotaSuperior f a\n  exact \u27e8c * a, CotaSuperior_mul ha hc\u27e9\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (hc : c \u2265 0)\n  : acotadaSup f \u2192 acotadaSup (fun x \u21a6 c * f x) :=\nfun \u27e8a, ha\u27e9 \u21a6 \u27e8c * a, CotaSuperior_mul ha hc\u27e9\n\n-- Lemas usados\n-- ============\n\n-- #check (CotaSuperior_mul : CotaSuperior f a \u2192 c \u2265 0 \u2192 CotaSuperior (fun x \u21a6 c * f x) (c * a))\n<\/pre>\n
Referencias<\/b><\/p>\n