{"id":1730,"date":"2023-10-26T06:00:17","date_gmt":"2023-10-26T04:00:17","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1730"},"modified":"2023-10-19T12:19:48","modified_gmt":"2023-10-19T10:19:48","slug":"26-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/26-oct-23\/","title":{"rendered":"La composici\u00f3n de funciones inyectivas es inyectiva"},"content":{"rendered":"

Demostrar con Lean4 que la composici\u00f3n de funciones inyectivas es inyectiva.<\/p>\n

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

\nimport Mathlib.Tactic\n\nopen Function\n\nvariable {\u03b1 : Type _} {\u03b2 : Type _} {\u03b3 : Type _}\nvariable {f : \u03b1 \u2192 \u03b2} {g : \u03b2 \u2192 \u03b3}\n\nexample\n  (hg : Injective g)\n  (hf : Injective f) :\n  Injective (g \u2218 f) :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraciones en lenguaje natural (LN)<\/b><\/p>\n

\n1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Tenemos que demostrar que
\n\[ (\u2200 x, y) [(g \u2218 f)(x) = (g \u2218 f)(y) \u2192 x = y] \]
\nSean \(x, y\) tales que
\n\[ (g \u2218 f)(x) = (g \u2218 f)(y) \]
\nEntonces, por la definici\u00f3n de la composici\u00f3n,
\n\[ g(f(x)) = g(f(y)) \]
\ny, ser \(g\) inyectiva,
\n\[ f(x) = f(y) \]
\ny, ser \(f\) inyectiva,
\n\[ x = y \]<\/p>\n
2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Tenemos que demostrar que
\n\[ (\u2200 x, y) [(g \u2218 f)(x) = (g \u2218 f)(y) \u2192 x = y] \]
\nSean \(x, y\) tales que
\n\[ (g \u2218 f)(x) = (g \u2218 f)(y) \tag{1} \]
\ny tenemos que demostrar que
\n\[ x = y \tag{2} \]
\nEl objetivo (2), usando que \(f\) es inyectiva, se reduce a
\n\[ f(x) = f(y) \]
\nque, usando que \(g\) es inyectiva, se reduce a
\n\[ g(f(x)) = g(f(y)) \]
\nque, por la definici\u00f3n de la composici\u00f3n, coincide con (1).<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Tactic\n\nopen Function\n\nvariable {\u03b1 : Type _} {\u03b2 : Type _} {\u03b3 : Type _}\nvariable {f : \u03b1 \u2192 \u03b2} {g : \u03b2 \u2192 \u03b3}\n\n-- 1\u00aa demostraci\u00f3n (basada en la 1\u00aa en LN)\nexample\n  (hg : Injective g)\n  (hf : Injective f) :\n  Injective (g \u2218 f) :=\nby\n  intro (x : \u03b1) (y : \u03b1) (h1: (g \u2218 f) x = (g \u2218 f) y)\n  have h2: g (f x) = g (f y) := h1\n  have h3: f x = f y := hg h2\n  show x = y\n  exact hf h3\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (hg : Injective g)\n  (hf : Injective f) :\n  Injective (g \u2218 f) :=\nby\n  intro (x : \u03b1) (y : \u03b1) (h1: (g \u2218 f) x = (g \u2218 f) y)\n  have h2: f x = f y := hg h1\n  show x = y\n  exact hf h2\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (hg : Injective g)\n  (hf : Injective f) :\n  Injective (g \u2218 f) :=\nby\n  intro x y h\n  exact hf (hg h)\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (hg : Injective g)\n  (hf : Injective f) :\n  Injective (g \u2218 f) :=\nfun _ _ h \u21a6 hf (hg h)\n\n-- 5\u00aa demostraci\u00f3n (basada en la 2\u00aa en LN)\nexample\n  (hg : Injective g)\n  (hf : Injective f) :\n  Injective (g \u2218 f) :=\nby\n  intros x y h\n  -- x y : \u03b1\n  -- h : (g \u2218 f) x = (g \u2218 f) y\n  apply hf\n  -- \u22a2 f x = f y\n  apply hg\n  -- \u22a2 g (f x) = g (f y)\n  apply h\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (hg : Injective g)\n  (hf : Injective f) :\n  Injective (g \u2218 f) :=\n-- by exact?\nInjective.comp hg hf\n\n-- 7\u00aa demostraci\u00f3n\nexample\n  (hg : Injective g)\n  (hf : Injective f) :\n  Injective (g \u2218 f) :=\nby tauto\n\n-- Lemas usados\n-- ============\n\n-- #check (Injective.comp : Injective g \u2192 Injective f \u2192 Injective (g \u2218 f))\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