{"id":1774,"date":"2023-11-16T06:00:12","date_gmt":"2023-11-16T04:00:12","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1774"},"modified":"2023-11-07T19:30:33","modified_gmt":"2023-11-07T17:30:33","slug":"16-nov-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/16-nov-23\/","title":{"rendered":"Si para cada a existe un x tal que f(x) > a, entonces f no tiene cota superior"},"content":{"rendered":"

Demostrar con Lean4 que si \(f\) es una funci\u00f3n de \(\u211d\) en \(\u211d\) tal que para cada \(a\) existe un \(x\) tal que \(f(x) > a\), entonces \(f\) no tiene cota superior.<\/p>\n

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

\nimport Mathlib.Data.Real.Basic\n\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, f x \u2264 a\n\ndef acotadaSup (f : \u211d \u2192 \u211d) : Prop :=\n  \u2203 a, CotaSuperior f a\n\nvariable (f : \u211d \u2192 \u211d)\n\nexample\n  (h : \u2200 a, \u2203 x, f x > a)\n  : \u00ac acotadaSup f :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nSupongamos que \(f\) tiene cota superior. Sea \(b\) una de dichas cotas superiores. Por la hip\u00f3tesis, existe un \(x\) tal que \(f(x) > b\). Adem\u00e1s, como \(b\) es una cota superior de \(f\), \(f(x) \u2264 b\) que contradice la desigualdad anterior.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Data.Real.Basic\n\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, f x \u2264 a\n\ndef acotadaSup (f : \u211d \u2192 \u211d) : Prop :=\n  \u2203 a, CotaSuperior f a\n\nvariable (f : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 a, \u2203 x, f x > a)\n  : \u00ac acotadaSup f :=\nby\n  intros hf\n  -- hf : acotadaSup f\n  -- \u22a2 False\n  cases' hf with b hb\n  -- b : \u211d\n  -- hb : CotaSuperior f b\n  cases' h b with x hx\n  -- x : \u211d\n  -- hx : f x > b\n  have : f x \u2264 b := hb x\n  linarith\n\n-- 2\u00aa demostraci\u00f3n\ntheorem sinCotaSup\n  (h : \u2200 a, \u2203 x, f x > a)\n  : \u00ac acotadaSup f :=\nby\n  intros hf\n  -- hf : acotadaSup f\n  -- \u22a2 False\n  rcases hf with \u27e8b, hb : CotaSuperior f b\u27e9\n  rcases h b with \u27e8x, hx : f x > b\u27e9\n  have : f x \u2264 b := hb x\n  linarith\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