Demostrar con Lean4 que si \(f\) una funci\u00f3n de \(\u211d\) en \(\u211d\) tal que
\n\[ (\u2200 x, y)[f(x) \u2264 f(y) \u2192 x \u2264 y] \]
\nentonces \(f\) es inyectiva.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nopen Function\n\nvariable (f : \u211d \u2192 \u211d)\n\nexample\n (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n : Injective f :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sean \(x, y \u2208 \u211d\) tales que
\n\[ f(x) = f(y) \tag{1} \]
\nTenemos que demostrar que \(x = y\).<\/p>\n
De (1), tenemos que
\n\[ f(x) \u2264 f(y) \]
\ny, por la hip\u00f3tesis,
\n\[ x \u2264 y \tag{2} \]<\/p>\n
Tambi\u00e9n de (1), tenemos que
\n\[ f(y) \u2264 f(x) \]
\ny, por la hip\u00f3tesis,
\n\[ y \u2264 x \tag{3} \]<\/p>\n
De (2) y (3), tenemos que
\n\[ x = y \]<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Real.Basic\nopen Function\n\nvariable (f : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n : Injective f :=\nby\n intros x y hxy\n -- x y : \u211d\n -- hxy : f x = f y\n -- \u22a2 x = y\n have h1 : f x \u2264 f y := le_of_eq hxy\n have h2 : x \u2264 y := h h1\n have h3 : f y \u2264 f x := ge_of_eq hxy\n have h4 : y \u2264 x := h h3\n show x = y\n exact le_antisymm h2 h4\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n : Injective f :=\nby\n intros x y hxy\n -- x y : \u211d\n -- hxy : f x = f y\n -- \u22a2 x = y\n have h1 : x \u2264 y := h (le_of_eq hxy)\n have h2 : y \u2264 x := h (ge_of_eq hxy)\n show x = y\n exact le_antisymm h1 h2\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n : Injective f :=\nby\n intros x y hxy\n -- x y : \u211d\n -- hxy : f x = f y\n -- \u22a2 x = y\n show x = y\n exact le_antisymm (h (le_of_eq hxy)) (h (ge_of_eq hxy))\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n : Injective f :=\nfun _ _ hxy \u21a6 le_antisymm (h hxy.le) (h hxy.ge)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n : Injective f :=\nby\n intros x y hxy\n -- x y : \u211d\n -- hxy : f x = f y\n -- \u22a2 x = y\n apply le_antisymm\n . -- \u22a2 x \u2264 y\n apply h\n -- \u22a2 f x \u2264 f y\n exact le_of_eq hxy\n . -- \u22a2 y \u2264 x\n apply h\n -- \u22a2 f y \u2264 f x\n exact ge_of_eq hxy\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : \u2200 {x y}, f x \u2264 f y \u2192 x \u2264 y)\n : Injective f :=\nby\n intros x y hxy\n -- x y : \u211d\n -- hxy : f x = f y\n -- \u22a2 x = y\n apply le_antisymm\n . -- \u22a2 x \u2264 y\n exact h (le_of_eq hxy)\n . -- \u22a2 y \u2264 x\n exact h (ge_of_eq hxy)\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (ge_of_eq : a = b \u2192 a \u2265 b)\n-- #check (le_antisymm : a \u2264 b \u2192 b \u2264 a \u2192 a = b)\n-- #check (le_of_eq : a = b \u2192 a \u2264 b)\n<\/pre>\n