Demostrar con Lean4, que en \u211d
\n\\[ \\left\\{ 0 < \u03b5, \u03b5 \u2264 1, |x| < \u03b5, |y| < \u03b5 \\right\\} \u22a2 |xy| < \u03b5 \\]\n\nPara ello, completar la siguiente teor\u00eda de Lean4:\n\n\n\n
\r\nimport Mathlib.Data.Real.Basic\r\n\r\nexample :\r\n \u2200 {x y \u03b5 : \u211d}, 0 < \u03b5 \u2192 \u03b5 \u2264 1 \u2192 |x| < \u03b5 \u2192 |y| < \u03b5 \u2192 |x * y| < \u03b5 :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nSe usar\u00e1n los siguientes lemas
\n\\begin{align}
\n &|a\u00b7b| = |a|\u00b7|b| \\tag{L1} \\\\
\n &0\u00b7a = 0 \\tag{L2} \\\\
\n &0 \u2264 |a| \\tag{L3} \\\\
\n &a \u2264 b \u2192 a \u2260 b \u2192 a < b \\tag{L4} \\\\\n &a \u2260 b \u2194 b \u2260 a \\tag{L5} \\\\\n &0 < a \u2192 (ab < ac \u2194 b < c) \\tag{L6} \\\\\n &0 < a \u2192 (ba < ca \u2194 b < c) \\tag{L7} \\\\\n &0 < a \u2192 (ba \u2264 ca \u2194 b \u2264 c) \\tag{L8} \\\\\n &1\u00b7a = a \\tag{L9} \\\\\n\\end{align}\n\nSean \\(x, y, \u03b5 \u2208 \u211d\\) tales que\n\\begin{align}\n 0 &< \u03b5 \\tag{he1} \\\\\n \u03b5 &\u2264 1 \\tag{he2} \\\\\n |x| &< \u03b5 \\tag{hx} \\\\\n |y| &< \u03b5 \\tag{hy}\n\\end{align}\ny tenemos que demostrar que\n\\[ |xy| < \u03b5 \\]\nLo haremos distinguiendo caso seg\u00fan \\(|x| = 0\\).\n\n\n\n
\n1\u00ba caso. Supongamos que
\n\\[ |x| = 0 \\tag{1} \\]
\nEntonces,
\n\\begin{align}
\n |xy| &= |x||y| &&\\text{[por L1]} \\\\
\n &= 0|y| &&\\text{[por h1]} \\\\
\n &= 0 &&\\text{[por L2]} \\\\
\n &< \u03b5 &&\\text{[por he1]}\n\\end{align}\n\n2\u00ba caso. Supongamos que\n\\[ |x| \u2260 0 \\tag{2} \\]\nEntonces, por L4, L3 y L5, se tiene\n\\[ 0 < x \\tag{3} \\]\ny, por tanto,\n\\begin{align}\n |xy| &= |x||y| &&\\text{[por L1]} \\\\\n &< |x|\u03b5 &&\\text{[por L6, (3) y (hy)]} \\\\\n &< \u03b5\u03b5 &&\\text{[por L7, (he1) y (hx)]} \\\\\n &\u2264 1\u03b5 &&\\text{[por L8, (he1) y (he2)]} \\\\\n &= \u03b5 &&\\text{[por L9]}\n\\end{align}\n\nDemostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample :\r\n \u2200 {x y \u03b5 : \u211d}, 0 < \u03b5 \u2192 \u03b5 \u2264 1 \u2192 |x| < \u03b5 \u2192 |y| < \u03b5 \u2192 |x * y| < \u03b5 :=\r\nby\r\n intros x y \u03b5 he1 he2 hx hy\r\n by_cases h : (|x| = 0)\r\n . -- h : |x| = 0\r\n show |x * y| < \u03b5\r\n calc\r\n |x * y|\r\n = |x| * |y| := abs_mul x y\r\n _ = 0 * |y| := by rw [h]\r\n _ = 0 := zero_mul (abs y)\r\n _ < \u03b5 := he1\r\n . -- h : \u00ac|x| = 0\r\n have h1 : 0 < |x| := by\r\n have h2 : 0 \u2264 |x| := abs_nonneg x\r\n show 0 < |x|\r\n exact lt_of_le_of_ne h2 (ne_comm.mpr h)\r\n show |x * y| < \u03b5\r\n calc |x * y|\r\n = |x| * |y| := abs_mul x y\r\n _ < |x| * \u03b5 := (mul_lt_mul_left h1).mpr hy\r\n _ < \u03b5 * \u03b5 := (mul_lt_mul_right he1).mpr hx\r\n _ \u2264 1 * \u03b5 := (mul_le_mul_right he1).mpr he2\r\n _ = \u03b5 := one_mul \u03b5\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample :\r\n \u2200 {x y \u03b5 : \u211d}, 0 < \u03b5 \u2192 \u03b5 \u2264 1 \u2192 |x| < \u03b5 \u2192 |y| < \u03b5 \u2192 |x * y| < \u03b5 :=\r\nby\r\n intros x y \u03b5 he1 he2 hx hy\r\n by_cases (|x| = 0)\r\n . -- h : |x| = 0\r\n show |x * y| < \u03b5\r\n calc\r\n |x * y| = |x| * |y| := by apply abs_mul\r\n _ = 0 * |y| := by rw [h]\r\n _ = 0 := by apply zero_mul\r\n _ < \u03b5 := by apply he1\r\n . -- h : \u00ac|x| = 0\r\n have h1 : 0 < |x| := by\r\n have h2 : 0 \u2264 |x| := by apply abs_nonneg\r\n exact lt_of_le_of_ne h2 (ne_comm.mpr h)\r\n show |x * y| < \u03b5\r\n calc\r\n |x * y| = |x| * |y| := by rw [abs_mul]\r\n _ < |x| * \u03b5 := by apply (mul_lt_mul_left h1).mpr hy\r\n _ < \u03b5 * \u03b5 := by apply (mul_lt_mul_right he1).mpr hx\r\n _ \u2264 1 * \u03b5 := by apply (mul_le_mul_right he1).mpr he2\r\n _ = \u03b5 := by rw [one_mul]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample :\r\n \u2200 {x y \u03b5 : \u211d}, 0 < \u03b5 \u2192 \u03b5 \u2264 1 \u2192 |x| < \u03b5 \u2192 |y| < \u03b5 \u2192 |x * y| < \u03b5 :=\r\nby\r\n intros x y \u03b5 he1 he2 hx hy\r\n by_cases (|x| = 0)\r\n . -- h : |x| = 0\r\n show |x * y| < \u03b5\r\n calc |x * y| = |x| * |y| := by simp only [abs_mul]\r\n _ = 0 * |y| := by simp only [h]\r\n _ = 0 := by simp only [zero_mul]\r\n _ < \u03b5 := by simp only [he1]\r\n . -- h : \u00ac|x| = 0\r\n have h1 : 0 < |x| := by\r\n have h2 : 0 \u2264 |x| := by simp only [abs_nonneg]\r\n exact lt_of_le_of_ne h2 (ne_comm.mpr h)\r\n show |x * y| < \u03b5\r\n calc\r\n |x * y| = |x| * |y| := by simp [abs_mul]\r\n _ < |x| * \u03b5 := by simp only [mul_lt_mul_left, h1, hy]\r\n _ < \u03b5 * \u03b5 := by simp only [mul_lt_mul_right, he1, hx]\r\n _ \u2264 1 * \u03b5 := by simp only [mul_le_mul_right, he1, he2]\r\n _ = \u03b5 := by simp only [one_mul]\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- variable (a b c : \u211d)\r\n-- #check (abs_mul a b : |a * b| = |a| * |b|)\r\n-- #check (abs_nonneg a : 0 \u2264 |a|)\r\n-- #check (lt_of_le_of_ne : a \u2264 b \u2192 a \u2260 b \u2192 a < b)\r\n-- #check (mul_le_mul_right : 0 < a \u2192 (b * a \u2264 c * a \u2194 b \u2264 c))\r\n-- #check (mul_lt_mul_left : 0 < a \u2192 (a * b < a * c \u2194 b < c))\r\n-- #check (mul_lt_mul_right : 0 < a \u2192 (b * a < c * a \u2194 b < c))\r\n-- #check (ne_comm : a \u2260 b \u2194 b \u2260 a)\r\n-- #check (one_mul a : 1 * a = a)\r\n-- #check (zero_mul a : 0 * a = 0)\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n