{"id":8040,"date":"2023-10-28T13:53:48","date_gmt":"2023-10-28T11:53:48","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8040"},"modified":"2023-10-28T13:53:48","modified_gmt":"2023-10-28T11:53:48","slug":"28-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/28-oct-23\/","title":{"rendered":"La semana en Calculemus (28 de octubre de 2023)"},"content":{"rendered":"\n<p>Esta semana he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. Si a es una cota superior de s y a \u2264 b, entonces b es una cota superior de s<\/a><\/li>\n<li><a href=\"#ej2\">2. La funci\u00f3n (x \u21a6 x + c) es inyectiva<\/a><\/li>\n<li><a href=\"#ej3\">3. Si c \u2260 0, entonces la funci\u00f3n (x \u21a6 cx) es inyectiva<\/a><\/li>\n<li><a href=\"#ej4\">4. La composici\u00f3n de funciones inyectivas es inyectiva<\/a><\/li>\n<li><a href=\"#ej5\">5. Hay alg\u00fan n\u00famero real entre 2 y 3<\/a><\/li>\n<\/ul>\n<p>A continuaci\u00f3n se muestran las soluciones.<br \/>\n<!--more--><br \/>\n<a name=\"ej1\"><\/a><\/p>\n<h3>1. Si a es una cota superior de s y a \u2264 b, entonces b es una cota superior de s<\/h3>\n<p>Demostrar con Lean4 que si &#92;(a&#92;) es una cota superior de &#92;(s&#92;) y &#92;(a \u2264 b&#92;), entonces &#92;(b&#92;) es una cota superior de &#92;(s&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\n\nvariable {\u03b1 : Type _} [PartialOrder \u03b1]\nvariable (s : Set \u03b1)\nvariable (a b : \u03b1)\n\n-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.\ndef CotaSupConj (s : Set \u03b1) (a : \u03b1) :=\n  \u2200 {x}, x \u2208 s \u2192 x \u2264 a\n\nexample\n  (h1 : CotaSupConj s a)\n  (h2 : a \u2264 b)\n  : CotaSupConj s b :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Tenemos que demostrar que<br \/>\n&#92;[ (\u2200 x) [x \u2208 s \u2192 x \u2264 b] &#92;]<br \/>\nSea &#92;(x&#92;) tal que &#92;(x \u2208 s&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   x &amp;\u2264 a   &amp;&amp;&#92;text{[porque &#92;(a&#92;) es una cota superior de &#92;(s&#92;)]} &#92;&#92;<br \/>\n     &amp;\u2264 b<br \/>\n&#92;end{align}<br \/>\nPor tanto, &#92;(x \u2264 b&#92;).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\n\nvariable {\u03b1 : Type _} [PartialOrder \u03b1]\nvariable (s : Set \u03b1)\nvariable (a b : \u03b1)\n\n-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.\ndef CotaSupConj (s : Set \u03b1) (a : \u03b1) :=\n  \u2200 {x}, x \u2208 s \u2192 x \u2264 a\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : CotaSupConj s a)\n  (h2 : a \u2264 b)\n  : CotaSupConj s b :=\nby\n  intro x (xs : x \u2208 s)\n  have h3 : x \u2264 a := h1 xs\n  show x \u2264 b\n  exact le_trans h3 h2\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : CotaSupConj s a)\n  (h2 : a \u2264 b)\n  : CotaSupConj s b :=\nby\n  intro x (xs : x \u2208 s)\n  calc x \u2264 a := h1 xs\n       _ \u2264 b := h2\n-\n-- Lemas usados\n-- ============\n\n-- variable (c : \u03b1)\n-- #check (le_trans : a \u2264 b \u2192 b \u2264 c \u2192 a \u2264 c)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Cotas_superiores_de_conjuntos.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 27.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. La funci\u00f3n (x \u21a6 x + c) es inyectiva<\/h3>\n<p>Demostrar con Lean4 que la funci\u00f3n &#92;(x \u21a6 x + c&#92;) es inyectiva.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nopen Function\n\nvariable {c : \u211d}\n\nexample : Injective ((. + c)) :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1 el lema<br \/>\n&#92;[ (\u2200 a, b, c) [a + b = c + b \u2192 a = c] &#92;tag{L1} &#92;]<\/p>\n<p>Hay que demostrar que<br \/>\n&#92;[ (\u2200 x\u2081, x\u2082) [f(x\u2081) = f(x\u2082) \u2192 x\u2081 = x\u2082] &#92;]<br \/>\nSean &#92;(x\u2081, x\u2082&#92;) tales que &#92;(f(x\u2081) = f(x\u2082)&#92;). Entonces,<br \/>\n&#92;[ x\u2081 + c = x\u2082 + c &#92;]<br \/>\ny, por L1, &#92;(x\u2081 = x\u2082&#92;).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nopen Function\n\nvariable {c : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\nexample : Injective ((. + c)) :=\nby\n  intro (x1 : \u211d) (x2 : \u211d) (h1 : x1 + c = x2 + c)\n  show x1 = x2\n  exact add_right_cancel h1\n\n-- 2\u00aa demostraci\u00f3n\nexample : Injective ((. + c)) :=\nby\n  intro x1 x2 h1\n  show x1 = x2\n  exact add_right_cancel h1\n\n-- 3\u00aa demostraci\u00f3n\nexample : Injective ((. + c)) :=\n  fun _ _ h \u21a6 add_right_cancel h\n\n-- Lemas usados\n-- ============\n\n-- variable {a b : \u211d}\n-- #check (add_right_cancel : a + b = c + b \u2192 a = c)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Suma_constante_es_inyectiva.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 28.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Si c \u2260 0, entonces la funci\u00f3n (x \u21a6 cx) es inyectiva<\/h3>\n<p>Demostrar con Lean4 que si &#92;(c \u2260 0&#92;), entonces la funci\u00f3n &#92;(x \u21a6 cx&#92;) es inyectiva.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nopen Function\nvariable {c : \u211d}\n\nexample\n  (h : c \u2260 0)\n  : Injective ((c * .)) :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1 el lema<br \/>\n&#92;[ (\u2200 a, b, c) [a \u2260 0 \u2192 (ab = ac \u2194 b = c))] &#92;tag{L1} &#92;]<\/p>\n<p>Hay que demostrar que<br \/>\n&#92;[ (\u2200 x\u2081, x\u2082) [f(x\u2081) = f(x\u2082) \u2192 x\u2081 = x\u2082] &#92;]<br \/>\nSean &#92;(x\u2081, x\u2082&#92;) tales que &#92;(f(x\u2081) = f(x\u2082)&#92;). Entonces,<br \/>\n&#92;[ cx\u2081 = cx\u2082 &#92;]<br \/>\ny, por L1 y puesto que &#92;(c \u2260 0&#92;), se tiene que<br \/>\n&#92;[ x\u2081 = x\u2082 &#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nopen Function\nvariable {c : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : c \u2260 0)\n  : Injective ((c * .)) :=\nby\n  intro (x1 : \u211d) (x2 : \u211d) (h1 : c * x1 = c * x2)\n  show x1 = x2\n  exact (mul_right_inj' h).mp h1\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h : c \u2260 0)\n  : Injective ((c * .)) :=\nfun _ _ h1 \u21a6 mul_left_cancel\u2080 h h1\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (mul_right_inj' : a \u2260 0 \u2192 (a * b = a * c \u2194 b = c))\n-- #check (mul_left_cancel\u2080 : a \u2260 0 \u2192 a * b = a * c \u2192 b = c)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Producto_constante_no_nula_es_inyectiva.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 28.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. La composici\u00f3n de funciones inyectivas es inyectiva<\/h3>\n<p>Demostrar con Lean4 que la composici\u00f3n de funciones inyectivas es inyectiva.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\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><b>Demostraciones en lenguaje natural (LN)<\/b><\/p>\n<p><b>1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>Tenemos que demostrar que<br \/>\n&#92;[ (\u2200 x, y) [(g \u2218 f)(x) = (g \u2218 f)(y) \u2192 x = y] &#92;]<br \/>\nSean &#92;(x, y&#92;) tales que<br \/>\n&#92;[ (g \u2218 f)(x) = (g \u2218 f)(y) &#92;]<br \/>\nEntonces, por la definici\u00f3n de la composici\u00f3n,<br \/>\n&#92;[ g(f(x)) = g(f(y)) &#92;]<br \/>\ny, ser &#92;(g&#92;) inyectiva,<br \/>\n&#92;[ f(x) = f(y) &#92;]<br \/>\ny, ser &#92;(f&#92;) inyectiva,<br \/>\n&#92;[ x = y &#92;]<\/p>\n<p><b>2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>Tenemos que demostrar que<br \/>\n&#92;[ (\u2200 x, y) [(g \u2218 f)(x) = (g \u2218 f)(y) \u2192 x = y] &#92;]<br \/>\nSean &#92;(x, y&#92;) tales que<br \/>\n&#92;[ (g \u2218 f)(x) = (g \u2218 f)(y) &#92;tag{1} &#92;]<br \/>\ny tenemos que demostrar que<br \/>\n&#92;[ x = y &#92;tag{2} &#92;]<br \/>\nEl objetivo (2), usando que &#92;(f&#92;) es inyectiva, se reduce a<br \/>\n&#92;[ f(x) = f(y) &#92;]<br \/>\nque, usando que &#92;(g&#92;) es inyectiva, se reduce a<br \/>\n&#92;[ g(f(x)) = g(f(y)) &#92;]<br \/>\nque, por la definici\u00f3n de la composici\u00f3n, coincide con (1).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\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<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Composicion_de_funciones_inyectivas.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 28.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. Hay alg\u00fan n\u00famero real entre 2 y 3<\/h3>\n<p>Demostrar con Lean4 que hay alg\u00fan n\u00famero real entre 2 y 3.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nexample : \u2203 x : \u211d, 2 < x \u2227 x < 3 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Puesto que &#92;(2 &lt; 5\/2 &lt; 3&#92;), basta elegir &#92;(5\/2&#92;).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\n-- 1\u00aa demostraci\u00f3n\nexample : \u2203 x : \u211d, 2 < x \u2227 x < 3 :=\nby\n  have h : 2 < (5 : \u211d) \/ 2 \u2227 (5 : \u211d) \/ 2 < 3 :=\n    by norm_num\n  show \u2203 x : \u211d, 2 < x \u2227 x < 3\n  exact Exists.intro (5 \/ 2) h\n\n-- 2\u00aa demostraci\u00f3n\nexample : \u2203 x : \u211d, 2 < x \u2227 x < 3 :=\nby\n  have h : 2 < (5 : \u211d) \/ 2 \u2227 (5 : \u211d) \/ 2 < 3 :=\n    by norm_num\n  show \u2203 x : \u211d, 2 < x \u2227 x < 3\n  exact \u27e85 \/ 2, h\u27e9\n\n-- 3\u00aa demostraci\u00f3n\nexample : \u2203 x : \u211d, 2 < x \u2227 x < 3 :=\nby\n  use 5 \/ 2\n  norm_num\n\n-- 4\u00aa demostraci\u00f3n\nexample : \u2203 x : \u211d, 2 < x \u2227 x < 3 :=\n\u27e85 \/ 2, by norm_num\u27e9\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Existencia_de_valor_intermedio.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 28.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. Si a es una cota superior de s y a \u2264 b, entonces b es una cota superior de s 2. La funci\u00f3n (x \u21a6 x + c) es inyectiva 3. Si c \u2260 0, entonces la funci\u00f3n (x \u21a6&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[335],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8040"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=8040"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8040\/revisions"}],"predecessor-version":[{"id":8041,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8040\/revisions\/8041"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8040"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8040"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8040"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}