{"id":8068,"date":"2024-01-13T17:15:58","date_gmt":"2024-01-13T16:15:58","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8068"},"modified":"2024-01-13T17:16:18","modified_gmt":"2024-01-13T16:16:18","slug":"13-ene-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/13-ene-24\/","title":{"rendered":"La semana en Calculemus (13 de enero de 2024)"},"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, y > x\u00b2 \u22a2 y > 0 \u2228 y &lt; -1<\/a><\/li>\n<li><a href=\"#ej2\">2. En \u211d, -y > x\u00b2 + 1 \u22a2 y > 0 \u2228 y &lt; -1<\/a><\/li>\n<li><a href=\"#ej3\">3. En \u211d, si x &lt; |y|, entonces x &lt; y \u00f3 x &lt; -y<\/a><\/li>\n<li><a href=\"#ej4\">4. En \u211d, x \u2264 |x|<\/a><\/li>\n<li><a href=\"#ej5\">5. En \u211d, -x \u2264 |x|<\/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, y > x\u00b2 \u22a2 y > 0 \u2228 y &lt; -1<\/h3>\n<p>Demostrar con Lean4 que en &#92;(\u211d&#92;), &#92;(y > x^2 \u22a2 y > 0 \u2228 y &lt; -1&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\nexample\n  (h : y > x^2)\n  : y > 0 \u2228 y < -1 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Usando el lema<br \/>\n&#92;[ (\u2200 x \u2208 \u211d)[x\u00b2 \u2265 0] &#92;]<br \/>\nse tiene que<br \/>\n&#92;begin{align}<br \/>\n   y &amp;> x\u00b2 &amp;&amp;&#92;text{[por hip\u00f3tesis]} &#92;&#92;<br \/>\n     &amp;\u2265 0  &amp;&amp;&#92;text{[por el lema]}<br \/>\n&#92;end{align}<br \/>\nPor tanto, &#92;(y > 0&#92;) y, al verificar la primera parte de la diyunci\u00f3n, se verifica la disyunci\u00f3n.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : y > x^2)\n  : y > 0 \u2228 y < -1 :=\nby\n  have h1 : y > 0 := by\n    calc y > x^2 := h\n         _ \u2265 0   := pow_two_nonneg x\n  show y > 0 \u2228 y < -1\n  exact Or.inl h1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : y > x^2)\n  : y > 0 \u2228 y < -1 :=\nby\n  left\n  -- \u22a2 y > 0\n  calc y > x^2 := h\n       _ \u2265 0   := pow_two_nonneg x\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : y > x^2)\n  : y > 0 \u2228 y < -1 :=\nby\n  left\n  -- \u22a2 y > 0\n  linarith [pow_two_nonneg x]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : y > x^2)\n  : y > 0 \u2228 y < -1 :=\nby { left ; linarith [pow_two_nonneg x] }\n\n-- Lema usado\n-- ==========\n\n-- #check (pow_two_nonneg x : 0 \u2264 x ^ 2)\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\/Introduccion_de_la_disyuncion_1.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. 38.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. En \u211d, -y > x\u00b2 + 1 \u22a2 y > 0 \u2228 y &lt; -1<\/h3>\n<p>Demostrar con Lean4 que en &#92;(\u211d&#92;),<br \/>\n&#92;[ -y > x\u00b2 + 1 \u22a2 y > 0 \u2228 y &lt; -1 &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\nexample\n  (h : -y > x^2 + 1)\n  : y > 0 \u2228 y < -1 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Usaremos los siguientes lemas<br \/>\n&#92;begin{align}<br \/>\n   &amp;(\u2200 b, c \u2208 \u211d)[b \u2264 c \u2192 \u2200 (a : \u211d),  b + a \u2264 c + a)]               &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;(\u2200 a \u2208 \u211d)[0 \u2264 a\u00b2]                                              &#92;tag{L2} &#92;&#92;<br \/>\n   &amp;(\u2200 a  \u2208 \u211d)[0 + a = a]                                          &#92;tag{L3} &#92;&#92;<br \/>\n   &amp;(\u2200 a, b \u2208 \u211d)[a &lt; -b \u2194 b &lt; -a]                                  &#92;tag{L4}<br \/>\n&#92;end{align}<\/p>\n<p>Se tiene<br \/>\n&#92;begin{align}<br \/>\n   -y &amp;> x^2 + 1    &amp;&amp;&#92;text{[por la hip\u00f3tesis]} &#92;&#92;<br \/>\n      &amp;\u2265 0 + 1      &amp;&amp;&#92;text{[por L1 y L2]} &#92;&#92;<br \/>\n      &amp;= 1          &amp;&amp;&#92;text{[por L3]}<br \/>\n&#92;end{align}<br \/>\nPor tanto,<br \/>\n&#92;[ -y > 1 &#92;]<br \/>\ny, aplicando el lema L4, se tiene<br \/>\n&#92;[ y &lt; -1 &#92;]<br \/>\nComo se verifica la segunda parte de la disyunci\u00f3n, se verifica la disyunci\u00f3n.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : -y > x^2 + 1)\n  : y > 0 \u2228 y < -1 :=\nby\n  have h1 : -y > 1 := by\n    calc -y > x^2 + 1 := by exact h\n          _ \u2265 0 + 1   := add_le_add_right (pow_two_nonneg x) 1\n          _ = 1       := zero_add 1\n  have h2: y < -1 := lt_neg.mp h1\n  show y > 0 \u2228 y < -1\n  exact Or.inr h2\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : -y > x^2 + 1)\n  : y > 0 \u2228 y < -1 :=\nby\n  have h1 : -y > 1 := by linarith [pow_two_nonneg x]\n  have h2: y < -1 := lt_neg.mp h1\n  show y > 0 \u2228 y < -1\n  exact Or.inr h2\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : -y > x^2 + 1)\n  : y > 0 \u2228 y < -1 :=\nby\n  have h1: y < -1 := by linarith [pow_two_nonneg x]\n  show y > 0 \u2228 y < -1\n  exact Or.inr h1\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : -y > x^2 + 1)\n  : y > 0 \u2228 y < -1 :=\nby\n  right\n  -- \u22a2 y < -1\n  linarith [pow_two_nonneg x]\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : -y > x^2 + 1)\n  : y > 0 \u2228 y < -1 :=\nby { right ; linarith [pow_two_nonneg x] }\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c : \u211d)\n-- #check (add_le_add_right : b \u2264 c \u2192 \u2200 (a : \u211d),  b + a \u2264 c + a)\n-- #check (lt_neg : a < -b \u2194 b < -a)\n-- #check (pow_two_nonneg a : 0 \u2264 a ^ 2)\n-- #check (zero_add a : 0 + a = a)\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\/Introduccion_de_la_disyuncion_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. 39.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. En \u211d, si x &lt; |y|, entonces x &lt; y \u00f3 x &lt; -y<\/h3>\n<p>Demostrar con Lean4 que en &#92;(\u211d&#92;), si &#92;(x &lt; |y|&#92;), entonces &#92;(x &lt; y&#92;) \u00f3 &#92;(x &lt; -y&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\nexample : x < |y| \u2192 x < y \u2228 x < -y :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se demostrar\u00e1 por casos seg\u00fan &#92;(y \u2265 0&#92;).<\/p>\n<p>Primer caso: Supongamos que &#92;(y \u2265 0&#92;). Entonces, &#92;(|y| = y&#92;) y, por tanto, &#92;(x &lt; y&#92;).<\/p>\n<p>Segundo caso: Supongamos que &#92;(y &lt; 0&#92;). Entonces, &#92;(|y| = -y&#92;) y, por tanto, &#92;(x &lt; -y&#92;).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x < |y| \u2192 x < y \u2228 x < -y :=\nby\n  intro h1\n  -- h1 : x < |y|\n  -- \u22a2 x < y \u2228 x < -y\n  cases' le_or_gt 0 y with h2 h3\n  . -- h2 : 0 \u2264 y\n    left\n    -- \u22a2 x < y\n    rwa [abs_of_nonneg h2] at h1\n  . -- h3 : 0 > y\n    right\n    -- \u22a2 x < -y\n    rwa [abs_of_neg h3] at h1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x < |y| \u2192 x < y \u2228 x < -y :=\nlt_abs.mp\n\n-- Lemas usados\n-- ============\n\n-- #check (le_or_gt x y : x \u2264 y \u2228 x > y)\n-- #check (abs_of_nonneg : 0 \u2264 x \u2192 abs x = x)\n-- #check (abs_of_neg : x < 0 \u2192 abs x = -x)\n-- #check (lt_abs : x < |y| \u2194 x < y \u2228 x < -y)\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\/Eliminacion_de_la_disyuncion.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. 38.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. En \u211d, x \u2264 |x|<\/h3>\n<p>Demostrar con Lean4 que en &#92;(\u211d&#92;), &#92;(x \u2264 |x|&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x : \u211d}\n\nexample : x \u2264 |x| :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1n los siguientes lemas<br \/>\n&#92;begin{align}<br \/>\n   &amp;(\u2200 x \u2208 \u211d)[0 \u2264 x \u2192 |x| = x]                                     &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;(\u2200 x, y \u2208 \u211d)[x &lt; y \u2192 x \u2264 y]                                    &#92;tag{L2} &#92;&#92;<br \/>\n   &amp;(\u2200 x \u2208 \u211d)[x \u2264 0 \u2192 x \u2264 -x]                                      &#92;tag{L3} &#92;&#92;<br \/>\n   &amp;(\u2200 x \u2208 \u211d)[x &lt; 0 \u2192 |x| = -x]                                    &#92;tag{L4}<br \/>\n&#92;end{align}<\/p>\n<p>Se demostrar\u00e1 por casos seg\u00fan &#92;(x \u2265 0&#92;):<\/p>\n<p>Primer caso: Supongamos que &#92;(x \u2265 0&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   x &amp;\u2264 x      &#92;&#92;<br \/>\n     &amp;= |x|    &amp;&amp;&#92;text{[por L1]}<br \/>\n&#92;end{align}<\/p>\n<p>Segundo caso: Supongamos que &#92;(x &lt; 0&#92;). Entonces, por el L2, se tiene<br \/>\n&#92;[ x \u2264 0 &#92;tag{1} &#92;]<br \/>\nPor tanto,<br \/>\n&#92;begin{align}<br \/>\n   x &amp;\u2264 -x     &amp;&amp;&#92;text{[por L3 y (1)]} &#92;&#92;<br \/>\n     &amp;= |x|    &amp;&amp;&#92;text{[por L4]}<br \/>\n&#92;end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 |x| :=\nby\n  cases' le_or_gt 0 x with h1 h2\n  . -- h1 : 0 \u2264 x\n    show x \u2264 |x|\n    calc x \u2264 x   := le_refl x\n         _ = |x| := (abs_of_nonneg h1).symm\n  . -- h2 : 0 > x\n    have h3 : x \u2264 0 := le_of_lt h2\n    show x \u2264 |x|\n    calc x \u2264 -x  := le_neg_self_iff.mpr h3\n         _ = |x| := (abs_of_neg h2).symm\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 |x| :=\nby\n  cases' le_or_gt 0 x with h1 h2\n  . -- h1 : 0 \u2264 x\n    rw [abs_of_nonneg h1]\n  . -- h2 : 0 > x\n    rw [abs_of_neg h2]\n    -- \u22a2 x \u2264 -x\n    apply Left.self_le_neg\n    -- \u22a2 x \u2264 0\n    exact le_of_lt h2\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 |x| :=\nby\n  rcases (le_or_gt 0 x) with h1 | h2\n  . -- h1 : 0 \u2264 x\n    rw [abs_of_nonneg h1]\n  . -- h1 : 0 \u2264 x\n    rw [abs_of_neg h2]\n    linarith\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 |x| :=\n  le_abs_self x\n\n-- Lemas usados\n-- ============\n\n-- variable (y : \u211d)\n-- #check (Left.self_le_neg : x \u2264 0 \u2192 x \u2264 -x)\n-- #check (abs_of_neg : x < 0 \u2192 |x| = -x)\n-- #check (abs_of_nonneg : 0 \u2264 x \u2192 |x| = x)\n-- #check (le_abs_self x : x \u2264 |x|)\n-- #check (le_neg_self_iff : x \u2264 -x \u2194 x \u2264 0)\n-- #check (le_of_lt : x < y \u2192 x \u2264 y)\n-- #check (le_or_gt x y : x \u2264 y \u2228 x > y)\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\/Cota_inf_de_abs.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. 38.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. En \u211d, -x \u2264 |x|<\/h3>\n<p>Demostrar con Lean4 que en &#92;(\u211d&#92;), &#92;(-x \u2264 |x|&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x : \u211d}\n\nexample : -x \u2264 |x| :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1n los siguientes lemas<br \/>\n&#92;begin{align}<br \/>\n   &amp;(\u2200 x \u2208 \u211d)[0 \u2264 x \u2192 -x \u2264 x]                                      &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;(\u2200 x \u2208 \u211d)[0 \u2264 x \u2192 |x| = x]                                     &#92;tag{L2} &#92;&#92;<br \/>\n   &amp;(\u2200 x \u2208 \u211d)[x \u2264 x]                                               &#92;tag{L3} &#92;&#92;<br \/>\n   &amp;(\u2200 x \u2208 \u211d)[x &lt; 0 \u2192 |x| = -x]                                    &#92;tag{L4}<br \/>\n&#92;end{align}<\/p>\n<p>Se demostrar\u00e1 por casos seg\u00fan &#92;(x \u2265 0&#92;):<\/p>\n<p>Primer caso: Supongamos que &#92;(x \u2265 0&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   -x &amp;\u2264 x      &amp;&amp;&#92;text{[por L1]} &#92;&#92;<br \/>\n      &amp;= |x|    &amp;&amp;&#92;text{[por L2]}<br \/>\n&#92;end{align}<\/p>\n<p>Segundo caso: Supongamos que &#92;(x &lt; 0&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   -x &amp;\u2264 -x     &amp;&amp;&#92;text{[por L3]} &#92;&#92;<br \/>\n      &amp;= |x|    &amp;&amp;&#92;text{[por L4]}<br \/>\n&#92;end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : -x \u2264 |x| :=\nby\n  cases' (le_or_gt 0 x) with h1 h2\n  . -- h1 : 0 \u2264 x\n    show -x \u2264 |x|\n    calc -x \u2264 x   := by exact neg_le_self h1\n          _ = |x| := (abs_of_nonneg h1).symm\n  . -- h2 : 0 > x\n    show -x \u2264 |x|\n    calc -x \u2264 -x  := by exact le_refl (-x)\n          _ = |x| := (abs_of_neg h2).symm\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : -x \u2264 |x| :=\nby\n  cases' (le_or_gt 0 x) with h1 h2\n  . -- h1 : 0 \u2264 x\n    rw [abs_of_nonneg h1]\n    -- \u22a2 -x \u2264 x\n    exact neg_le_self h1\n  . -- h2 : 0 > x\n    rw [abs_of_neg h2]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : -x \u2264 |x| :=\nby\n  rcases (le_or_gt 0 x) with h1 | h2\n  . -- h1 : 0 \u2264 x\n    rw [abs_of_nonneg h1]\n    -- \u22a2 -x \u2264 x\n    linarith\n  . -- h2 : 0 > x\n    rw [abs_of_neg h2]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : -x \u2264 |x| :=\n  neg_le_abs_self x\n\n-- Lemas usados\n-- ============\n\n-- variable (y : \u211d)\n-- #check (abs_of_neg : x < 0 \u2192 |x| = -x)\n-- #check (abs_of_nonneg : 0 \u2264 x \u2192 |x| = x)\n-- #check (le_or_gt x y : x \u2264 y \u2228 x > y)\n-- #check (le_refl x : x \u2264 x)\n-- #check (neg_le_abs_self x : -x \u2264 |x|)\n-- #check (neg_le_self : 0 \u2264 x \u2192 -x \u2264 x)\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\/Cota_inf2_de_abs.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. 38.<\/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, y > x\u00b2 \u22a2 y > 0 \u2228 y &lt; -1 2. En \u211d, -y > x\u00b2 + 1 \u22a2 y > 0 \u2228 y &lt; -1 3. En \u211d, si x &lt; |y|, entonces x &lt; y&#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\/8068"}],"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=8068"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8068\/revisions"}],"predecessor-version":[{"id":8069,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8068\/revisions\/8069"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8068"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8068"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8068"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}