{"id":1745,"date":"2023-11-01T06:00:26","date_gmt":"2023-11-01T04:00:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1745"},"modified":"2023-10-26T11:26:42","modified_gmt":"2023-10-26T09:26:42","slug":"01-nov-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/01-nov-23\/","title":{"rendered":"Si a es una cota superior de f y c \u2265 0, entonces ca es una cota superior de cf"},"content":{"rendered":"

Demostrar con Lean4 que si \(a\) es una cota superior de \(f\) y \(c \u2265 0\), entonces \(ca\) es una cota superior de \(cf\).<\/p>\n

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

\nimport Mathlib.Data.Real.Basic\n\n-- (CotaSuperior f a) se verifica si a es una cota superior de f.\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, f x \u2264 a\n\nvariable {f : \u211d \u2192 \u211d}\nvariable {c : \u211d}\n\nexample\n  (hfa : CotaSuperior f a)\n  (h : c \u2265 0)\n  : CotaSuperior (fun x \u21a6 c * f x) (c * a) :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nSe usar\u00e1 el lema
\n\[ \{b \u2264 c, 0 \u2264 a\} \u22a2 ab \u2264 ac \tag{L1} \]<\/p>\n
Tenemos que demostrar que
\n\[ (\u2200 y \u2208 \u211d) cf(y) \u2264 ca \]
\nSea \(y \u2208 R\). Puesto que \(a\) es una cota de \(f\), se tiene que
\n\[ f(y) \u2264 a \]
\nque, junto con \(c \u2265 0\), por el lema L1 nos da
\n\[ cf(y) \u2264 ca \]<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Data.Real.Basic\n\n-- (CotaSuperior f a) se verifica si a es una cota superior de f.\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, f x \u2264 a\n\nvariable {f : \u211d \u2192 \u211d}\nvariable {c : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (hfa : CotaSuperior f a)\n  (h : c \u2265 0)\n  : CotaSuperior (fun x \u21a6 c * f x) (c * a) :=\nby\n  intro y\n  -- y : \u211d\n  -- \u22a2 (fun x => c * f x) y \u2264 c * a\n  have ha : f y \u2264 a := hfa y\n  calc (fun x => c * f x) y\n       = c * f y := by rfl\n     _ \u2264 c * a   := mul_le_mul_of_nonneg_left ha h\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (hfa : CotaSuperior f a)\n  (h : c \u2265 0)\n  : CotaSuperior (fun x \u21a6 c * f x) (c * a) :=\nby\n  intro y\n  calc (fun x => c * f x) y\n       = c * f y := by rfl\n     _ \u2264 c * a   := mul_le_mul_of_nonneg_left (hfa y) h\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (hfa : CotaSuperior f a)\n  (h : c \u2265 0)\n  : CotaSuperior (fun x \u21a6 c * f x) (c * a) :=\nby\n  intro y\n  show (fun x => c * f x) y \u2264 c * a\n  exact mul_le_mul_of_nonneg_left (hfa y) h\n\n-- 4\u00aa demostraci\u00f3n\nlemma CotaSuperior_mul\n  (hfa : CotaSuperior f a)\n  (h : c \u2265 0)\n  : CotaSuperior (fun x \u21a6 c * f x) (c * a) :=\nfun y \u21a6 mul_le_mul_of_nonneg_left (hfa y) h\n\n-- Lemas usados\n-- ============\n\n-- variable (c : \u211d)\n-- #check (mul_le_mul_of_nonneg_left : b \u2264 c \u2192 0 \u2264 a \u2192 a * b \u2264 a * c)\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