{"id":1777,"date":"2023-11-17T06:00:45","date_gmt":"2023-11-17T04:00:45","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1777"},"modified":"2023-11-06T12:34:29","modified_gmt":"2023-11-06T10:34:29","slug":"17-nov-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/17-nov-23\/","title":{"rendered":"Si para cada a existe un x tal que f(x) < a, entonces f no tiene cota inferior"},"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 inferior.<\/p>\n

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

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

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