{"id":8010,"date":"2023-09-02T13:44:07","date_gmt":"2023-09-02T11:44:07","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8010"},"modified":"2023-09-02T13:44:07","modified_gmt":"2023-09-02T11:44:07","slug":"02-sep-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/02-sep-23\/","title":{"rendered":"La semana en Calculemus (2 de septiembre 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. En \u211d, si a \u2264 b y c &lt; d, entonces a + e\u1d9c + f \u2264 b + e\u1d48 + f<\/a><\/li>\n<li><a href=\"#ej2\">2. En \u211d, si d \u2264 f, entonces c + e^(a + d) \u2264 c + e^(a + f)<\/a><\/li>\n<li><a href=\"#ej3\">3. En \u211d, si a \u2264 b, entonces log(1+e^a) \u2264 log(1+e^b)<\/a><\/li>\n<li><a href=\"#ej4\">4. En \u211d, si a \u2264 b entonces c &#8211; e^b \u2264 c &#8211; e^a<\/a><\/li>\n<li><a href=\"#ej5\">5. En \u211d, 2ab \u2264 a\u00b2 + b\u00b2<\/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. En \u211d, si a \u2264 b y c &lt; d, entonces a + e\u1d9c + f \u2264 b + e\u1d48 + f<\/h3>\n<p>Demostrar con Lean4 que &#92;(a&#92;), &#92;(b&#92;), &#92;(c&#92;), &#92;(d&#92;) y &#92;(f&#92;) son n\u00fameros reales tales que &#92;(a &#92;leq b&#92;) y &#92;(c &lt; d&#92;), entonces<br \/>\n&#92;[a + e^c + f &#92;leq b + e^d + f&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\nopen Real\nvariable (a b c d f : \u211d)\n\nexample\n  (h1 : a \u2264 b)\n  (h2 : c < d)\n  : a + exp c + f < b + exp d + 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>Aplicando a la hip\u00f3tesis 3 (&#92;(c &lt; d&#92;)) la monoton\u00eda de la exponencial, se tiene<br \/>\n&#92;[e^c &lt; e^d&#92;]<br \/>\nque, junto a la hip\u00f3tesis 1 (&#92;(a &#92;leq b&#92;)) y la monoton\u00eda de la suma da<br \/>\n&#92;[a + e^c &lt; b + e^d&#92;]<br \/>\ny, de nuevo por la monoton\u00eda de la suma, se tiene<br \/>\n&#92;[a + e^c + f &lt; b + e^d + f&#92;]<\/p>\n<p><b>2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>Tenemos que demostrar que<br \/>\n&#92;[(a + e^c) + f &lt; (b + e^d) + f&#92;]<br \/>\nque, por la monoton\u00eda de la suma, se reduce a las siguientes dos desigualdades:<br \/>\n&#92;begin{align}<br \/>\n   &amp;a + e^c &lt; b + e^d &#92;tag{1} &#92;&#92;<br \/>\n   &amp;f &#92;leq f          &#92;tag{2}<br \/>\n&#92;end{align}<\/p>\n<p>La (1), de nuevo por la monoton\u00eda de la suma, se reduce a las siguientes dos:<br \/>\n&#92;begin{align}<br \/>\n   &amp;a &#92;leq b     &#92;tag{1.1} &#92;&#92;<br \/>\n   &amp;e^c &lt; e^d    &#92;tag{1.2}<br \/>\n&#92;end{align}<\/p>\n<p>&lt;<\/p>\n<p>div>La (1.1) se tiene por la hip\u00f3tesis 1, la (1.2) se tiene aplicando la monoton\u00eda de la exponencial a la hip\u00f3tesis 2 y la (2) se tiene por la propiedad reflexiva.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\nopen Real\nvariable (a b c d f : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : a \u2264 b)\n  (h2 : c < d)\n  : a + exp c + f < b + exp d + f :=\nby\n  have h3 : exp c < exp d :=\n    exp_lt_exp.mpr h2\n  have h4 : a + exp c < b + exp d :=\n    add_lt_add_of_le_of_lt h1 h3\n  show a + exp c + f < b + exp d + f\n  exact add_lt_add_right h4 f\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : a \u2264 b)\n  (h2 : c < d)\n  : a + exp c + f < b + exp d + f :=\nby\n  apply add_lt_add_of_lt_of_le\n  { apply add_lt_add_of_le_of_lt\n    { exact h1 }\n    { apply exp_lt_exp.mpr\n      exact h2 } }\n  { apply le_refl }\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : a \u2264 b)\n  (h2 : c < d)\n  : a + exp c + f < b + exp d + f :=\nby\n  apply add_lt_add_of_lt_of_le\n  . apply add_lt_add_of_le_of_lt h1\n    apply exp_lt_exp.mpr h2\n  rfl\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Inecuaciones_con_exponenciales_2.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. 15.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. En \u211d, si d \u2264 f, entonces c + e^(a + d) \u2264 c + e^(a + f)<\/h3>\n<p>Demostrar con Lean4 que si &#92;(a&#92;), &#92;(c&#92;), &#92;(d&#92;) y &#92;(f&#92;) son n\u00fameros reales tales que &#92;(d \u2264 f&#92;), entonces<br \/>\n&#92;[c + e^{a + d} &#92;leq c + e^{a + f}&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\nopen Real\nvariable (a c d f : \u211d)\n\nexample\n  (h : d \u2264 f)\n  : c + exp (a + d) \u2264 c + exp (a + 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>De la hip\u00f3tesis, por la monotonia de la suma, se tiene<br \/>\n&#92;[a + d &#92;leq a + f&#92;]<br \/>\nque, por la monoton\u00eda de la exponencial, da<br \/>\n&#92;[e^{a + d} &#92;leq e^{a + f}&#92;]<br \/>\ny, por la monoton\u00eda de la suma, se tiene<br \/>\n&#92;[c + e^{a + d} &#92;leq c + e^{a + f}&#92;]<\/p>\n<p><b>2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>Tenemos que demostrar que<br \/>\n&#92;[c + e^{a + d} &#92;leq c + e^{a + f}&#92;]<br \/>\nPor la monoton\u00eda de la suma, se reduce a<br \/>\n&#92;[e^{a + d} &#92;leq e^{a + f}&#92;]<br \/>\nque, por la monoton\u00eda de la exponencial, se reduce a<br \/>\n&#92;[a + d &#92;leq a + f&#92;]<br \/>\nque, por la monoton\u00eda de la suma, se reduce a<br \/>\n&#92;[d &#92;leq f&#92;]<br \/>\nque es la hip\u00f3tesis.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\nopen Real\nvariable (a c d f : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : d \u2264 f)\n  : c + exp (a + d) \u2264 c + exp (a + f) :=\nby\n  have h1 : a + d \u2264 a + f :=\n    add_le_add_left h a\n  have h2 : exp (a + d) \u2264 exp (a + f) :=\n    exp_le_exp.mpr h1\n  show c + exp (a + d) \u2264 c + exp (a + f)\n  exact add_le_add_left h2 c\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h : d \u2264 f)\n  : c + exp (a + d) \u2264 c + exp (a + f) :=\nby\n  apply add_le_add_left\n  apply exp_le_exp.mpr\n  apply add_le_add_left\n  exact h\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Inecuaciones_con_exponenciales_3.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. 15.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. En \u211d, si a \u2264 b, entonces log(1+e^a) \u2264 log(1+e^b)<\/h3>\n<p>Demostrar con Lean4 que si &#92;(a&#92;) y &#92;(b&#92;) son n\u00fameros reales tales que &#92;(a &#92;leq b&#92;), entonces<br \/>\n&#92;[&#92;log(1+e^a) &#92;leq &#92;log(1+e^b)&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\nopen Real\nvariable (a b : \u211d)\n\nexample\n  (h : a \u2264 b)\n  : log (1 + exp a) \u2264 log (1 + exp b) :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Por la monoton\u00eda del logaritmo, basta demostrar que<br \/>\n&#92;begin{align}<br \/>\n   &amp;0 &lt; 1 + e^a               &#92;tag{1} &#92;&#92;<br \/>\n   &amp;1 + e^a &#92;leq 1 + e^b      &#92;tag{2}<br \/>\n&#92;end{align}<\/p>\n<p>La (1), por la suma de positivos, se reduce a<br \/>\n&#92;begin{align}<br \/>\n   &amp;0 &lt; 1                       &#92;tag{1.1} &#92;&#92;<br \/>\n   &amp;0 &lt; e^a                     &#92;tag{1.2}<br \/>\n&#92;end{align}<br \/>\nLa (1.1) es una propiedad de los n\u00fameros naturales y la (1.2) de la<br \/>\nfunci\u00f3n exponencial.<\/p>\n<p>&lt;<\/p>\n<p>div>La (2), por la monoton\u00eda de la suma, se reduce a<br \/>\n&#92;[e^a &#92;leq e^b&#92;]<br \/>\nque, por la monoton\u00eda de la exponencial, se reduce a<br \/>\n&#92;[a &#92;leq b&#92;]<br \/>\nque es la hip\u00f3tesis.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\nopen Real\nvariable (a b : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : a \u2264 b)\n  : log (1 + exp a) \u2264 log (1 + exp b) :=\nby\n  have h1 : (0 : \u211d) < 1 :=\n    zero_lt_one\n  have h2 : 0 < exp a :=\n    exp_pos a\n  have h3 : 0 < 1 + exp a :=\n    add_pos h1 h2\n  have h4 : exp a \u2264 exp b :=\n    exp_le_exp.mpr h\n  have h5 : 1 + exp a \u2264 1 + exp b :=\n    add_le_add_left h4 1\n  show log (1 + exp a) \u2264 log (1 + exp b)\n  exact log_le_log' h3 h5\n\n-- 2\u00aa demostraci\u1e55n\nexample\n  (h : a \u2264 b)\n  : log (1 + exp a) \u2264 log (1 + exp b) :=\nby\n  apply log_le_log'\n  { apply add_pos\n    { exact zero_lt_one }\n    { exact exp_pos a }}\n  { apply add_le_add_left\n    exact exp_le_exp.mpr h }\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Desigualdad_logaritmica.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. 15.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. En \u211d, si a \u2264 b entonces c - e^b \u2264 c - e^a<\/h3>\n<p>Sean &#92;(a&#92;), &#92;(b&#92;) y &#92;(c&#92;) n\u00fameros reales. Demostrar con Lean4 que si &#92;(a &#92;leq b&#92;), entonces<br \/>\n&#92;[c - e^b &#92;leq c - e^a&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\n\nopen Real\n\nvariable (a b c : \u211d)\n\nexample\n  (h : a \u2264 b)\n  : c - exp b \u2264 c - exp a :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Aplicando la monoton\u00eda de la exponencial a la hip\u00f3tesis, se tiene<br \/>\n&#92;[e^a &#92;leq e^b&#92;]<br \/>\ny, restando de &#92;(c&#92;), se invierte la desigualdad<br \/>\n&#92;[c - e^b \u2264 c - e^a&#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\n\nopen Real\n\nvariable (a b c : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : a \u2264 b)\n  : c - exp b \u2264 c - exp a :=\nby\n   have h1 : exp a \u2264 exp b :=\n     exp_le_exp.mpr h\n   show c - exp b \u2264 c - exp a\n   exact sub_le_sub_left h1 c\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h : a \u2264 b)\n  : c - exp b \u2264 c - exp a :=\nby\n   apply sub_le_sub_left _ c\n   apply exp_le_exp.mpr h\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h : a \u2264 b)\n  : c - exp b \u2264 c - exp a :=\nsub_le_sub_left (exp_le_exp.mpr h) c\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h : a \u2264 b)\n  : c - exp b \u2264 c - exp a :=\nby linarith [exp_le_exp.mpr h]\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Inecuaciones_con_exponenciales_4.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. 16.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. En \u211d, 2ab \u2264 a\u00b2 + b\u00b2<\/h3>\n<p>Sean &#92;(a&#92;) y &#92;(b&#92;) n\u00fameros reales. Demostrar con Lean4 que<br \/>\n&#92;[2ab \u2264 a^2 + b^2&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (a b : \u211d)\n\nexample : 2*a*b \u2264 a^2 + b^2 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Puesto que los cuadrados son positivos, se tiene<br \/>\n&#92;[(a - b)^2 \u2265 0&#92;]<br \/>\nDesarrollando el cuadrado, se obtiene<br \/>\n&#92;[a^2 - 2ab + b^2 \u2265 0&#92;]<br \/>\nSumando &#92;(2ab&#92;) a ambos lados, queda<br \/>\n&#92;[a^2 + b^2 \u2265 2ab&#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (a b : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample : 2*a*b \u2264 a^2 + b^2 :=\nby\n  have h1 : 0 \u2264 (a - b)^2         := sq_nonneg (a - b)\n  have h2 : 0 \u2264 a^2 - 2*a*b + b^2 := by linarith only [h1]\n  show 2*a*b \u2264 a^2 + b^2\n  linarith\n\n-- 2\u00aa demostraci\u00f3n\nexample : 2*a*b \u2264 a^2 + b^2 :=\nby\n  have h : 0 \u2264 a^2 - 2*a*b + b^2\n  { calc a^2 - 2*a*b + b^2\n         = (a - b)^2                 := (sub_sq a b).symm\n       _ \u2265 0                         := sq_nonneg (a - b) }\n  calc 2*a*b\n       = 2*a*b + 0                   := (add_zero (2*a*b)).symm\n     _ \u2264 2*a*b + (a^2 - 2*a*b + b^2) := add_le_add (le_refl _) h\n     _ = a^2 + b^2                   := by ring\n\n-- 3\u00aa demostraci\u00f3n\nexample : 2*a*b \u2264 a^2 + b^2 :=\nby\n  have h : 0 \u2264 a^2 - 2*a*b + b^2\n  { calc a^2 - 2*a*b + b^2\n         = (a - b)^2       := (sub_sq a b).symm\n       _ \u2265 0               := sq_nonneg (a - b) }\n  linarith only [h]\n\n-- 4\u00aa demostraci\u00f3n\nexample : 2*a*b \u2264 a^2 + b^2 :=\n-- by apply?\ntwo_mul_le_add_sq a b\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Doble_me_suma_cuadrados.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. 16.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. En \u211d, si a \u2264 b y c &lt; d, entonces a + e\u1d9c + f \u2264 b + e\u1d48 + f 2. En \u211d, si d \u2264 f, entonces c + e^(a + d) \u2264 c + e^(a +&#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\/8010"}],"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=8010"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8010\/revisions"}],"predecessor-version":[{"id":8011,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8010\/revisions\/8011"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8010"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8010"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8010"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}