{"id":2506,"date":"2024-05-24T06:00:06","date_gmt":"2024-05-24T04:00:06","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=2506"},"modified":"2024-05-22T13:16:37","modified_gmt":"2024-05-22T11:16:37","slug":"24-may-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/24-may-24\/","title":{"rendered":"Los supremos de las sucesiones crecientes son sus l\u00edmites"},"content":{"rendered":"\n

Sea \(u\) una sucesi\u00f3n creciente. Demostrar con Lean4 que si \(S\) es un supremo de \(u\), entonces el l\u00edmite de \(u\) es \(S\).<\/p>\n

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

\nimport Mathlib.Data.Real.Basic\n\nvariable (u : \u2115 \u2192 \u211d)\nvariable (S : \u211d)\n\n-- (limite u c) expresa que el l\u00edmite de u es c.\ndef limite (u : \u2115 \u2192 \u211d) (c : \u211d) :=\n  \u2200 \u03b5 > 0, \u2203 m, \u2200 n \u2265 m, |u n - c| \u2264 \u03b5\n\n-- (supremo u S) expresa que el supremo de u es S.\ndef supremo (u : \u2115 \u2192 \u211d) (S : \u211d) :=\n  (\u2200 n, u n \u2264 S) \u2227 \u2200 \u03b5 > 0, \u2203 k, u k \u2265 S - \u03b5\n\nexample\n  (hu : Monotone u)\n  (hS : supremo u S)\n  : limite u S :=\nby sorry\n<\/pre>\n
<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(\u03b5 \u2208 \u211d\) tal que \(\u03b5 > 0\). Tenemos que demostrar que
\n\[ (\u2203 m \u2208 \u2115)(\u2200 n \u2208 \u2115)[n \u2265 m \u2192 |u_n – S| \u2264 \u03b5] \tag{1} \]<\/p>\n
Por ser \(S\) un supremo de u, existe un k \u2208 \u2115 tal que
\n\[ u_k \u2265 S – \u03b5 \tag{2} \]
\nVamos a demostrar que \(k\) verifica la condici\u00f3n de (1); es decir, que si \(n \u2208 \u2115\) tal que \(n \u2265 k\), entonces
\n\[ |u_n – S| \u2264 \u03b5 \]
\no, equivalentemente,
\n\[ -\u03b5 \u2264 u_n – S \u2264 \u03b5 \]<\/p>\n
La primera desigualdad se tiene por la siguente cadena:
\n\begin{align}
\n   -\u03b5 &= (S – \u03b5) – S    \\
\n      &\u2264 u_k – S         &&\text{[por (2)]} \\
\n      &\u2264 u_n – S         &&\text{[porque \(u\) es creciente y \(n \u2265 k\)]}
\n\end{align}<\/p>\n
La segunda desigualdad se tiene por la siguente cadena:
\n\begin{align}
\n   u_n – S &\u2264 S – S      &&\text{[porque \(S\) es un supremo de \(u\)]} \\
\n          &= 0          \\
\n          &\u2264 \u03b5
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n
\nimport Mathlib.Data.Real.Basic\n\nvariable (u : \u2115 \u2192 \u211d)\nvariable (S : \u211d)\n\n-- (limite u c) expresa que el l\u00edmite de u es c.\ndef limite (u : \u2115 \u2192 \u211d) (c : \u211d) :=\n  \u2200 \u03b5 > 0, \u2203 m, \u2200 n \u2265 m, |u n - c| \u2264 \u03b5\n\n-- (supremo u S) expresa que el supremo de u es S.\ndef supremo (u : \u2115 \u2192 \u211d) (S : \u211d) :=\n  (\u2200 n, u n \u2264 S) \u2227 \u2200 \u03b5 > 0, \u2203 k, u k \u2265 S - \u03b5\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : Monotone u)\n  (hS : supremo u S)\n  : limite u S :=\nby\n  unfold limite\n  -- \u22a2 \u2200 (\u03b5 : \u211d), \u03b5 > 0 \u2192 \u2203 m, \u2200 (n : \u2115), n \u2265 m \u2192 |u n - S| \u2264 \u03b5\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 m, \u2200 (n : \u2115), n \u2265 m \u2192 |u n - S| \u2264 \u03b5\n  unfold supremo at hS\n  -- hS : (\u2200 (n : \u2115), u n \u2264 S) \u2227 \u2200 (\u03b5 : \u211d), \u03b5 > 0 \u2192 \u2203 k, u k \u2265 S - \u03b5\n  cases' hS with hS\u2081 hS\u2082\n  -- hS\u2081 : \u2200 (n : \u2115), u n \u2264 S\n  -- hS\u2082 : \u2200 (\u03b5 : \u211d), \u03b5 > 0 \u2192 \u2203 k, u k \u2265 S - \u03b5\n  cases' hS\u2082 \u03b5 h\u03b5 with k hk\n  -- k : \u2115\n  -- hk : u k \u2265 S - \u03b5\n  use k\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 k \u2192 |u n - S| \u2264 \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 k\n  -- \u22a2 |u n - S| \u2264 \u03b5\n  rw [abs_le]\n  -- \u22a2 -\u03b5 \u2264 u n - S \u2227 u n - S \u2264 \u03b5\n  constructor\n  . -- \u22a2 -\u03b5 \u2264 u n - S\n    unfold Monotone at hu\n    -- hu : \u2200 \u2983a b : \u2115\u2984, a \u2264 b \u2192 u a \u2264 u b\n    specialize hu hn\n    -- hu : u k \u2264 u n\n    calc -\u03b5\n         = (S - \u03b5) - S := by ring\n       _ \u2264 u k - S     := sub_le_sub_right hk S\n       _ \u2264 u n - S     := sub_le_sub_right hu S\n  . calc u n - S\n         \u2264 S - S       := sub_le_sub_right (hS\u2081 n) S\n       _ = 0           := sub_self S\n       _ \u2264 \u03b5           := le_of_lt h\u03b5\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : Monotone u)\n  (hS : supremo u S)\n  : limite u S :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 m, \u2200 (n : \u2115), n \u2265 m \u2192 |u n - S| \u2264 \u03b5\n  cases' hS with hS\u2081 hS\u2082\n  -- hS\u2081 : \u2200 (n : \u2115), u n \u2264 S\n  -- hS\u2082 : \u2200 (\u03b5 : \u211d), \u03b5 > 0 \u2192 \u2203 k, u k \u2265 S - \u03b5\n  cases' hS\u2082 \u03b5 h\u03b5 with k hk\n  -- k : \u2115\n  -- hk : u k \u2265 S - \u03b5\n  use k\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 k \u2192 |u n - S| \u2264 \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 k\n  -- \u22a2 |u n - S| \u2264 \u03b5\n  rw [abs_le]\n  -- \u22a2 -\u03b5 \u2264 u n - S \u2227 u n - S \u2264 \u03b5\n  constructor\n  . -- \u22a2 -\u03b5 \u2264 u n - S\n    linarith [hu hn]\n  . -- \u22a2 u n - S \u2264 \u03b5\n    linarith [hS\u2081 n]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hu : Monotone u)\n  (hS : supremo u S)\n  : limite u S :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 m, \u2200 (n : \u2115), n \u2265 m \u2192 |u n - S| \u2264 \u03b5\n  cases' hS with hS\u2081 hS\u2082\n  -- hS\u2081 : \u2200 (n : \u2115), u n \u2264 S\n  -- hS\u2082 : \u2200 (\u03b5 : \u211d), \u03b5 > 0 \u2192 \u2203 k, u k \u2265 S - \u03b5\n  cases' hS\u2082 \u03b5 h\u03b5 with k hk\n  -- k : \u2115\n  -- hk : u k \u2265 S - \u03b5\n  use k\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 k \u2192 |u n - S| \u2264 \u03b5\n  intros n hn\n  -- n : \u2115\n  -- hn : n \u2265 k\n  -- \u22a2 |u n - S| \u2264 \u03b5\n  rw [abs_le]\n  -- \u22a2 -\u03b5 \u2264 u n - S \u2227 u n - S \u2264 \u03b5\n  constructor <;> linarith [hu hn, hS\u2081 n]\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (abs_le : |a| \u2264 b \u2194 -b \u2264 a \u2227 a \u2264 b)\n-- #check (le_of_lt : a < b \u2192 a \u2264 b)\n-- #check (sub_le_sub_right : a \u2264 b \u2192 \u2200 (c : \u211d), a - c \u2264 b - c)\n-- #check (sub_self a : a - a = 0)\n<\/pre>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
3. Demostraciones con Isabelle\/HOL<\/h2>\n
\ntheory Los_supremos_de_las_sucesiones_crecientes_son_sus_limites\nimports Main HOL.Real\nbegin\n\n(* (limite u c) expresa que el l\u00edmite de u es c. *)\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\" where\n  \"limite u c \u27f7 (\u2200\u03b5>0. \u2203k. \u2200n\u2265k. \u00a6u n - c\u00a6 \u2264 \u03b5)\"\n\n(* (supremo u M) expresa que el supremo de u es M. *)\ndefinition supremo :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\" where\n  \"supremo u M \u27f7 ((\u2200n. u n \u2264 M) \u2227 (\u2200\u03b5>0. \u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5))\"\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"mono u\"\n          \"supremo u M\"\n  shows   \"limite u M\"\nproof (unfold limite_def; intro allI impI)\n  fix \u03b5 :: real\n  assume \"0 < \u03b5\"\n  have hM : \"((\u2200n. u n \u2264 M) \u2227 (\u2200\u03b5>0. \u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5))\"\n    using assms(2)\n    by (simp add: supremo_def)\n  then have \"\u2200\u03b5>0. \u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5\"\n    by (rule conjunct2)\n  then have \"\u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5\"\n    by (simp only: \u20390 < \u03b5\u203a)\n  then obtain n0 where \"\u2200n\u2265n0. u n \u2265 M - \u03b5\"\n    by (rule exE)\n  have \"\u2200n\u2265n0. \u00a6u n - M\u00a6 \u2264 \u03b5\"\n  proof (intro allI impI)\n    fix n\n    assume \"n \u2265 n0\"\n    show \"\u00a6u n - M\u00a6 \u2264 \u03b5\"\n    proof (rule abs_leI)\n      have \"\u2200n. u n \u2264 M\"\n        using hM by (rule conjunct1)\n      then have \"u n - M \u2264 M - M\"\n        by simp\n      also have \"\u2026 = 0\"\n        by (simp only: diff_self)\n      also have \"\u2026 \u2264 \u03b5\"\n        using \u20390 < \u03b5\u203a by (simp only: less_imp_le)\n      finally show \"u n - M \u2264 \u03b5\"\n        by this\n    next\n      have \"-\u03b5 = (M - \u03b5) - M\"\n        by simp\n      also have \"\u2026 \u2264 u n - M\"\n        using \u2039\u2200n\u2265n0. M - \u03b5 \u2264 u n\u203a \u2039n0 \u2264 n\u203a by auto\n      finally have \"-\u03b5 \u2264 u n - M\"\n        by this\n      then show \"- (u n - M) \u2264 \u03b5\"\n        by simp\n    qed\n  qed\n  then show \"\u2203k. \u2200n\u2265k. \u00a6u n - M\u00a6 \u2264 \u03b5\"\n    by (rule exI)\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"mono u\"\n          \"supremo u M\"\n  shows   \"limite u M\"\nproof (unfold limite_def; intro allI impI)\n  fix \u03b5 :: real\n  assume \"0 < \u03b5\"\n  have hM : \"((\u2200n. u n \u2264 M) \u2227 (\u2200\u03b5>0. \u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5))\"\n    using assms(2)\n    by (simp add: supremo_def)\n  then have \"\u2203k. \u2200n\u2265k. u n \u2265 M - \u03b5\"\n    using \u20390 < \u03b5\u203a by presburger\n  then obtain n0 where \"\u2200n\u2265n0. u n \u2265 M - \u03b5\"\n    by (rule exE)\n  then have \"\u2200n\u2265n0. \u00a6u n - M\u00a6 \u2264 \u03b5\"\n    using hM by auto\n  then show \"\u2203k. \u2200n\u2265k. \u00a6u n - M\u00a6 \u2264 \u03b5\"\n    by (rule exI)\nqed\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"
Sea \(u\) una sucesi\u00f3n creciente. Demostrar con Lean4 que si \(S\) es un supremo de \(u\), entonces el l\u00edmite de \(u\) es \(S\). Para ello, completar la siguiente teor\u00eda de Lean4: import Mathlib.Data.Real.Basic variable (u : \u2115 \u2192 \u211d) variable (S : \u211d) — (limite u c) expresa que el l\u00edmite de u es c. def limite (u : \u2115 \u2192 \u211d) (c : \u211d) := \u2200 \u03b5 > 0, \u2203 m, \u2200 n \u2265 m, |u n – c| \u2264 \u03b5 — (supremo u S) expresa que el supremo de u es S. def supremo (u : \u2115 \u2192 \u211d) (S : \u211d) := (\u2200 n, u n \u2264 S) \u2227 \u2200 \u03b5 > 0, \u2203 k, u k \u2265 S – \u03b5 example…<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"default","_kad_post_title":"default","_kad_post_layout":"default","_kad_post_sidebar_id":"","_kad_post_content_style":"default","_kad_post_vertical_padding":"default","_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,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[14],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2506"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=2506"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2506\/revisions"}],"predecessor-version":[{"id":2508,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2506\/revisions\/2508"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=2506"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=2506"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=2506"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}