Demostrar con Lean4 que en los espacios m\u00e9tricos, \\(d(x,y) \u2265 0\\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Topology.MetricSpace.Basic\r\nvariable {X : Type _} [MetricSpace X]\r\nvariable (x y : X)\r\n\r\nexample : 0 \u2264 d x y :=\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 &0 \u2264 ab \u2192 0 < b \u2192 0 \u2264 a \\tag{L1} \\\\\n &d(x,x) = 0 \\tag{L2} \\\\\n &d(x,z) \u2264 d(x,y) + d(y,z) \\tag{L3} \\\\\n &d(x,y) = d(y,x) \\tag{L4} \\\\\n &2a = a + a \\tag{L5} \\\\\n &0 < 2 \\tag{L6} \\\\\n\\end{align}\n\nPor L1 es suficiente demostrar las siguientes desigualdades:\n\\begin{align}\n 0 &\u2264 2d(x,y) \\tag{1} \\\\\n 0 &< 2 \\tag{2}\n\\end{align}\n\nLa (1) se demuestra por las siguiente cadena de desigualdades:\n\\begin{align}\n 0 &= d(x,x) &&\\text{[por L2]} \\\\\n &\u2264 d(x,y) + d(y,x) &&\\text{[por L3]} \\\\\n &= d(x,y) + d(x,y) &&\\text{[por L4]} \\\\\n &= 2 d(x,y) &&\\text{[por L5]}\n\\end{align}\n\nLa (2) se tiene por L6. \n \n\n\n
\nDemostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Topology.MetricSpace.Basic\r\nvariable {X : Type _} [MetricSpace X]\r\nvariable (x y : X)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : 0 \u2264 dist x y :=\r\nby\r\n have h1 : 0 \u2264 dist x y * 2 := calc\r\n 0 = dist x x := (dist_self x).symm\r\n _ \u2264 dist x y + dist y x := dist_triangle x y x\r\n _ = dist x y + dist x y := by rw [dist_comm x y]\r\n _ = dist x y * 2 := (mul_two (dist x y)).symm\r\n show 0 \u2264 dist x y\r\n exact nonneg_of_mul_nonneg_left h1 zero_lt_two\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : 0 \u2264 dist x y :=\r\nby\r\n apply nonneg_of_mul_nonneg_left\r\n . -- 0 \u2264 dist x y * 2\r\n calc 0 = dist x x := by simp only [dist_self]\r\n _ \u2264 dist x y + dist y x := by simp only [dist_triangle]\r\n _ = dist x y + dist x y := by simp only [dist_comm]\r\n _ = dist x y * 2 := by simp only [mul_two]\r\n . -- 0 < 2\r\n exact zero_lt_two\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : 0 \u2264 dist x y :=\r\nby\r\n have : 0 \u2264 dist x y + dist y x := by\r\n rw [\u2190 dist_self x]\r\n apply dist_triangle\r\n linarith [dist_comm x y]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : 0 \u2264 dist x y :=\r\n-- by apply?\r\ndist_nonneg\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- variable (a b : \u211d)\r\n-- variable (z : X)\r\n-- #check (dist_comm x y : dist x y = dist y x)\r\n-- #check (dist_nonneg : 0 \u2264 dist x y)\r\n-- #check (dist_self x : dist x x = 0)\r\n-- #check (dist_triangle x y z : dist x z \u2264 dist x y + dist y z)\r\n-- #check (mul_two a : a * 2 = a + a)\r\n-- #check (nonneg_of_mul_nonneg_left : 0 \u2264 a * b \u2192 0 < b \u2192 0 \u2264 a)\r\n-- #check (zero_lt_two : 0 < 2)\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