{"id":1806,"date":"2023-11-24T06:00:50","date_gmt":"2023-11-24T04:00:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1806"},"modified":"2023-11-13T11:51:09","modified_gmt":"2023-11-13T09:51:09","slug":"24-nov-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/24-nov-23\/","title":{"rendered":"Si (\u2200\u03b5 > 0)[x \u2264 \u03b5], entonces x \u2264 0"},"content":{"rendered":"\n

Demostrar con Lean4 que si \((\u2200\u03b5 > 0)[x \u2264 \u03b5]\), entonces \(x \u2264 0\).<\/p>\n

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

\nimport Mathlib.Data.Real.Basic\nvariable (x : \u211d)\n\nexample\n  (h : \u2200 \u03b5 > 0, x \u2264 \u03b5)\n  : x \u2264 0 :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Basta demostrar que \(x \u226f 0\). Para ello, supongamos que \(x > 0\) y vamos a demostrar que
\n\[ \u00ac(\u2200\u03b5)[\u03b5 > 0 \u2192 x \u2264 \u03b5] \tag{1} \]
\nque es una contradicci\u00f3n con la hip\u00f3tesis. Interiorizando la negaci\u00f3n, (1) es equivalente a
\n\[ (\u2203\u03b5)[\u03b5 > 0 \u2227 \u03b5 < x] \tag{2} \]
\nPara demostrar (2), elegimos \(\u03b5 = \dfrac{x}{2}\) ya que, como \(x > 0\), se tiene
\n\[ 0 < \dfrac{x}{2} < x\]<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Data.Real.Basic\n\nvariable (x : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 \u03b5 > 0, x \u2264 \u03b5)\n  : x \u2264 0 :=\nby\n  apply le_of_not_gt\n  -- \u22a2 \u00acx > 0\n  intro hx0\n  -- hx0 : x > 0\n  -- \u22a2 False\n  apply absurd h\n  -- \u22a2 \u00ac\u2200 (\u03b5 : \u211d), \u03b5 > 0 \u2192 x \u2264 \u03b5\n  push_neg\n  -- \u22a2 \u2203 \u03b5, \u03b5 > 0 \u2227 \u03b5 < x\n  use x \/2\n  -- \u22a2 x \/ 2 > 0 \u2227 x \/ 2 < x\n  constructor\n  { show x \/ 2 > 0\n    exact half_pos hx0 }\n  { show x \/ 2 < x\n    exact half_lt_self hx0 }\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (x : \u211d)\n  (h : \u2200 \u03b5 > 0, x \u2264 \u03b5)\n  : x \u2264 0 :=\nby\n  contrapose! h\n  -- \u22a2 \u2203 \u03b5, \u03b5 > 0 \u2227 \u03b5 < x\n  use x \/ 2\n  -- \u22a2 x \/ 2 > 0 \u2227 x \/ 2 < x\n  constructor\n  { show x \/ 2 > 0\n    exact half_pos h }\n  { show x \/ 2 < x\n    exact half_lt_self h }\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- variable (p q : Prop)\n-- #check (le_of_not_gt : \u00aca > b \u2192 a \u2264 b)\n-- #check (half_lt_self : 0 < a \u2192 a \/ 2 < a)\n-- #check (half_pos : 0 < a \u2192 0 < a \/ 2)\n-- #check (absurd : p \u2192 \u00acp \u2192 q)\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