{"id":8058,"date":"2023-12-10T07:00:28","date_gmt":"2023-12-10T06:00:28","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8058"},"modified":"2023-12-12T11:34:17","modified_gmt":"2023-12-12T10:34:17","slug":"10-dic-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/10-dic-23\/","title":{"rendered":"La semana en Calculemus (10 de diciembre 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. P \u2192 \u00ac\u00acP<\/a><\/li>\n<li><a href=\"#ej2\">2. Si f no est\u00e1 acotada superiormente, entonces (\u2200a)(\u2203x)(f(x) > a)<\/a><\/li>\n<li><a href=\"#ej3\">3. Si \u00ac(\u2200a)(\u2203x)(f(x) > a), entonces f est\u00e1 acotada superiormente<\/a><\/li>\n<li><a href=\"#ej4\">4. Si f no es mon\u00f3tona, entonces \u2203x\u2203y(x \u2264 y \u2227 f(y) &lt; f(x))\u200b<\/a><\/li>\n<li><a href=\"#ej5\">5. Si 0 &lt; 0, entonces a > 37 para cualquier n\u00famero a<\/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. P \u2192 \u00ac\u00acP<\/h3>\n<p>Demostrar con Lean4 que &#92;(P \u2192 \u00ac\u00acP&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nvariable (P : Prop)\n\nexample\n  (h : P)\n  : \u00ac\u00acP :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Supongamos &#92;(\u00acP&#92;). Entonces, tenemos una contradicci\u00f3n con la hip\u00f3tesis (&#92;(P&#92;)).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nvariable (P : Prop)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : P)\n  : \u00ac\u00acP :=\nby\n  intro h1\n  -- h1 : \u00acP\n  -- \u22a2 False\n  exact (h1 h)\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : P)\n  : \u00ac\u00acP :=\nfun h1 \u21a6 h1 h\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : P)\n  : \u00ac\u00acP :=\nnot_not_intro h\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : P)\n  : \u00ac \u00ac P :=\nby tauto\n\n-- Lemas usados\n-- ============\n\n-- #check (not_not_intro : P \u2192 \u00ac\u00acP)\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_doble_negacion.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. 33.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. Si f no est\u00e1 acotada superiormente, entonces (\u2200a)(\u2203x)[f(x) > a]<\/h3>\n<p>Demostrar con Lean4 que si &#92;(f&#92;) no est\u00e1 acotada superiormente, entonces &#92;((\u2200a)(\u2203x)[f(x) > a]\u200b&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, f x \u2264 a\n\ndef acotadaSup (f : \u211d \u2192 \u211d) :=\n  \u2203 a, CotaSuperior f a\n\nvariable (f : \u211d \u2192 \u211d)\n\nexample\n  (h : \u00acacotadaSup f)\n  : \u2200 a, \u2203 x, f x > a :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p><b>1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>Usaremos los siguientes lemas<br \/>\n&#92;begin{align}<br \/>\n   &amp;\u00ac(\u2203x)P(x) \u2192 (\u2200x)\u00acP(x) &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;\u00aca > b \u2192 a \u2264 b        &#92;tag{L2}<br \/>\n&#92;end{align}<\/p>\n<p>Sea &#92;(a \u2208 \u211d&#92;). Tenemos que demostrar que<br \/>\n&#92;[ (\u2203x)[f(x) > a] &#92;]<br \/>\nLo haremos por reducci\u00f3n al absurdo. Para ello, suponemos que<br \/>\n&#92;[ \u00ac(\u2203x)[f(x) > a] &#92;tag{1} &#92;]<br \/>\ny tenemos que obtener una contradicci\u00f3n. Aplicando L1 a (1) se tiene<br \/>\n&#92;[ (\u2200x)[\u00ac f(x) > a] &#92;]<br \/>\ny, aplicando L2, se tiene<br \/>\n&#92;[ (\u2200x)[f(x) \u2264 a] &#92;]<br \/>\nLo que significa que &#92;(a&#92;) es una cota superior de &#92;(f&#92;) y, por tanto &#92;(f&#92;) est\u00e1 acotada superiormente, en cotradicci\u00f3n con la hip\u00f3tesis.<\/p>\n<p><b>2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n<p>Por la contrarec\u00edproca, se supone que<br \/>\n&#92;[ \u00ac(\u2200a)(\u2203x)[f(x) > a] &#92;tag{1} &#92;]<br \/>\ny tenemos que demostrar que &#92;(f&#92;) est\u00e1 acotada superiormente.<\/p>\n<p>Interiorizando la negaci\u00f3n en (1) y simplificando, se tiene que<br \/>\n&#92;[ (\u2203a)(\u2200x)[f x \u2264 a] &#92;]<br \/>\nque es lo que ten\u00edamos que demostrar.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, f x \u2264 a\n\ndef acotadaSup (f : \u211d \u2192 \u211d) :=\n  \u2203 a, CotaSuperior f a\n\nvariable (f : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00acacotadaSup f)\n  : \u2200 a, \u2203 x, f x > a :=\nby\n  intro a\n  -- a : \u211d\n  -- \u22a2 \u2203 x, f x > a\n  by_contra h1\n  -- h1 : \u00ac\u2203 x, f x > a\n  -- \u22a2 False\n  have h2 : \u2200 x, \u00ac f x > a :=\n    forall_not_of_not_exists h1\n  have h3 : \u2200 x, f x \u2264 a := by\n    intro x\n    have h3a : \u00ac f x > a := h2 x\n    show f x \u2264 a\n    exact le_of_not_gt h3a\n  have h4 : CotaSuperior f a := h3\n  have h5 : \u2203 b, CotaSuperior f b := \u27e8a, h4\u27e9\n  have h6 : acotadaSup f := h5\n  show False\n  exact h h6\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00acacotadaSup f)\n  : \u2200 a, \u2203 x, f x > a :=\nby\n  intro a\n  -- a : \u211d\n  -- \u22a2 \u2203 x, f x > a\n  by_contra h1\n  -- h1 : \u00ac\u2203 x, f x > a\n  -- \u22a2 False\n  apply h\n  -- \u22a2 acotadaSup f\n  use a\n  -- \u22a2 CotaSuperior f a\n  intro x\n  -- x : \u211d\n  -- \u22a2 f x \u2264 a\n  apply le_of_not_gt\n  -- \u22a2 \u00acf x > a\n  intro h2\n  -- h2 : f x > a\n  -- \u22a2 False\n  apply h1\n  -- \u22a2 \u2203 x, f x > a\n  use x\n  -- \u22a2 f x > a\n  exact h2\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00acacotadaSup f)\n  : \u2200 a, \u2203 x, f x > a :=\nby\n  unfold acotadaSup at h\n  -- h : \u00ac\u2203 a, CotaSuperior f a\n  unfold CotaSuperior at h\n  -- h : \u00ac\u2203 a, \u2200 (x : \u211d), f x \u2264 a\n  push_neg at h\n  -- \u2200 (a : \u211d), \u2203 x, f x > a\n  exact h\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00acacotadaSup f)\n  : \u2200 a, \u2203 x, f x > a :=\nby\n  simp only [acotadaSup, CotaSuperior] at h\n  -- h : \u00ac\u2203 a, \u2200 (x : \u211d), f x \u2264 a\n  push_neg at h\n  -- \u2200 (a : \u211d), \u2203 x, f x > a\n  exact h\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00acacotadaSup f) :\n  \u2200 a, \u2203 x, f x > a :=\nby\n  contrapose h\n  -- h : \u00ac\u2200 (a : \u211d), \u2203 x, f x > a\n  -- \u22a2 \u00ac\u00acacotadaSup f\n  push_neg at *\n  -- h : \u2203 a, \u2200 (x : \u211d), f x \u2264 a\n  -- \u22a2 acotadaSup f\n  exact h\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00acacotadaSup f) :\n  \u2200 a, \u2203 x, f x > a :=\nby\n  contrapose! h\n  -- h : \u2203 a, \u2200 (x : \u211d), f x \u2264 a\n  -- \u22a2 acotadaSup f\n  exact h\n\n-- Lemas usados\n-- ============\n\n-- variable {\u03b1 : Type _}\n-- variable (P : \u03b1 \u2192 Prop)\n-- #check (forall_not_of_not_exists : (\u00ac\u2203 x, P x) \u2192 \u2200 x, \u00acP x)\n--\n-- variable (a b : \u211d)\n-- #check (le_of_not_gt : \u00aca > b \u2192 a \u2264 b)\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\/CN_no_acotada_superiormente.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. 33.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Si \u00ac(\u2200a)(\u2203x)[f(x) > a]\u200b, entonces f est\u00e1 acotada superiormente<\/h3>\n<p>Demostrar con Lean4 que si &#92;(\u00ac(\u2200a)(\u2203x)[f(x) > a]&#92;)\u200b, entonces &#92;(f&#92;) est\u00e1 acotada superiormente.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, f x \u2264 a\n\ndef acotadaSup (f : \u211d \u2192 \u211d) :=\n  \u2203 a, CotaSuperior f a\n\nvariable (f : \u211d \u2192 \u211d)\n\nexample\n  (h : \u00ac\u2200 a, \u2203 x, f x > a)\n  : acotadaSup f :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Tenemos que demostrar que &#92;(f&#92;) es acotada superiormente; es decir, que<br \/>\n&#92;[ (\u2203a)(\u2200x)[f(x) \u2264 a] &#92;]<br \/>\nque es exactamente la f\u00f3rmula obtenida interiorizando la negaci\u00f3n en la hip\u00f3tesis.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, f x \u2264 a\n\ndef acotadaSup (f : \u211d \u2192 \u211d) :=\n  \u2203 a, CotaSuperior f a\n\nvariable (f : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00ac\u2200 a, \u2203 x, f x > a)\n  : acotadaSup f :=\nby\n  unfold acotadaSup\n  -- \u22a2 \u2203 a, CotaSuperior f a\n  unfold CotaSuperior\n  -- \u22a2 \u2203 a, \u2200 (x : \u211d), f x \u2264 a\n  push_neg at h\n  -- h : \u2203 a, \u2200 (x : \u211d), f x \u2264 a\n  exact h\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00ac\u2200 a, \u2203 x, f x > a)\n  : acotadaSup f :=\nby\n  unfold acotadaSup CotaSuperior\n  -- \u22a2 \u2203 a, \u2200 (x : \u211d), f x \u2264 a\n  push_neg at h\n  -- h : \u2203 a, \u2200 (x : \u211d), f x \u2264 a\n  exact h\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00ac\u2200 a, \u2203 x, f x > a)\n  : acotadaSup f :=\nby\n  push_neg at h\n  -- h : \u2203 a, \u2200 (x : \u211d), f x \u2264 a\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:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/CS_de_acotada_superiormente.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. 34.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. Si f no es mon\u00f3tona, entonces \u2203x\u2203y[x \u2264 y \u2227 f(y) &lt; f(x)]<\/h3>\n<p>Demostrar con Lean4 que si &#92;(f&#92;) no es mon\u00f3tona, entonces &#92;(\u2203x\u2203y[x \u2264 y \u2227 f(y) &lt; f(x)]\u200b&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nvariable (f : \u211d \u2192 \u211d)\n\nexample\n  (h : \u00acMonotone f)\n  : \u2203 x y, x \u2264 y \u2227 f y < f x :=\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;\u00ac(\u2200x)P(x) \u2194 (\u2203 x)\u00acP(x)      &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;\u00ac(p \u2192 q) \u2194 p \u2227 \u00acq           &#92;tag{L2} &#92;&#92;<br \/>\n   &amp;(\u2200a, b \u2208 \u211d)[\u00acb \u2264 a \u2192 a &lt; b] &#92;tag{L3}<br \/>\n&#92;end{align}<\/p>\n<p>Por la definici\u00f3n de funci\u00f3n mon\u00f3tona,<br \/>\n&#92;[ \u00ac(\u2200x)(\u2200y)[x \u2264 y \u2192 f(x) \u2264 f(y)] &#92;]<br \/>\nAplicando L1 se tiene<br \/>\n&#92;[ (\u2203x)\u00ac(\u2200y)[x \u2264 y \u2192 f(x) \u2264 f(y)] &#92;]<br \/>\nSea &#92;(a&#92;) tal que<br \/>\n&#92;[ \u00ac(\u2200y)[a \u2264 y \u2192 f(a) \u2264 f(y)] &#92;]<br \/>\nAplicando L1 se tiene<br \/>\n&#92;[ (\u2203y)\u00ac[a \u2264 y \u2192 f(a) \u2264 f(y)] &#92;]<br \/>\nSea &#92;(b&#92;) tal que<br \/>\n&#92;[ \u00ac[a \u2264 b \u2192 f(a) \u2264 f(b)] &#92;]<br \/>\nAplicando L2 se tiene que<br \/>\n&#92;[ a \u2264 b \u2227 \u00ac(f(a) \u2264 f(b)) &#92;]<br \/>\nAplicando L3 se tiene que<br \/>\n&#92;[ a \u2264 b \u2227 f(b) &lt; f(a) &#92;]<br \/>\nPor tanto,<br \/>\n&#92;[ (\u2203x,y)[x \u2264 y \u2227 f(y) &lt; f(x)] &#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nvariable (f : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00acMonotone f)\n  : \u2203 x y, x \u2264 y \u2227 f y < f x :=\nby\n  have h1 : \u00ac\u2200 x y, x \u2264 y \u2192 f x \u2264 f y := h\n  have h2 : \u2203 x, \u00ac(\u2200 y, x \u2264 y \u2192 f x \u2264 f y) := not_forall.mp h1\n  rcases h2 with \u27e8a, ha : \u00ac\u2200 y, a \u2264 y \u2192 f a \u2264 f y\u27e9\n  have h3 : \u2203 y, \u00ac(a \u2264 y \u2192 f a \u2264 f y) := not_forall.mp ha\n  rcases h3 with \u27e8b, hb : \u00ac(a \u2264 b \u2192 f a \u2264 f b)\u27e9\n  have h4 : a \u2264 b \u2227 \u00ac(f a \u2264 f b) := not_imp.mp hb\n  have h5 : a \u2264 b \u2227 f b < f a := \u27e8h4.1, lt_of_not_le h4.2\u27e9\n  use a, b\n  -- \u22a2 a \u2264 b \u2227 f b < f a\n  exact h5\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u00acMonotone f)\n  : \u2203 x y, x \u2264 y \u2227 f y < f x :=\nby\n  simp only [Monotone] at h\n  -- h : \u00ac\u2200 \u2983a b : \u211d\u2984, a \u2264 b \u2192 f a \u2264 f b\n  push_neg at h\n  -- h : Exists fun \u2983a\u2984 => Exists fun \u2983b\u2984 => a \u2264 b \u2227 f b < f a\n  exact h\n\n-- Lemas usados\n-- ============\n\n-- variable {\u03b1 : Type _}\n-- variable (P : \u03b1 \u2192 Prop)\n-- variable (p q : Prop)\n-- variable (a b : \u211d)\n-- #check (not_forall : (\u00ac\u2200 x, P x) \u2194 \u2203 x, \u00acP x)\n-- #check (not_imp : \u00ac(p \u2192 q) \u2194 p \u2227 \u00acq)\n-- #check (lt_of_not_le : \u00acb \u2264 a \u2192 a < b)\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\/CN_de_no_monotona.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. 34.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. Si 0 &lt; 0, entonces a > 37 para cualquier n\u00famero a<\/h3>\n<p>Demostrar con Lean4 que si &#92;(0 &lt; 0&#92;), entonces &#92;(a > 37&#92;) para cualquier n\u00famero &#92;(a&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\n\nvariable (a : \u2115)\n\nexample\n  (h : 0 < 0)\n  : a > 37 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Basta demostrar una contradicci\u00f3n, ya que de una contradicci\u00f3n se sigue cualquier cosa.<\/p>\n<p>La hip\u00f3tesis es una contradicci\u00f3n con la propiedad irreflexiva de la relaci\u00f3n &#92;(&lt;&#92;).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\n\nvariable (a : \u2115)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : 0 < 0)\n  : a > 37 :=\nby\n  exfalso\n  -- \u22a2 False\n  show False\n  exact lt_irrefl 0 h\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : 0 < 0)\n  : a > 37 :=\nby\n  exfalso\n  -- \u22a2 False\n  apply lt_irrefl 0 h\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : 0 < 0)\n  : a > 37 :=\nabsurd h (lt_irrefl 0)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : 0 < 0)\n  : a > 37 :=\nby\n  have : \u00ac 0 < 0 :=  lt_irrefl 0\n  contradiction\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : 0 < 0)\n  : a > 37 :=\nby linarith\n\n-- Lemas usados\n-- ============\n\n-- variable (p q : Prop)\n-- #check (lt_irrefl a : \u00aca < a)\n-- #check (absurd : p \u2192 \u00acp \u2192 q)\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\/Principio_de_explosion.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. 34.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. P \u2192 \u00ac\u00acP 2. Si f no est\u00e1 acotada superiormente, entonces (\u2200a)(\u2203x)(f(x) > a) 3. Si \u00ac(\u2200a)(\u2203x)(f(x) > a), entonces f est\u00e1 acotada superiormente 4. Si f no es mon\u00f3tona, entonces \u2203x\u2203y(x \u2264 y \u2227 f(y) &lt; f(x))\u200b 5. Si&#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\/8058"}],"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=8058"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8058\/revisions"}],"predecessor-version":[{"id":8059,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8058\/revisions\/8059"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8058"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8058"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8058"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}