Demostrar con Lean4 que, en los anillos ordenados,
\n\\[ \\{a \u2264 b, 0 \u2264 c\\} \u22a2 ac \u2264 bc \\]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Algebra.Order.Ring.Defs\r\nvariable {R : Type _} [StrictOrderedRing R]\r\nvariable (a b c : R)\r\n\r\nexample\r\n (h1 : a \u2264 b)\r\n (h2 : 0 \u2264 c)\r\n : a * c \u2264 b * c :=\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 a – b \u2194 b \u2264 a \\tag{L1} \\\\
\n &0 \u2264 a \u2192 0 \u2264 b \u2192 0 \u2264 ab \\tag{L2} \\\\
\n &(a – b)c = ac – bc \\tag{L3}
\n\\end{align}<\/p>\n
Supongamos que
\n\\begin{align}
\n a &\u2264 b \\tag{1} \\\\
\n 0 &\u2264 c
\n\\end{align}
\nDe (1), por L1, se tiene
\n\\[ 0 \u2264 b – a \\]
\ny con (2), por L2, se tiene
\n\\[ 0 \u2264 (b – a)c \\]
\nque, por L3, da
\n\\[ 0 \u2264 bc – ac \\]
\ny, aplic\u00e1ndole L1, se tiene
\n\\[ ac \u2264 bc \\]<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Algebra.Order.Ring.Defs\r\nvariable {R : Type _} [StrictOrderedRing R]\r\nvariable (a b c : R)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h1 : a \u2264 b)\r\n (h2 : 0 \u2264 c)\r\n : a * c \u2264 b * c :=\r\nby\r\n have h3 : 0 \u2264 b - a :=\r\n sub_nonneg.mpr h1\r\n have h4 : 0 \u2264 b * c - a * c := calc\r\n 0 \u2264 (b - a) * c := mul_nonneg h3 h2\r\n _ = b * c - a * c := sub_mul b a c\r\n show a * c \u2264 b * c\r\n exact sub_nonneg.mp h4\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h1 : a \u2264 b)\r\n (h2 : 0 \u2264 c)\r\n : a * c \u2264 b * c :=\r\nby\r\n have h3 : 0 \u2264 b - a := sub_nonneg.mpr h1\r\n have h4 : 0 \u2264 (b - a) * c := mul_nonneg h3 h2\r\n -- h4 : 0 \u2264 b * c - a * c\r\n rw [sub_mul] at h4\r\n -- a * c \u2264 b * c\r\n exact sub_nonneg.mp h4\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h1 : a \u2264 b)\r\n (h2 : 0 \u2264 c)\r\n : a * c \u2264 b * c :=\r\nby\r\n -- 0 \u2264 b * c - a * c\r\n apply sub_nonneg.mp\r\n -- 0 \u2264 (b - a) * c\r\n rw [\u2190 sub_mul]\r\n apply mul_nonneg\r\n . -- 0 \u2264 b - a\r\n exact sub_nonneg.mpr h1\r\n . -- 0 \u2264 c\r\n exact h2\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h1 : a \u2264 b)\r\n (h2 : 0 \u2264 c)\r\n : a * c \u2264 b * c :=\r\nby\r\n apply sub_nonneg.mp\r\n rw [\u2190 sub_mul]\r\n apply mul_nonneg (sub_nonneg.mpr h1) h2\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample\r\n (h1 : a \u2264 b)\r\n (h2 : 0 \u2264 c)\r\n : a * c \u2264 b * c :=\r\n-- by apply?\r\nmul_le_mul_of_nonneg_right h1 h2\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- #check (mul_le_mul_of_nonneg_right : a \u2264 b \u2192 0 \u2264 c \u2192 a * c \u2264 b * c)\r\n-- #check (mul_nonneg : 0 \u2264 a \u2192 0 \u2264 b \u2192 0 \u2264 a * b)\r\n-- #check (sub_mul a b c : (a - b) * c = a * c - b * c)\r\n-- #check (sub_nonneg : 0 \u2264 a - b \u2194 b \u2264 a)\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