julio 2021 – Calculemus

Producto de una sucesión acotada por otra convergente a cero

PorJosé A. Alonso 31 julio 2021

Demostrar que el producto de una sucesión acotada por una convergente a 0 también converge a 0.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
import tactic

variables (u v : ℕ → ℝ)
variable  (a : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (c : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

def acotada (a : ℕ → ℝ) :=
∃ B, ∀ n, |a n| ≤ B

example
  (hU : acotada u)
  (hV : limite v 0)
  : limite (u*v) 0 :=
sorry

import data.real.basic

import tactic

variables (u v : ℕ → ℝ)

variable (a : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

def acotada (a : ℕ → ℝ) :=

∃ B, ∀ n, |a n| ≤ B

example

(hU : acotada u)

(hV : limite v 0)

: limite (u*v) 0 :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

variables (u v : ℕ → ℝ)
variable  (a : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (c : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

def acotada (a : ℕ → ℝ) :=
∃ B, ∀ n, |a n| ≤ B

-- 1ª demostración
example
  (hU : acotada u)
  (hV : limite v 0)
  : limite (u*v) 0 :=
begin
  cases hU with B hB,
  have hBnoneg : 0 ≤ B,
    calc 0 ≤ |u 0| : abs_nonneg (u 0)
       ... ≤ B     : hB 0,
  by_cases hB0 : B = 0,
  { subst hB0,
    intros ε hε,
    use 0,
    intros n hn,
    simp_rw [sub_zero] at *,
    calc |(u * v) n|
         = |u n * v n|   : congr_arg abs (pi.mul_apply u v n)
     ... = |u n| * |v n| : abs_mul (u n) (v n)
     ... ≤ 0 * |v n|     : mul_le_mul_of_nonneg_right (hB n) (abs_nonneg (v n))
     ... = 0             : zero_mul (|v n|)
     ... < ε             : hε, },
  { change B ≠ 0 at hB0,
    have hBpos : 0 < B := (ne.le_iff_lt hB0.symm).mp hBnoneg,
    intros ε hε,
    cases hV (ε/B) (div_pos hε hBpos) with N hN,
    use N,
    intros n hn,
    simp_rw [sub_zero] at *,
    calc |(u * v) n|
         = |u n * v n|    : congr_arg abs (pi.mul_apply u v n)
     ... = |u n| * |v n|  : abs_mul (u n) (v n)
     ... ≤ B * |v n|      : mul_le_mul_of_nonneg_right (hB n) (abs_nonneg _)
     ... < B * (ε/B)      : mul_lt_mul_of_pos_left (hN n hn) hBpos
     ... = ε              : mul_div_cancel' ε hB0 },
end

-- 2ª demostración
example
  (hU : acotada u)
  (hV : limite v 0)
  : limite (u*v) 0 :=
begin
  cases hU with B hB,
  have hBnoneg : 0 ≤ B,
    calc 0 ≤ |u 0| : abs_nonneg (u 0)
       ... ≤ B     : hB 0,
  by_cases hB0 : B = 0,
  { subst hB0,
    intros ε hε,
    use 0,
    intros n hn,
    simp_rw [sub_zero] at *,
    calc |(u * v) n|
         = |u n| * |v n| : by finish [abs_mul]
     ... ≤ 0 * |v n|     : mul_le_mul_of_nonneg_right (hB n) (abs_nonneg (v n))
     ... = 0             : by ring
     ... < ε             : hε, },
  { change B ≠ 0 at hB0,
    have hBpos : 0 < B := (ne.le_iff_lt hB0.symm).mp hBnoneg,
    intros ε hε,
    cases hV (ε/B) (div_pos hε hBpos) with N hN,
    use N,
    intros n hn,
    simp_rw [sub_zero] at *,
    calc |(u * v) n|
         = |u n| * |v n|  : by finish [abs_mul]
     ... ≤ B * |v n|      : mul_le_mul_of_nonneg_right (hB n) (abs_nonneg _)
     ... < B * (ε/B)      : by finish
     ... = ε              : mul_div_cancel' ε hB0 },
end

import data.real.basic

import tactic

variables (u v : ℕ → ℝ)

variable (a : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

def acotada (a : ℕ → ℝ) :=

∃ B, ∀ n, |a n| ≤ B

-- 1ª demostración

example

(hU : acotada u)

(hV : limite v 0)

: limite (u*v) 0 :=

begin

cases hU with B hB,

have hBnoneg : 0 ≤ B,

calc 0 ≤ |u 0| : abs_nonneg (u 0)

... ≤ B : hB 0,

by_cases hB0 : B = 0,

{ subst hB0,

intros ε hε,

use 0,

intros n hn,

simp_rw [sub_zero] at *,

calc |(u * v) n|

= |u n * v n| : congr_arg abs (pi.mul_apply u v n)

... = |u n| * |v n| : abs_mul (u n) (v n)

... ≤ 0 * |v n| : mul_le_mul_of_nonneg_right (hB n) (abs_nonneg (v n))

... = 0 : zero_mul (|v n|)

... < ε : hε, },

{ change B ≠ 0 at hB0,

have hBpos : 0 < B := (ne.le_iff_lt hB0.symm).mp hBnoneg,

intros ε hε,

cases hV (ε/B) (div_pos hε hBpos) with N hN,

use N,

intros n hn,

simp_rw [sub_zero] at *,

calc |(u * v) n|

= |u n * v n| : congr_arg abs (pi.mul_apply u v n)

... = |u n| * |v n| : abs_mul (u n) (v n)

... ≤ B * |v n| : mul_le_mul_of_nonneg_right (hB n) (abs_nonneg _)

... < B * (ε/B) : mul_lt_mul_of_pos_left (hN n hn) hBpos

... = ε : mul_div_cancel' ε hB0 },

end

-- 2ª demostración

example

(hU : acotada u)

(hV : limite v 0)

: limite (u*v) 0 :=

begin

cases hU with B hB,

have hBnoneg : 0 ≤ B,

calc 0 ≤ |u 0| : abs_nonneg (u 0)

... ≤ B : hB 0,

by_cases hB0 : B = 0,

{ subst hB0,

intros ε hε,

use 0,

intros n hn,

simp_rw [sub_zero] at *,

calc |(u * v) n|

= |u n| * |v n| : by finish [abs_mul]

... ≤ 0 * |v n| : mul_le_mul_of_nonneg_right (hB n) (abs_nonneg (v n))

... = 0 : by ring

... < ε : hε, },

{ change B ≠ 0 at hB0,

have hBpos : 0 < B := (ne.le_iff_lt hB0.symm).mp hBnoneg,

intros ε hε,

cases hV (ε/B) (div_pos hε hBpos) with N hN,

use N,

intros n hn,

simp_rw [sub_zero] at *,

calc |(u * v) n|

= |u n| * |v n| : by finish [abs_mul]

... ≤ B * |v n| : mul_le_mul_of_nonneg_right (hB n) (abs_nonneg _)

... < B * (ε/B) : by finish

... = ε : mul_div_cancel' ε hB0 },

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Producto_de_una_sucesion_acotada_por_otra_convergente_a_cero
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

definition acotada :: "(nat ⇒ real) ⇒ bool"
  where "acotada u ⟷ (∃B. ∀n. ¦u n¦ ≤ B)"

lemma
  assumes "acotada u"
          "limite v 0"
  shows   "limite (λn. u n * v n) 0"
proof -
  obtain B where hB : "∀n. ¦u n¦ ≤ B"
    using assms(1) acotada_def by auto
  then have hBnoneg : "0 ≤ B" by auto
  show "limite (λn. u n * v n) 0"
  proof (cases "B = 0")
    assume "B = 0"
    show "limite (λn. u n * v n) 0"
    proof (unfold limite_def; intro allI impI)
      fix ε :: real
      assume "0 < ε"
      have "∀n≥0. ¦u n * v n - 0¦ < ε"
      proof (intro allI impI)
        fix n :: nat
        assume "n ≥ 0"
        show "¦u n * v n - 0¦ < ε"
          using ‹0 < ε› ‹B = 0› hB by auto
      qed
      then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε"
        by (rule exI)
    qed
  next
    assume "B ≠ 0"
    then have hBpos : "0 < B"
      using hBnoneg by auto
    show "limite (λn. u n * v n) 0"
    proof (unfold limite_def; intro allI impI)
      fix ε :: real
      assume "0 < ε"
      then have "0 < ε/B"
        by (simp add: hBpos)
      then obtain N where hN : "∀n≥N. ¦v n - 0¦ < ε/B"
        using assms(2) limite_def by auto
      have "∀n≥N. ¦u n * v n - 0¦ < ε"
      proof (intro allI impI)
        fix n :: nat
        assume "n ≥ N"
        have "¦v n¦ < ε/B"
          using ‹N ≤ n› hN by auto
        have "¦u n * v n - 0¦ = ¦u n¦ * ¦v n¦"
          by (simp add: abs_mult)
        also have "… ≤ B * ¦v n¦"
          by (simp add: hB mult_right_mono)
        also have "… < B * (ε/B)"
          using ‹¦v n¦ < ε/B› hBpos
          by (simp only: mult_strict_left_mono)
        also have "… = ε"
          using ‹B ≠ 0› by simp
        finally show "¦u n * v n - 0¦ < ε"
          by this
      qed
      then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε"
        by (rule exI)
    qed
  qed
qed

end

theory Producto_de_una_sucesion_acotada_por_otra_convergente_a_cero

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

definition acotada :: "(nat ⇒ real) ⇒ bool"

where "acotada u ⟷ (∃B. ∀n. ¦u n¦ ≤ B)"

lemma

assumes "acotada u"

"limite v 0"

shows "limite (λn. u n * v n) 0"

proof -

obtain B where hB : "∀n. ¦u n¦ ≤ B"

using assms(1) acotada_def by auto

then have hBnoneg : "0 ≤ B" by auto

show "limite (λn. u n * v n) 0"

proof (cases "B = 0")

assume "B = 0"

show "limite (λn. u n * v n) 0"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

have "∀n≥0. ¦u n * v n - 0¦ < ε"

proof (intro allI impI)

fix n :: nat

assume "n ≥ 0"

show "¦u n * v n - 0¦ < ε"

using ‹0 < ε› ‹B = 0› hB by auto

qed

then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε"

by (rule exI)

qed

assume "B ≠ 0"

then have hBpos : "0 < B"

using hBnoneg by auto

show "limite (λn. u n * v n) 0"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then have "0 < ε/B"

by (simp add: hBpos)

then obtain N where hN : "∀n≥N. ¦v n - 0¦ < ε/B"

using assms(2) limite_def by auto

have "∀n≥N. ¦u n * v n - 0¦ < ε"

proof (intro allI impI)

fix n :: nat

assume "n ≥ N"

have "¦v n¦ < ε/B"

using ‹N ≤ n› hN by auto

have "¦u n * v n - 0¦ = ¦u n¦ * ¦v n¦"

by (simp add: abs_mult)

also have "… ≤ B * ¦v n¦"

by (simp add: hB mult_right_mono)

also have "… < B * (ε/B)"

using ‹¦v n¦ < ε/B› hBpos

by (simp only: mult_strict_left_mono)

also have "… = ε"

using ‹B ≠ 0› by simp

finally show "¦u n * v n - 0¦ < ε"

by this

qed

then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε"

by (rule exI)

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las sucesiones acotadas por cero son nulas

PorJosé A. Alonso 31 julio 202129 julio 2021

Demostrar que las sucesiones acotadas por cero son nulas.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
import tactic

variable (u : ℕ → ℝ)

notation `|`x`|` := abs x

example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
sorry

import data.real.basic

import tactic

variable (u : ℕ → ℝ)

notation `|`x`|` := abs x

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

variable (u : ℕ → ℝ)

notation `|`x`|` := abs x

-- 1ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
begin
  intro n,
  rw ← abs_eq_zero,
  specialize h n,
  apply le_antisymm,
  { exact h, },
  { exact abs_nonneg (u n), },
end

-- 2ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
begin
  intro n,
  rw ← abs_eq_zero,
  specialize h n,
  exact le_antisymm h (abs_nonneg (u n)),
end

-- 3ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
begin
  intro n,
  rw ← abs_eq_zero,
  exact le_antisymm (h n) (abs_nonneg (u n)),
end

-- 4ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
begin
  intro n,
  exact abs_eq_zero.mp (le_antisymm (h n) (abs_nonneg (u n))),
end

-- 5ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
λ n, abs_eq_zero.mp (le_antisymm (h n) (abs_nonneg (u n)))

-- 6ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
by finish

import data.real.basic

import tactic

variable (u : ℕ → ℝ)

notation `|`x`|` := abs x

-- 1ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

begin

intro n,

rw ← abs_eq_zero,

specialize h n,

apply le_antisymm,

{ exact h, },

{ exact abs_nonneg (u n), },

end

-- 2ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

begin

intro n,

rw ← abs_eq_zero,

specialize h n,

exact le_antisymm h (abs_nonneg (u n)),

end

-- 3ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

begin

intro n,

rw ← abs_eq_zero,

exact le_antisymm (h n) (abs_nonneg (u n)),

end

-- 4ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

begin

intro n,

exact abs_eq_zero.mp (le_antisymm (h n) (abs_nonneg (u n))),

end

-- 5ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

λ n, abs_eq_zero.mp (le_antisymm (h n) (abs_nonneg (u n)))

-- 6ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

by finish

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Las_sucesiones_acotadas_por_cero_son_nulas
imports Main HOL.Real
begin

(* 1ª demostración *)
lemma
  fixes a :: "nat ⇒ real"
  assumes "∀n. ¦a n¦ ≤ 0"
  shows   "∀n. a n = 0"
proof (rule allI)
  fix n
  have "¦a n¦ = 0"
  proof (rule antisym)
    show "¦a n¦ ≤ 0"
      using assms by (rule allE)
  next
    show " 0 ≤ ¦a n¦"
      by (rule abs_ge_zero)
  qed
  then show "a n = 0"
    by (simp only: abs_eq_0_iff)
qed

(* 2ª demostración *)
lemma
  fixes a :: "nat ⇒ real"
  assumes "∀n. ¦a n¦ ≤ 0"
  shows   "∀n. a n = 0"
proof (rule allI)
  fix n
  have "¦a n¦ = 0"
  proof (rule antisym)
    show "¦a n¦ ≤ 0" try
      using assms by (rule allE)
  next
    show " 0 ≤ ¦a n¦"
      by simp
  qed
  then show "a n = 0"
    by simp
qed

(* 3ª demostración *)
lemma
  fixes a :: "nat ⇒ real"
  assumes "∀n. ¦a n¦ ≤ 0"
  shows   "∀n. a n = 0"
proof (rule allI)
  fix n
  have "¦a n¦ = 0"
    using assms by auto
  then show "a n = 0"
    by simp
qed

(* 4ª demostración *)
lemma
  fixes a :: "nat ⇒ real"
  assumes "∀n. ¦a n¦ ≤ 0"
  shows   "∀n. a n = 0"
using assms by auto

end

theory Las_sucesiones_acotadas_por_cero_son_nulas

imports Main HOL.Real

begin

(* 1ª demostración *)

lemma

fixes a :: "nat ⇒ real"

assumes "∀n. ¦a n¦ ≤ 0"

shows "∀n. a n = 0"

proof (rule allI)

fix n

have "¦a n¦ = 0"

proof (rule antisym)

show "¦a n¦ ≤ 0"

using assms by (rule allE)

show " 0 ≤ ¦a n¦"

by (rule abs_ge_zero)

qed

then show "a n = 0"

by (simp only: abs_eq_0_iff)

qed

(* 2ª demostración *)

lemma

fixes a :: "nat ⇒ real"

assumes "∀n. ¦a n¦ ≤ 0"

shows "∀n. a n = 0"

proof (rule allI)

fix n

have "¦a n¦ = 0"

proof (rule antisym)

show "¦a n¦ ≤ 0" try

using assms by (rule allE)

show " 0 ≤ ¦a n¦"

by simp

qed

then show "a n = 0"

by simp

qed

(* 3ª demostración *)

lemma

fixes a :: "nat ⇒ real"

assumes "∀n. ¦a n¦ ≤ 0"

shows "∀n. a n = 0"

proof (rule allI)

fix n

have "¦a n¦ = 0"

using assms by auto

then show "a n = 0"

by simp

qed

(* 4ª demostración *)

lemma

fixes a :: "nat ⇒ real"

assumes "∀n. ¦a n¦ ≤ 0"

shows "∀n. a n = 0"

using assms by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Límite de sucesión menor que otra sucesión

PorJosé A. Alonso 30 julio 202129 julio 2021

En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

Se define que a es el límite de la sucesión u, por

   def limite : (ℕ → ℝ) → ℝ → Prop :=
   λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

1 2	def limite : (ℕ → ℝ) → ℝ → Prop := λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, \|u n - a\| < ε

donde se usa la notación |x| para el valor absoluto de x

   notation `|`x`|` := abs x

1	notation `\|`x`\|` := abs x

Demostrar que si aₙ → l, bₙ → m y aₙ ≤ bₙ para todo n, entonces l ≤ m.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
import tactic

variables (u v : ℕ → ℝ)
variables (a c : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (c : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  (hu : limite u a)
  (hv : limite v c)
  (hle : ∀ n, u n ≤ v n)
  : a ≤ c :=
sorry

import data.real.basic

import tactic

variables (u v : ℕ → ℝ)

variables (a c : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example

(hu : limite u a)

(hv : limite v c)

(hle : ∀ n, u n ≤ v n)

: a ≤ c :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

variables (u v : ℕ → ℝ)
variables (a c : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (c : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

-- 1ª demostración
example
  (hu : limite u a)
  (hv : limite v c)
  (hle : ∀ n, u n ≤ v n)
  : a ≤ c :=
begin
  apply le_of_not_lt,
  intro hlt,
  set ε := (a - c) /2 with hεac,
  have hε : 0 < ε :=
    half_pos (sub_pos.mpr hlt),
  cases hu ε hε with Nu HNu,
  cases hv ε hε with Nv HNv,
  let N := max Nu Nv,
  have HNu' : Nu ≤ N := le_max_left Nu Nv,
  have HNv' : Nv ≤ N := le_max_right Nu Nv,
  have Ha : |u N - a| < ε := HNu N HNu',
  have Hc : |v N - c| < ε := HNv N HNv',
  have HN : u N ≤ v N := hle N,
  apply lt_irrefl (a - c),
  calc a - c
       = (a - u N) + (u N - c)   : by ring
   ... ≤ (a - u N) + (v N - c)   : by simp [HN]
   ... ≤ |(a - u N) + (v N - c)| : le_abs_self ((a - u N) + (v N - c))
   ... ≤ |a - u N| + |v N - c|   : abs_add (a - u N) (v N - c)
   ... = |u N - a| + |v N - c|   : by simp only [abs_sub]
   ... < ε + ε                   : add_lt_add Ha Hc
   ... = a - c                   : add_halves (a - c),
end

-- 2ª demostración
example
  (hu : limite u a)
  (hv : limite v c)
  (hle : ∀ n, u n ≤ v n)
  : a ≤ c :=
begin
  apply le_of_not_lt,
  intro hlt,
  set ε := (a - c) /2 with hε,
  cases hu ε (by linarith) with Nu HNu,
  cases hv ε (by linarith) with Nv HNv,
  let N := max Nu Nv,
  have Ha : |u N - a| < ε :=
    HNu N (le_max_left Nu Nv),
  have Hc : |v N - c| < ε :=
    HNv N (le_max_right Nu Nv),
  have HN : u N ≤ v N := hle N,
  apply lt_irrefl (a - c),
  calc a - c
       = (a - u N) + (u N - c)   : by ring
   ... ≤ (a - u N) + (v N - c)   : by simp [HN]
   ... ≤ |(a - u N) + (v N - c)| : le_abs_self ((a - u N) + (v N - c))
   ... ≤ |a - u N| + |v N - c|   : abs_add (a - u N) (v N - c)
   ... = |u N - a| + |v N - c|   : by simp only [abs_sub]
   ... < ε + ε                   : add_lt_add Ha Hc
   ... = a - c                   : add_halves (a - c),
end

-- 3ª demostración
example
  (hu : limite u a)
  (hv : limite v c)
  (hle : ∀ n, u n ≤ v n)
  : a ≤ c :=
begin
  apply le_of_not_lt,
  intro hlt,
  set ε := (a - c) /2 with hε,
  cases hu ε (by linarith) with Nu HNu,
  cases hv ε (by linarith) with Nv HNv,
  let N := max Nu Nv,
  have Ha : |u N - a| < ε :=
    HNu N (le_max_left Nu Nv),
  have Hc : |v N - c| < ε :=
    HNv N (le_max_right Nu Nv),
  have HN : u N ≤ v N := hle N,
  apply lt_irrefl (a - c),
  calc a - c
       = (a - u N) + (u N - c)   : by ring
   ... ≤ (a - u N) + (v N - c)   : by simp [HN]
   ... ≤ |(a - u N) + (v N - c)| : by simp [le_abs_self]
   ... ≤ |a - u N| + |v N - c|   : by simp [abs_add]
   ... = |u N - a| + |v N - c|   : by simp [abs_sub]
   ... < ε + ε                   : add_lt_add Ha Hc
   ... = a - c                   : by simp,
end

-- 4ª demostración
example
  (hu : limite u a)
  (hv : limite v c)
  (hle : ∀ n, u n ≤ v n)
  : a ≤ c :=
begin
  apply le_of_not_lt,
  intro hlt,
  set ε := (a - c) /2 with hε,
  cases hu ε (by linarith) with Nu HNu,
  cases hv ε (by linarith) with Nv HNv,
  let N := max Nu Nv,
  have Ha : |u N - a| < ε :=
    HNu N (le_max_left Nu Nv),
  have Hc : |v N - c| < ε :=
    HNv N (le_max_right Nu Nv),
  have HN : u N ≤ v N := hle N,
  apply lt_irrefl (a - c),
  rw abs_lt at Ha Hc,
  linarith,
end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

import data.real.basic

import tactic

variables (u v : ℕ → ℝ)

variables (a c : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

-- 1ª demostración

example

(hu : limite u a)

(hv : limite v c)

(hle : ∀ n, u n ≤ v n)

: a ≤ c :=

begin

apply le_of_not_lt,

intro hlt,

set ε := (a - c) /2 with hεac,

have hε : 0 < ε :=

half_pos (sub_pos.mpr hlt),

cases hu ε hε with Nu HNu,

cases hv ε hε with Nv HNv,

let N := max Nu Nv,

have HNu' : Nu ≤ N := le_max_left Nu Nv,

have HNv' : Nv ≤ N := le_max_right Nu Nv,

have Ha : |u N - a| < ε := HNu N HNu',

have Hc : |v N - c| < ε := HNv N HNv',

have HN : u N ≤ v N := hle N,

apply lt_irrefl (a - c),

calc a - c

= (a - u N) + (u N - c) : by ring

... ≤ (a - u N) + (v N - c) : by simp [HN]

... ≤ |(a - u N) + (v N - c)| : le_abs_self ((a - u N) + (v N - c))

... ≤ |a - u N| + |v N - c| : abs_add (a - u N) (v N - c)

... = |u N - a| + |v N - c| : by simp only [abs_sub]

... < ε + ε : add_lt_add Ha Hc

... = a - c : add_halves (a - c),

end

-- 2ª demostración

example

(hu : limite u a)

(hv : limite v c)

(hle : ∀ n, u n ≤ v n)

: a ≤ c :=

begin

apply le_of_not_lt,

intro hlt,

set ε := (a - c) /2 with hε,

cases hu ε (by linarith) with Nu HNu,

cases hv ε (by linarith) with Nv HNv,

let N := max Nu Nv,

have Ha : |u N - a| < ε :=

HNu N (le_max_left Nu Nv),

have Hc : |v N - c| < ε :=

HNv N (le_max_right Nu Nv),

have HN : u N ≤ v N := hle N,

apply lt_irrefl (a - c),

calc a - c

= (a - u N) + (u N - c) : by ring

... ≤ (a - u N) + (v N - c) : by simp [HN]

... ≤ |(a - u N) + (v N - c)| : le_abs_self ((a - u N) + (v N - c))

... ≤ |a - u N| + |v N - c| : abs_add (a - u N) (v N - c)

... = |u N - a| + |v N - c| : by simp only [abs_sub]

... < ε + ε : add_lt_add Ha Hc

... = a - c : add_halves (a - c),

end

-- 3ª demostración

example

(hu : limite u a)

(hv : limite v c)

(hle : ∀ n, u n ≤ v n)

: a ≤ c :=

begin

apply le_of_not_lt,

intro hlt,

set ε := (a - c) /2 with hε,

cases hu ε (by linarith) with Nu HNu,

cases hv ε (by linarith) with Nv HNv,

let N := max Nu Nv,

have Ha : |u N - a| < ε :=

HNu N (le_max_left Nu Nv),

have Hc : |v N - c| < ε :=

HNv N (le_max_right Nu Nv),

have HN : u N ≤ v N := hle N,

apply lt_irrefl (a - c),

calc a - c

= (a - u N) + (u N - c) : by ring

... ≤ (a - u N) + (v N - c) : by simp [HN]

... ≤ |(a - u N) + (v N - c)| : by simp [le_abs_self]

... ≤ |a - u N| + |v N - c| : by simp [abs_add]

... = |u N - a| + |v N - c| : by simp [abs_sub]

... < ε + ε : add_lt_add Ha Hc

... = a - c : by simp,

end

-- 4ª demostración

example

(hu : limite u a)

(hv : limite v c)

(hle : ∀ n, u n ≤ v n)

: a ≤ c :=

begin

apply le_of_not_lt,

intro hlt,

set ε := (a - c) /2 with hε,

cases hu ε (by linarith) with Nu HNu,

cases hv ε (by linarith) with Nv HNv,

let N := max Nu Nv,

have Ha : |u N - a| < ε :=

HNu N (le_max_left Nu Nv),

have Hc : |v N - c| < ε :=

HNv N (le_max_right Nu Nv),

have HN : u N ≤ v N := hle N,

apply lt_irrefl (a - c),

rw abs_lt at Ha Hc,

linarith,

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Limite_de_sucesion_menor_que_otra_sucesion
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

(* 1ª demostración *)
lemma
  assumes "limite u a"
          "limite v c"
          "∀n. u n ≤ v n"
  shows   "a ≤ c"
proof (rule leI ; intro notI)
  assume "c < a"
  let ?ε = "(a - c) /2"
  have "0 < ?ε"
    using ‹c < a› by simp
  obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"
    using assms(1) limite_def ‹0 < ?ε› by blast
  obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"
    using assms(2) limite_def ‹0 < ?ε› by blast
  let ?N = "max Nu Nv"
  have "?N ≥ Nu"
    by simp
  then have Ha : "¦u ?N - a¦ < ?ε"
    using HNu by simp
  have "?N ≥ Nv"
    by simp
  then have Hc : "¦v ?N - c¦ < ?ε"
    using HNv by simp
  have "a - c < a - c"
  proof -
    have "a - c = (a - u ?N) + (u ?N - c)"
      by simp
    also have "… ≤ (a - u ?N) + (v ?N - c)"
      using assms(3) by auto
    also have "… ≤ ¦(a - u ?N) + (v ?N - c)¦"
      by (rule abs_ge_self)
    also have "… ≤ ¦a - u ?N¦ + ¦v ?N - c¦"
      by (rule abs_triangle_ineq)
    also have "… = ¦u ?N - a¦ + ¦v ?N - c¦"
      by (simp only: abs_minus_commute)
    also have "… < ?ε + ?ε"
      using Ha Hc by (simp only: add_strict_mono)
    also have "… = a - c"
      by (rule field_sum_of_halves)
    finally show "a - c < a - c"
      by this
  qed
  have "¬ a - c < a - c"
    by (rule less_irrefl)
  then show False
    using ‹a - c < a - c› by (rule notE)
qed

(* 2ª demostración *)
lemma
  assumes "limite u a"
          "limite v c"
          "∀n. u n ≤ v n"
  shows   "a ≤ c"
proof (rule leI ; intro notI)
  assume "c < a"
  let ?ε = "(a - c) /2"
  have "0 < ?ε"
    using ‹c < a› by simp
  obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"
    using assms(1) limite_def ‹0 < ?ε› by blast
  obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"
    using assms(2) limite_def ‹0 < ?ε› by blast
  let ?N = "max Nu Nv"
  have "?N ≥ Nu"
    by simp
  then have Ha : "¦u ?N - a¦ < ?ε"
    using HNu by simp
  then have Ha' : "u ?N - a < ?ε ∧ -(u ?N - a) < ?ε"
    by argo
  have "?N ≥ Nv"
    by simp
  then have Hc : "¦v ?N - c¦ < ?ε"
    using HNv by simp
  then have Hc' : "v ?N - c < ?ε ∧ -(v ?N - c) < ?ε"
    by argo
  have "a - c < a - c"
    using assms(3) Ha' Hc'
    by (smt (verit, best) field_sum_of_halves)
  have "¬ a - c < a - c"
    by simp
  then show False
    using ‹a - c < a - c› by simp
qed

(* 3ª demostración *)
lemma
  assumes "limite u a"
          "limite v c"
          "∀n. u n ≤ v n"
  shows   "a ≤ c"
proof (rule leI ; intro notI)
  assume "c < a"
  let ?ε = "(a - c) /2"
  have "0 < ?ε"
    using ‹c < a› by simp
  obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"
    using assms(1) limite_def ‹0 < ?ε› by blast
  obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"
    using assms(2) limite_def ‹0 < ?ε› by blast
  let ?N = "max Nu Nv"
  have "?N ≥ Nu"
    by simp
  then have Ha : "¦u ?N - a¦ < ?ε"
    using HNu by simp
  then have Ha' : "u ?N - a < ?ε ∧ -(u ?N - a) < ?ε"
    by argo
  have "?N ≥ Nv"
    by simp
  then have Hc : "¦v ?N - c¦ < ?ε"
    using HNv by simp
  then have Hc' : "v ?N - c < ?ε ∧ -(v ?N - c) < ?ε"
    by argo
  show False
    using assms(3) Ha' Hc'
    by (smt (verit, best) field_sum_of_halves)
qed

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

theory Limite_de_sucesion_menor_que_otra_sucesion

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

(* 1ª demostración *)

lemma

assumes "limite u a"

"limite v c"

"∀n. u n ≤ v n"

shows "a ≤ c"

proof (rule leI ; intro notI)

assume "c < a"

let ?ε = "(a - c) /2"

have "0 < ?ε"

using ‹c < a› by simp

obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"

using assms(1) limite_def ‹0 < ?ε› by blast

obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"

using assms(2) limite_def ‹0 < ?ε› by blast

let ?N = "max Nu Nv"

have "?N ≥ Nu"

by simp

then have Ha : "¦u ?N - a¦ < ?ε"

using HNu by simp

have "?N ≥ Nv"

by simp

then have Hc : "¦v ?N - c¦ < ?ε"

using HNv by simp

have "a - c < a - c"

proof -

have "a - c = (a - u ?N) + (u ?N - c)"

by simp

also have "… ≤ (a - u ?N) + (v ?N - c)"

using assms(3) by auto

also have "… ≤ ¦(a - u ?N) + (v ?N - c)¦"

by (rule abs_ge_self)

also have "… ≤ ¦a - u ?N¦ + ¦v ?N - c¦"

by (rule abs_triangle_ineq)

also have "… = ¦u ?N - a¦ + ¦v ?N - c¦"

by (simp only: abs_minus_commute)

also have "… < ?ε + ?ε"

using Ha Hc by (simp only: add_strict_mono)

also have "… = a - c"

by (rule field_sum_of_halves)

finally show "a - c < a - c"

by this

qed

have "¬ a - c < a - c"

by (rule less_irrefl)

then show False

using ‹a - c < a - c› by (rule notE)

qed

(* 2ª demostración *)

lemma

assumes "limite u a"

"limite v c"

"∀n. u n ≤ v n"

shows "a ≤ c"

proof (rule leI ; intro notI)

assume "c < a"

let ?ε = "(a - c) /2"

have "0 < ?ε"

using ‹c < a› by simp

obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"

using assms(1) limite_def ‹0 < ?ε› by blast

obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"

using assms(2) limite_def ‹0 < ?ε› by blast

let ?N = "max Nu Nv"

have "?N ≥ Nu"

by simp

then have Ha : "¦u ?N - a¦ < ?ε"

using HNu by simp

then have Ha' : "u ?N - a < ?ε ∧ -(u ?N - a) < ?ε"

by argo

have "?N ≥ Nv"

by simp

then have Hc : "¦v ?N - c¦ < ?ε"

using HNv by simp

then have Hc' : "v ?N - c < ?ε ∧ -(v ?N - c) < ?ε"

by argo

have "a - c < a - c"

using assms(3) Ha' Hc'

by (smt (verit, best) field_sum_of_halves)

have "¬ a - c < a - c"

by simp

then show False

using ‹a - c < a - c› by simp

qed

(* 3ª demostración *)

lemma

assumes "limite u a"

"limite v c"

"∀n. u n ≤ v n"

shows "a ≤ c"

proof (rule leI ; intro notI)

assume "c < a"

let ?ε = "(a - c) /2"

have "0 < ?ε"

using ‹c < a› by simp

obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"

using assms(1) limite_def ‹0 < ?ε› by blast

obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"

using assms(2) limite_def ‹0 < ?ε› by blast

let ?N = "max Nu Nv"

have "?N ≥ Nu"

by simp

then have Ha : "¦u ?N - a¦ < ?ε"

using HNu by simp

then have Ha' : "u ?N - a < ?ε ∧ -(u ?N - a) < ?ε"

by argo

have "?N ≥ Nv"

by simp

then have Hc : "¦v ?N - c¦ < ?ε"

using HNv by simp

then have Hc' : "v ?N - c < ?ε ∧ -(v ?N - c) < ?ε"

by argo

show False

using assms(3) Ha' Hc'

by (smt (verit, best) field_sum_of_halves)

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Propiedad cancelativa del producto de números naturales

PorJosé A. Alonso 28 julio 2021

Sean k, m, n números naturales. Demostrar que

   k * m = k * n ↔ m = n ∨ k = 0

1	k * m = k * n ↔ m = n ∨ k = 0

Para ello, completar la siguiente teoría de Lean:

import data.nat.basic
open nat

variables {k m n : ℕ}

example :
  k * m = k * n ↔ m = n ∨ k = 0 :=
sorry

import data.nat.basic

open nat

variables {k m n : ℕ}

example :

k * m = k * n ↔ m = n ∨ k = 0 :=

sorry

[expand title=»Soluciones con Lean»]

import data.nat.basic
open nat

variables {k m n : ℕ}

-- Para que no use la notación con puntos
set_option pp.structure_projections false

-- 1ª demostración
example :
  k * m = k * n ↔ m = n ∨ k = 0 :=
begin
  have h1: k ≠ 0 → k * m = k * n → m = n,
    { induction n with n HI generalizing m,
      { by finish, },
      { cases m,
        { by finish, },
        { intros hk hS,
          congr,
          apply HI hk,
          rw mul_succ at hS,
          rw mul_succ at hS,
          exact add_right_cancel hS, }}},
  by finish,
end

-- 2ª demostración
example :
  k * m = k * n ↔ m = n ∨ k = 0 :=
begin
  have h1: k ≠ 0 → k * m = k * n → m = n,
    { induction n with n HI generalizing m,
      { by finish, },
      { cases m,
        { by finish, },
        { intros hk hS,
          congr,
          apply HI hk,
          simp only [mul_succ] at hS,
          exact add_right_cancel hS, }}},
  by finish,
end

-- 3ª demostración
example :
  k * m = k * n ↔ m = n ∨ k = 0 :=
begin
  have h1: k ≠ 0 → k * m = k * n → m = n,
    { induction n with n HI generalizing m,
      { by finish, },
      { cases m,
        { by finish, },
        { by finish, }}},
  by finish,
end

-- 4ª demostración
example :
  k * m = k * n ↔ m = n ∨ k = 0 :=
begin
  have h1: k ≠ 0 → k * m = k * n → m = n,
    { induction n with n HI generalizing m,
      { by finish, },
      { cases m; by finish }},
  by finish,
end

-- 5ª demostración
example :
  k * m = k * n ↔ m = n ∨ k = 0 :=
begin
  have h1: k ≠ 0 → k * m = k * n → m = n,
    { induction n with n HI generalizing m ; by finish },
  by finish,
end

-- 5ª demostración
example :
  k * m = k * n ↔ m = n ∨ k = 0 :=
begin
  by_cases hk : k = 0,
  { by simp, },
  { rw mul_right_inj' hk,
    by tauto, },
end

-- 6ª demostración
example :
  k * m = k * n ↔ m = n ∨ k = 0 :=
mul_eq_mul_left_iff

-- 7ª demostración
example :
  k * m = k * n ↔ m = n ∨ k = 0 :=
by simp

import data.nat.basic

open nat

variables {k m n : ℕ}

-- Para que no use la notación con puntos

set_option pp.structure_projections false

-- 1ª demostración

example :

k * m = k * n ↔ m = n ∨ k = 0 :=

begin

have h1: k ≠ 0 → k * m = k * n → m = n,

{ induction n with n HI generalizing m,

{ by finish, },

{ cases m,

{ by finish, },

{ intros hk hS,

congr,

apply HI hk,

rw mul_succ at hS,

exact add_right_cancel hS, }}},

by finish,

end

-- 2ª demostración

example :

k * m = k * n ↔ m = n ∨ k = 0 :=

begin

have h1: k ≠ 0 → k * m = k * n → m = n,

{ induction n with n HI generalizing m,

{ by finish, },

{ cases m,

{ by finish, },

{ intros hk hS,

congr,

apply HI hk,

simp only [mul_succ] at hS,

exact add_right_cancel hS, }}},

by finish,

end

-- 3ª demostración

example :

k * m = k * n ↔ m = n ∨ k = 0 :=

begin

have h1: k ≠ 0 → k * m = k * n → m = n,

{ induction n with n HI generalizing m,

{ by finish, },

{ cases m,

{ by finish, },

{ by finish, }}},

by finish,

end

-- 4ª demostración

example :

k * m = k * n ↔ m = n ∨ k = 0 :=

begin

have h1: k ≠ 0 → k * m = k * n → m = n,

{ induction n with n HI generalizing m,

{ by finish, },

{ cases m; by finish }},

by finish,

end

-- 5ª demostración

example :

k * m = k * n ↔ m = n ∨ k = 0 :=

begin

have h1: k ≠ 0 → k * m = k * n → m = n,

{ induction n with n HI generalizing m ; by finish },

by finish,

end

-- 5ª demostración

example :

k * m = k * n ↔ m = n ∨ k = 0 :=

begin

by_cases hk : k = 0,

{ by simp, },

{ rw mul_right_inj' hk,

by tauto, },

end

-- 6ª demostración

example :

k * m = k * n ↔ m = n ∨ k = 0 :=

mul_eq_mul_left_iff

-- 7ª demostración

example :

k * m = k * n ↔ m = n ∨ k = 0 :=

by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Propiedad_cancelativa_del_producto_de_numeros_naturales
imports Main
begin

(* 1ª demostración *)
lemma
  fixes k m n :: nat
  shows "k * m = k * n ⟷ m = n ∨ k = 0"
proof -
  have "k ≠ 0 ⟹ k * m = k * n ⟹ m = n"
  proof (induct n arbitrary: m)
    fix m
    assume "k ≠ 0" and "k * m = k * 0"
    show "m = 0"
      using ‹k * m = k * 0›
      by (simp only: mult_left_cancel[OF ‹k ≠ 0›])
  next
    fix n m
    assume HI : "⋀m. ⟦k ≠ 0; k * m = k * n⟧ ⟹ m = n"
       and hk : "k ≠ 0"
       and "k * m = k * Suc n"
    then show "m = Suc n"
    proof (cases m)
      assume "m = 0"
      then show "m = Suc n"
        using ‹k * m = k * Suc n›
        by (simp only: mult_left_cancel[OF ‹k ≠ 0›])
    next
      fix m'
      assume "m = Suc m'"
      then have "k * Suc m' = k * Suc n"
        using ‹k * m = k * Suc n› by (rule subst)
      then have "k * m' + k = k * n + k"
        by (simp only: mult_Suc_right)
      then have "k * m' = k * n"
        by (simp only: add_right_imp_eq)
      then have "m' = n"
        by (simp only: HI[OF hk])
      then show "m = Suc n"
        by (simp only: ‹m = Suc m'›)
    qed
  qed
  then show "k * m = k * n ⟷ m = n ∨ k = 0"
    by auto
qed

(* 2ª demostración *)
lemma
  fixes k m n :: nat
  shows "k * m = k * n ⟷ m = n ∨ k = 0"
proof -
  have "k ≠ 0 ⟹ k * m = k * n ⟹ m = n"
  proof (induct n arbitrary: m)
    fix m
    assume "k ≠ 0" and "k * m = k * 0"
    then show "m = 0" by simp
  next
    fix n m
    assume "⋀m. ⟦k ≠ 0; k * m = k * n⟧ ⟹ m = n"
       and "k ≠ 0"
       and "k * m = k * Suc n"
    then show "m = Suc n"
    proof (cases m)
      assume "m = 0"
      then show "m = Suc n"
        using ‹k * m = k * Suc n› ‹k ≠ 0› by auto
    next
      fix m'
      assume "m = Suc m'"
      then show "m = Suc n"
        using ‹k * m = k * Suc n› ‹k ≠ 0› by force
    qed
  qed
  then show "k * m = k * n ⟷ m = n ∨ k = 0" by auto
qed

(* 3ª demostración *)
lemma
  fixes k m n :: nat
  shows "k * m = k * n ⟷ m = n ∨ k = 0"
proof -
  have "k ≠ 0 ⟹ k * m = k * n ⟹ m = n"
  proof (induct n arbitrary: m)
    case 0
    then show ?case
      by simp
  next
    case (Suc n)
    then show ?case
    proof (cases m)
      case 0
      then show ?thesis
        using Suc.prems by auto
    next
      case (Suc nat)
      then show ?thesis
        using Suc.prems by auto
    qed
  qed
  then show ?thesis
    by auto
qed

(* 4ª demostración *)
lemma
  fixes k m n :: nat
  shows "k * m = k * n ⟷ m = n ∨ k = 0"
proof -
  have "k ≠ 0 ⟹ k * m = k * n ⟹ m = n"
  proof (induct n arbitrary: m)
    case 0
    then show "m = 0" by simp
  next
    case (Suc n)
    then show "m = Suc n"
      by (cases m) (simp_all add: eq_commute [of 0])
  qed
  then show ?thesis by auto
qed

(* 5ª demostración *)
lemma
  fixes k m n :: nat
  shows "k * m = k * n ⟷ m = n ∨ k = 0"
by (simp only: mult_cancel1)

(* 6ª demostración *)
lemma
  fixes k m n :: nat
  shows "k * m = k * n ⟷ m = n ∨ k = 0"
by simp

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

theory Propiedad_cancelativa_del_producto_de_numeros_naturales

imports Main

begin

(* 1ª demostración *)

lemma

fixes k m n :: nat

shows "k * m = k * n ⟷ m = n ∨ k = 0"

proof -

have "k ≠ 0 ⟹ k * m = k * n ⟹ m = n"

proof (induct n arbitrary: m)

fix m

assume "k ≠ 0" and "k * m = k * 0"

show "m = 0"

using ‹k * m = k * 0›

by (simp only: mult_left_cancel[OF ‹k ≠ 0›])

fix n m

assume HI : "⋀m. ⟦k ≠ 0; k * m = k * n⟧ ⟹ m = n"

and hk : "k ≠ 0"

and "k * m = k * Suc n"

then show "m = Suc n"

proof (cases m)

assume "m = 0"

then show "m = Suc n"

using ‹k * m = k * Suc n›

by (simp only: mult_left_cancel[OF ‹k ≠ 0›])

fix m'

assume "m = Suc m'"

then have "k * Suc m' = k * Suc n"

using ‹k * m = k * Suc n› by (rule subst)

then have "k * m' + k = k * n + k"

by (simp only: mult_Suc_right)

then have "k * m' = k * n"

by (simp only: add_right_imp_eq)

then have "m' = n"

by (simp only: HI[OF hk])

then show "m = Suc n"

by (simp only: ‹m = Suc m'›)

qed

then show "k * m = k * n ⟷ m = n ∨ k = 0"

by auto

qed

(* 2ª demostración *)

lemma

fixes k m n :: nat

shows "k * m = k * n ⟷ m = n ∨ k = 0"

proof -

have "k ≠ 0 ⟹ k * m = k * n ⟹ m = n"

proof (induct n arbitrary: m)

fix m

assume "k ≠ 0" and "k * m = k * 0"

then show "m = 0" by simp

fix n m

assume "⋀m. ⟦k ≠ 0; k * m = k * n⟧ ⟹ m = n"

and "k ≠ 0"

and "k * m = k * Suc n"

then show "m = Suc n"

proof (cases m)

assume "m = 0"

then show "m = Suc n"

using ‹k * m = k * Suc n› ‹k ≠ 0› by auto

fix m'

assume "m = Suc m'"

then show "m = Suc n"

using ‹k * m = k * Suc n› ‹k ≠ 0› by force

qed

then show "k * m = k * n ⟷ m = n ∨ k = 0" by auto

qed

(* 3ª demostración *)

lemma

fixes k m n :: nat

shows "k * m = k * n ⟷ m = n ∨ k = 0"

proof -

have "k ≠ 0 ⟹ k * m = k * n ⟹ m = n"

proof (induct n arbitrary: m)

case 0

then show ?case

by simp

case (Suc n)

then show ?case

proof (cases m)

case 0

then show ?thesis

using Suc.prems by auto

case (Suc nat)

then show ?thesis

using Suc.prems by auto

qed

then show ?thesis

by auto

qed

(* 4ª demostración *)

lemma

fixes k m n :: nat

shows "k * m = k * n ⟷ m = n ∨ k = 0"

proof -

have "k ≠ 0 ⟹ k * m = k * n ⟹ m = n"

proof (induct n arbitrary: m)

case 0

then show "m = 0" by simp

case (Suc n)

then show "m = Suc n"

by (cases m) (simp_all add: eq_commute [of 0])

qed

then show ?thesis by auto

qed

(* 5ª demostración *)

lemma

fixes k m n :: nat

shows "k * m = k * n ⟷ m = n ∨ k = 0"

by (simp only: mult_cancel1)

(* 6ª demostración *)

lemma

fixes k m n :: nat

shows "k * m = k * n ⟷ m = n ∨ k = 0"

by simp

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Propiedad de la densidad de los reales

PorJosé A. Alonso 27 julio 202127 julio 2021

Sean x, y números reales tales que

   ∀ z, y < z → x ≤ z

1	∀ z, y < z → x ≤ z

Demostrar que x ≤ y.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic

variables {x y : ℝ}

example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
sorry

import data.real.basic

variables {x y : ℝ}

example

(h : ∀ z, y < z → x ≤ z) :

x ≤ y :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variables {x y : ℝ}

-- 1ª demostración
example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
begin
  apply le_of_not_gt,
  intro hxy,
  cases (exists_between hxy) with a ha,
  apply (lt_irrefl a),
  calc a
       < x : ha.2
   ... ≤ a : h a ha.1,
end

-- 2ª demostración
example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
begin
  apply le_of_not_gt,
  intro hxy,
  cases (exists_between hxy) with a ha,
  apply (lt_irrefl a),
  exact lt_of_lt_of_le ha.2 (h a ha.1),
end

-- 3ª demostración
example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
begin
  apply le_of_not_gt,
  intro hxy,
  cases (exists_between hxy) with a ha,
  exact (lt_irrefl a) (lt_of_lt_of_le ha.2 (h a ha.1)),
end

-- 3ª demostración
example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
begin
  apply le_of_not_gt,
  intro hxy,
  rcases (exists_between hxy) with ⟨a, ha⟩,
  exact (lt_irrefl a) (lt_of_lt_of_le ha.2 (h a ha.1)),
end

-- 4ª demostración
example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
begin
  apply le_of_not_gt,
  intro hxy,
  rcases (exists_between hxy) with ⟨a, hya, hax⟩,
  exact (lt_irrefl a) (lt_of_lt_of_le hax (h a hya)),
end

-- 5ª demostración
example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
le_of_not_gt (λ hxy,
  let ⟨a, hya, hax⟩ := exists_between hxy in
  lt_irrefl a (lt_of_lt_of_le hax (h a hya)))

-- 6ª demostración
example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
le_of_forall_le_of_dense h

import data.real.basic

variables {x y : ℝ}

-- 1ª demostración

example

(h : ∀ z, y < z → x ≤ z) :

x ≤ y :=

begin

apply le_of_not_gt,

intro hxy,

cases (exists_between hxy) with a ha,

apply (lt_irrefl a),

calc a

< x : ha.2

... ≤ a : h a ha.1,

end

-- 2ª demostración

example

(h : ∀ z, y < z → x ≤ z) :

x ≤ y :=

begin

apply le_of_not_gt,

intro hxy,

cases (exists_between hxy) with a ha,

apply (lt_irrefl a),

exact lt_of_lt_of_le ha.2 (h a ha.1),

end

-- 3ª demostración

example

(h : ∀ z, y < z → x ≤ z) :

x ≤ y :=

begin

apply le_of_not_gt,

intro hxy,

cases (exists_between hxy) with a ha,

exact (lt_irrefl a) (lt_of_lt_of_le ha.2 (h a ha.1)),

end

-- 3ª demostración

example

(h : ∀ z, y < z → x ≤ z) :

x ≤ y :=

begin

apply le_of_not_gt,

intro hxy,

rcases (exists_between hxy) with ⟨a, ha⟩,

exact (lt_irrefl a) (lt_of_lt_of_le ha.2 (h a ha.1)),

end

-- 4ª demostración

example

(h : ∀ z, y < z → x ≤ z) :

x ≤ y :=

begin

apply le_of_not_gt,

intro hxy,

rcases (exists_between hxy) with ⟨a, hya, hax⟩,

exact (lt_irrefl a) (lt_of_lt_of_le hax (h a hya)),

end

-- 5ª demostración

example

(h : ∀ z, y < z → x ≤ z) :

x ≤ y :=

le_of_not_gt (λ hxy,

let ⟨a, hya, hax⟩ := exists_between hxy in

lt_irrefl a (lt_of_lt_of_le hax (h a hya)))

-- 6ª demostración

example

(h : ∀ z, y < z → x ≤ z) :

x ≤ y :=

le_of_forall_le_of_dense h

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Propiedad_de_la_densidad_de_los_reales
imports Main HOL.Real
begin

(* 1ª demostración *)
lemma
  fixes x y :: real
  assumes "∀ z. y < z ⟶ x ≤ z"
  shows "x ≤ y"
proof (rule linorder_class.leI; intro notI)
  assume "y < x"
  then have "∃z. y < z ∧ z < x"
    by (rule dense)
  then obtain a where ha : "y < a ∧ a < x"
    by (rule exE)
  have "¬ a < a"
    by (rule order.irrefl)
  moreover
  have "a < a"
  proof -
    have "y < a ⟶ x ≤ a"
      using assms by (rule allE)
    moreover
    have "y < a"
      using ha by (rule conjunct1)
    ultimately have "x ≤ a"
      by (rule mp)
    moreover
    have "a < x"
      using ha by (rule conjunct2)
    ultimately show "a < a"
      by (simp only: less_le_trans)
  qed
  ultimately show False
    by (rule notE)
qed

(* 2ª demostración *)
lemma
  fixes x y :: real
  assumes "⋀ z. y < z ⟹ x ≤ z"
  shows "x ≤ y"
proof (rule linorder_class.leI; intro notI)
  assume "y < x"
  then have "∃z. y < z ∧ z < x"
    by (rule dense)
  then obtain a where hya : "y < a" and hax : "a < x"
    by auto
  have "¬ a < a"
    by (rule order.irrefl)
  moreover
  have "a < a"
  proof -
    have "a < x"
      using hax .
    also have "… ≤ a"
      using assms[OF hya] .
    finally show "a < a" .
  qed
  ultimately show False
    by (rule notE)
qed

(* 3ª demostración *)
lemma
  fixes x y :: real
  assumes "⋀ z. y < z ⟹ x ≤ z"
  shows "x ≤ y"
proof (rule linorder_class.leI; intro notI)
  assume "y < x"
  then have "∃z. y < z ∧ z < x"
    by (rule dense)
  then obtain a where hya : "y < a" and hax : "a < x"
    by auto
  have "¬ a < a"
    by (rule order.irrefl)
  moreover
  have "a < a"
    using hax assms[OF hya] by (rule less_le_trans)
  ultimately show False
    by (rule notE)
qed

(* 4ª demostración *)
lemma
  fixes x y :: real
  assumes "⋀ z. y < z ⟹ x ≤ z"
  shows "x ≤ y"
by (meson assms dense not_less)

(* 5ª demostración *)
lemma
  fixes x y :: real
  assumes "⋀ z. y < z ⟹ x ≤ z"
  shows "x ≤ y"
using assms by (rule dense_ge)

(* 6ª demostración *)
lemma
  fixes x y :: real
  assumes "∀ z. y < z ⟶ x ≤ z"
  shows "x ≤ y"
using assms by (simp only: dense_ge)

end

100

101

102

103

104

105

theory Propiedad_de_la_densidad_de_los_reales

imports Main HOL.Real

begin

(* 1ª demostración *)

lemma

fixes x y :: real

assumes "∀ z. y < z ⟶ x ≤ z"

shows "x ≤ y"

proof (rule linorder_class.leI; intro notI)

assume "y < x"

then have "∃z. y < z ∧ z < x"

by (rule dense)

then obtain a where ha : "y < a ∧ a < x"

by (rule exE)

have "¬ a < a"

by (rule order.irrefl)

moreover

have "a < a"

proof -

have "y < a ⟶ x ≤ a"

using assms by (rule allE)

moreover

have "y < a"

using ha by (rule conjunct1)

ultimately have "x ≤ a"

by (rule mp)

moreover

have "a < x"

using ha by (rule conjunct2)

ultimately show "a < a"

by (simp only: less_le_trans)

qed

ultimately show False

by (rule notE)

qed

(* 2ª demostración *)

lemma

fixes x y :: real

assumes "⋀ z. y < z ⟹ x ≤ z"

shows "x ≤ y"

proof (rule linorder_class.leI; intro notI)

assume "y < x"

then have "∃z. y < z ∧ z < x"

by (rule dense)

then obtain a where hya : "y < a" and hax : "a < x"

by auto

have "¬ a < a"

by (rule order.irrefl)

moreover

have "a < a"

proof -

have "a < x"

using hax .

also have "… ≤ a"

using assms[OF hya] .

finally show "a < a" .

qed

ultimately show False

by (rule notE)

qed

(* 3ª demostración *)

lemma

fixes x y :: real

assumes "⋀ z. y < z ⟹ x ≤ z"

shows "x ≤ y"

proof (rule linorder_class.leI; intro notI)

assume "y < x"

then have "∃z. y < z ∧ z < x"

by (rule dense)

then obtain a where hya : "y < a" and hax : "a < x"

by auto

have "¬ a < a"

by (rule order.irrefl)

moreover

have "a < a"

using hax assms[OF hya] by (rule less_le_trans)

ultimately show False

by (rule notE)

qed

(* 4ª demostración *)

lemma

fixes x y :: real

assumes "⋀ z. y < z ⟹ x ≤ z"

shows "x ≤ y"

by (meson assms dense not_less)

(* 5ª demostración *)

lemma

fixes x y :: real

assumes "⋀ z. y < z ⟹ x ≤ z"

shows "x ≤ y"

using assms by (rule dense_ge)

(* 6ª demostración *)

lemma

fixes x y :: real

assumes "∀ z. y < z ⟶ x ≤ z"

shows "x ≤ y"

using assms by (simp only: dense_ge)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La paradoja del barbero

PorJosé A. Alonso 26 julio 202125 julio 2021

Demostrar la paradoja del barbero; es decir, que no existe un hombre que afeite a todos los que no se afeitan a sí mismo y sólo a los que no se afeitan a sí mismo.

Para ello, completar la siguiente teoría de Lean:

import tactic

variable (Hombre : Type)
variable (afeita : Hombre → Hombre → Prop)

example :
  ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=
sorry

import tactic

variable (Hombre : Type)

variable (afeita : Hombre → Hombre → Prop)

example :

¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable (Hombre : Type)
variable (afeita : Hombre → Hombre → Prop)

-- 1ª demostración
example :
  ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=
begin
  intro h,
  cases h with b hb,
  specialize hb b,
  by_cases (afeita b b),
  { apply absurd h,
    exact hb.mp h, },
  { apply h,
    exact hb.mpr h, },
end

-- 2ª demostración
example :
  ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=
begin
  intro h,
  cases h with b hb,
  specialize hb b,
  by_cases (afeita b b),
  { exact (hb.mp h) h, },
  { exact h (hb.mpr h), },
end

-- 3ª demostración
example :
  ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=
begin
  intro h,
  cases h with b hb,
  specialize hb b,
  by itauto,
end

-- 4ª demostración
example :
  ¬ (∃ x : Hombre,  ∀ y : Hombre, afeita x y ↔ ¬ afeita y y ) :=
begin
  rintro ⟨b, hb⟩,
  exact (iff_not_self (afeita b b)).mp (hb b),
end

-- 5ª demostración
example :
  ¬ (∃ x : Hombre,  ∀ y : Hombre, afeita x y ↔ ¬ afeita y y ) :=
λ ⟨b, hb⟩, (iff_not_self (afeita b b)).mp (hb b)

import tactic

variable (Hombre : Type)

variable (afeita : Hombre → Hombre → Prop)

-- 1ª demostración

example :

¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=

begin

intro h,

cases h with b hb,

specialize hb b,

by_cases (afeita b b),

{ apply absurd h,

exact hb.mp h, },

{ apply h,

exact hb.mpr h, },

end

-- 2ª demostración

example :

¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=

begin

intro h,

cases h with b hb,

specialize hb b,

by_cases (afeita b b),

{ exact (hb.mp h) h, },

{ exact h (hb.mpr h), },

end

-- 3ª demostración

example :

¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=

begin

intro h,

cases h with b hb,

specialize hb b,

by itauto,

end

-- 4ª demostración

example :

¬ (∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y ) :=

begin

rintro ⟨b, hb⟩,

exact (iff_not_self (afeita b b)).mp (hb b),

end

-- 5ª demostración

example :

¬ (∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y ) :=

λ ⟨b, hb⟩, (iff_not_self (afeita b b)).mp (hb b)

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory La_paradoja_del_barbero
imports Main
begin

(* 1ª demostración *)
lemma
  "¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)"
proof (rule notI)
  assume "∃ x. ∀ y. afeita x y ⟷ ¬ afeita y y"
  then obtain b where "∀ y. afeita b y ⟷ ¬ afeita y y"
    by (rule exE)
  then have h : "afeita b b ⟷ ¬ afeita b b"
    by (rule allE)
  show False
  proof (cases "afeita b b")
    assume "afeita b b"
    then have "¬ afeita b b"
      using h by (rule rev_iffD1)
    then show False
      using ‹afeita b b› by (rule notE)
  next
    assume "¬ afeita b b"
    then have "afeita b b"
      using h by (rule rev_iffD2)
    with ‹¬ afeita b b› show False
      by (rule notE)
  qed
qed

(* 2ª demostración *)
lemma
  "¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)"
proof
  assume "∃ x. ∀ y. afeita x y ⟷ ¬ afeita y y"
  then obtain b where "∀ y. afeita b y ⟷ ¬ afeita y y"
    by (rule exE)
  then have h : "afeita b b ⟷ ¬ afeita b b"
    by (rule allE)
  then show False
    by simp
qed

(* 3ª demostración *)
lemma
  "¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)"
  by auto

end

theory La_paradoja_del_barbero

imports Main

begin

(* 1ª demostración *)

lemma

"¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)"

proof (rule notI)

assume "∃ x. ∀ y. afeita x y ⟷ ¬ afeita y y"

then obtain b where "∀ y. afeita b y ⟷ ¬ afeita y y"

by (rule exE)

then have h : "afeita b b ⟷ ¬ afeita b b"

by (rule allE)

show False

proof (cases "afeita b b")

assume "afeita b b"

then have "¬ afeita b b"

using h by (rule rev_iffD1)

then show False

using ‹afeita b b› by (rule notE)

assume "¬ afeita b b"

then have "afeita b b"

using h by (rule rev_iffD2)

with ‹¬ afeita b b› show False

by (rule notE)

qed

(* 2ª demostración *)

lemma

"¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)"

proof

assume "∃ x. ∀ y. afeita x y ⟷ ¬ afeita y y"

then obtain b where "∀ y. afeita b y ⟷ ¬ afeita y y"

by (rule exE)

then have h : "afeita b b ⟷ ¬ afeita b b"

by (rule allE)

then show False

by simp

qed

(* 3ª demostración *)

lemma

"¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)"

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las sucesiones convergentes están acotadas

PorJosé A. Alonso 25 julio 202124 julio 2021

Demostrar que si u es una sucesión convergente, entonces está acotada; es decir,

    ∃ k b, ∀ n, n ≥ k → |u n| ≤ b

1	∃ k b, ∀ n, n ≥ k → \|u n\| ≤ b

Para ello, completar la siguiente teoría de Lean:

import data.real.basic

variable {u : ℕ → ℝ}
variable {a : ℝ}

notation `|`x`|` := abs x

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
sorry

import data.real.basic

variable {u : ℕ → ℝ}

variable {a : ℝ}

notation `|`x`|` := abs x

-- (limite u c) expresa que el límite de u es c.

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.

def convergente (u : ℕ → ℝ) :=

∃ a, limite u a

example

(h : convergente u)

: ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variable {u : ℕ → ℝ}
variable {a : ℝ}

notation `|`x`|` := abs x

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

-- 1ª demostración
example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
begin
  cases h with a ua,
  cases ua 1 zero_lt_one with k h,
  use [k, 1 + |a|],
  intros n hn,
  specialize h n hn,
  calc |u n|
       = |u n - a + a|   : congr_arg abs (eq_add_of_sub_eq rfl)
   ... ≤ |u n - a| + |a| : abs_add (u n - a) a
   ... ≤ 1 + |a|         : add_le_add_right h _
end

-- 2ª demostración
example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
begin
  cases h with a ua,
  cases ua 1 zero_lt_one with k h,
  use [k, 1 + |a|],
  intros n hn,
  specialize h n hn,
  calc |u n|
       = |u n - a + a|   : by ring_nf
   ... ≤ |u n - a| + |a| : abs_add (u n - a) a
   ... ≤ 1 + |a|         : by linarith,
end

import data.real.basic

variable {u : ℕ → ℝ}

variable {a : ℝ}

notation `|`x`|` := abs x

-- (limite u c) expresa que el límite de u es c.

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.

def convergente (u : ℕ → ℝ) :=

∃ a, limite u a

-- 1ª demostración

example

(h : convergente u)

: ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=

begin

cases h with a ua,

cases ua 1 zero_lt_one with k h,

use [k, 1 + |a|],

intros n hn,

specialize h n hn,

calc |u n|

= |u n - a + a| : congr_arg abs (eq_add_of_sub_eq rfl)

... ≤ |u n - a| + |a| : abs_add (u n - a) a

... ≤ 1 + |a| : add_le_add_right h _

end

-- 2ª demostración

example

(h : convergente u)

: ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=

begin

cases h with a ua,

cases ua 1 zero_lt_one with k h,

use [k, 1 + |a|],

intros n hn,

specialize h n hn,

calc |u n|

= |u n - a + a| : by ring_nf

... ≤ |u n - a| + |a| : abs_add (u n - a) a

... ≤ 1 + |a| : by linarith,

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Acotacion_de_convergentes
imports Main HOL.Real
begin

(* (limite u c) expresa que el límite de u es c. *)
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

(* (convergente u) expresa que u es convergente. *)
definition convergente :: "(nat ⇒ real) ⇒ bool" where
  "convergente u ⟷ (∃ a. limite u a)"

(* 1ª demostración *)
lemma
  assumes "convergente u"
  shows   "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
proof -
  obtain a where "limite u a"
    using assms convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ 1"
    using limite_def zero_less_one by blast
  have "∀n≥k. ¦u n¦ ≤ 1 + ¦a¦"
  proof (intro allI impI)
    fix n
    assume hn : "n ≥ k"
    have "¦u n¦ = ¦u n - a + a¦"    by simp
    also have "… ≤ ¦u n - a¦ + ¦a¦" by simp
    also have "… ≤ 1 + ¦a¦"         by (simp add: hk hn)
    finally show "¦u n¦ ≤ 1 + ¦a¦"  .
  qed
  then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
    by (intro exI)
qed

(* 2ª demostración *)
lemma
  assumes "convergente u"
  shows   "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
proof -
  obtain a where "limite u a"
    using assms convergente_def 
    by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ 1"
    using limite_def zero_less_one 
    by blast
  have "∀n≥k. ¦u n¦ ≤ 1 + ¦a¦"
    using hk 
    by fastforce
  then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
    by auto
qed

end

theory Acotacion_de_convergentes

imports Main HOL.Real

begin

(* (limite u c) expresa que el límite de u es c. *)

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

(* (convergente u) expresa que u es convergente. *)

definition convergente :: "(nat ⇒ real) ⇒ bool" where

"convergente u ⟷ (∃ a. limite u a)"

(* 1ª demostración *)

lemma

assumes "convergente u"

shows "∃ k b. ∀n≥k. ¦u n¦ ≤ b"

proof -

obtain a where "limite u a"

using assms convergente_def by blast

then obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ 1"

using limite_def zero_less_one by blast

have "∀n≥k. ¦u n¦ ≤ 1 + ¦a¦"

proof (intro allI impI)

fix n

assume hn : "n ≥ k"

have "¦u n¦ = ¦u n - a + a¦" by simp

also have "… ≤ ¦u n - a¦ + ¦a¦" by simp

also have "… ≤ 1 + ¦a¦" by (simp add: hk hn)

finally show "¦u n¦ ≤ 1 + ¦a¦" .

qed

then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b"

by (intro exI)

qed

(* 2ª demostración *)

lemma

assumes "convergente u"

shows "∃ k b. ∀n≥k. ¦u n¦ ≤ b"

proof -

obtain a where "limite u a"

using assms convergente_def

by blast

then obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ 1"

using limite_def zero_less_one

by blast

have "∀n≥k. ¦u n¦ ≤ 1 + ¦a¦"

using hk

by fastforce

then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b"

by auto

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Un número es par si y solo si lo es su cuadrado

PorJosé A. Alonso 24 julio 202124 julio 2021

Demostrar que un número es par si y solo si lo es su cuadrado.

Para ello, completar la siguiente teoría de Lean:

import data.int.parity
import tactic
open int

variable (n : ℤ)

example :
  even (n^2) ↔ even n :=
sorry

import data.int.parity

import tactic

open int

variable (n : ℤ)

example :

even (n^2) ↔ even n :=

sorry

[expand title=»Soluciones con Lean»]

import data.int.parity
import tactic
open int

variable (n : ℤ)

-- 1ª demostración
example :
  even (n^2) ↔ even n :=
begin
  split,
  { contrapose,
    rw ← odd_iff_not_even,
    rw ← odd_iff_not_even,
    unfold odd,
    intro h,
    cases h with k hk,
    use 2*k*(k+1),
    rw hk,
    ring, },
  { unfold even,
    intro h,
    cases h with k hk,
    use 2*k^2,
    rw hk,
    ring, },
end

-- 2ª demostración
example :
  even (n^2) ↔ even n :=
begin
  split,
  { contrapose,
    rw ← odd_iff_not_even,
    rw ← odd_iff_not_even,
    rintro ⟨k, rfl⟩,
    use 2*k*(k+1),
    ring, },
  { rintro ⟨k, rfl⟩,
    use 2*k^2,
    ring, },
end

-- 3ª demostración
example :
  even (n^2) ↔ even n :=
iff.intro
  ( have h : ¬even n → ¬even (n^2),
      { assume h1 : ¬even n,
        have h2 : odd n,
          from odd_iff_not_even.mpr h1,
        have h3: odd (n^2), from
          exists.elim h2
            ( assume k,
              assume hk : n = 2*k+1,
              have h4 : n^2 = 2*(2*k*(k+1))+1, from
                calc  n^2
                    = (2*k+1)^2       : by rw hk
                ... = 4*k^2+4*k+1     : by ring
                ... = 2*(2*k*(k+1))+1 : by ring,
              show odd (n^2),
                from exists.intro (2*k*(k+1)) h4),
        show ¬even (n^2),
          from odd_iff_not_even.mp h3 },
    show even (n^2) → even n,
      from not_imp_not.mp h )
  ( assume h1 : even n,
    show even (n^2), from
      exists.elim h1
        ( assume k,
          assume hk : n = 2*k ,
          have h2 : n^2 = 2*(2*k^2), from
            calc  n^2
                = (2*k)^2   : by rw hk
            ... = 2*(2*k^2) : by ring,
          show even (n^2),
            from exists.intro (2*k^2) h2 ))

-- 4ª demostración
example :
  even (n^2) ↔ even n :=
calc even (n^2)
     ↔ even (n * n)      : iff_of_eq (congr_arg even (sq n))
 ... ↔ (even n ∨ even n) : int.even_mul
 ... ↔ even n            : or_self (even n)

-- 5ª demostración
example :
  even (n^2) ↔ even n :=
calc even (n^2)
     ↔ even (n * n)      : by ring_nf
 ... ↔ (even n ∨ even n) : int.even_mul
 ... ↔ even n            : by simp

-- 6ª demostración
example :
  even (n^2) ↔ even n :=
begin
  split,
  { contrapose,
    intro h,
    rw ← odd_iff_not_even at *,
    cases h with k hk,
    use 2*k*(k+1),
    calc n^2
         = (2*k+1)^2       : by rw hk
     ... = 4*k^2+4*k+1     : by ring
     ... = 2*(2*k*(k+1))+1 : by ring, },
  { intro h,
    cases h with k hk,
    use 2*k^2,
    calc n^2
         = (2*k)^2   : by rw hk
     ... = 2*(2*k^2) : by ring, },
end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

import data.int.parity

import tactic

open int

variable (n : ℤ)

-- 1ª demostración

example :

even (n^2) ↔ even n :=

begin

split,

{ contrapose,

rw ← odd_iff_not_even,

unfold odd,

intro h,

cases h with k hk,

use 2*k*(k+1),

rw hk,

ring, },

{ unfold even,

intro h,

cases h with k hk,

use 2*k^2,

rw hk,

ring, },

end

-- 2ª demostración

example :

even (n^2) ↔ even n :=

begin

split,

{ contrapose,

rw ← odd_iff_not_even,

rintro ⟨k, rfl⟩,

use 2*k*(k+1),

ring, },

{ rintro ⟨k, rfl⟩,

use 2*k^2,

ring, },

end

-- 3ª demostración

example :

even (n^2) ↔ even n :=

iff.intro

( have h : ¬even n → ¬even (n^2),

{ assume h1 : ¬even n,

have h2 : odd n,

from odd_iff_not_even.mpr h1,

have h3: odd (n^2), from

exists.elim h2

( assume k,

assume hk : n = 2*k+1,

have h4 : n^2 = 2*(2*k*(k+1))+1, from

calc n^2

= (2*k+1)^2 : by rw hk

... = 4*k^2+4*k+1 : by ring

... = 2*(2*k*(k+1))+1 : by ring,

show odd (n^2),

from exists.intro (2*k*(k+1)) h4),

show ¬even (n^2),

from odd_iff_not_even.mp h3 },

show even (n^2) → even n,

from not_imp_not.mp h )

( assume h1 : even n,

show even (n^2), from

exists.elim h1

( assume k,

assume hk : n = 2*k ,

have h2 : n^2 = 2*(2*k^2), from

calc n^2

= (2*k)^2 : by rw hk

... = 2*(2*k^2) : by ring,

show even (n^2),

from exists.intro (2*k^2) h2 ))

-- 4ª demostración

example :

even (n^2) ↔ even n :=

calc even (n^2)

↔ even (n * n) : iff_of_eq (congr_arg even (sq n))

... ↔ (even n ∨ even n) : int.even_mul

... ↔ even n : or_self (even n)

-- 5ª demostración

example :

even (n^2) ↔ even n :=

calc even (n^2)

↔ even (n * n) : by ring_nf

... ↔ (even n ∨ even n) : int.even_mul

... ↔ even n : by simp

-- 6ª demostración

example :

even (n^2) ↔ even n :=

begin

split,

{ contrapose,

intro h,

rw ← odd_iff_not_even at *,

cases h with k hk,

use 2*k*(k+1),

calc n^2

= (2*k+1)^2 : by rw hk

... = 4*k^2+4*k+1 : by ring

... = 2*(2*k*(k+1))+1 : by ring, },

{ intro h,

cases h with k hk,

use 2*k^2,

calc n^2

= (2*k)^2 : by rw hk

... = 2*(2*k^2) : by ring, },

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Un_numero_es_par_syss_lo_es_su_cuadrado
imports Main
begin

(* 1ª demostración *)
lemma
  fixes n :: int
  shows "even (n²) ⟷ even n"
proof (rule iffI)
  assume "even (n²)"
  show "even n"
  proof (rule ccontr)
    assume "odd n"
    then obtain k where "n = 2*k+1"
      by (rule oddE)
    then have "n² = 2*(2*k*(k+1))+1"
    proof -
      have "n² = (2*k+1)²"
        by (simp add: ‹n = 2 * k + 1›)
      also have "… = 4*k²+4*k+1"
        by algebra
      also have "… = 2*(2*k*(k+1))+1"
        by algebra
      finally show "n² = 2*(2*k*(k+1))+1" .
    qed
    then have "∃k'. n² = 2*k'+1"
      by (rule exI)
    then have "odd (n²)"
      by fastforce
    then show False
      using ‹even (n²)› by blast
  qed
next
  assume "even n"
  then obtain k where "n = 2*k"
    by (rule evenE)
  then have "n² = 2*(2*k²)"
    by simp
  then show "even (n²)"
    by simp
qed

(* 2ª demostración *)
lemma
  fixes n :: int
  shows "even (n²) ⟷ even n"
proof
  assume "even (n²)"
  show "even n"
  proof (rule ccontr)
    assume "odd n"
    then obtain k where "n = 2*k+1"
      by (rule oddE)
    then have "n² = 2*(2*k*(k+1))+1"
      by algebra
    then have "odd (n²)"
      by simp
    then show False
      using ‹even (n²)› by blast
  qed
next
  assume "even n"
  then obtain k where "n = 2*k"
    by (rule evenE)
  then have "n² = 2*(2*k²)"
    by simp
  then show "even (n²)"
    by simp
qed

(* 3ª demostración *)
lemma
  fixes n :: int
  shows "even (n²) ⟷ even n"
proof -
  have "even (n²) = (even n ∧ (0::nat) < 2)"
    by (simp only: even_power)
  also have "… = (even n ∧ True)"
    by (simp only: less_numeral_simps)
  also have "… = even n"
    by (simp only: HOL.simp_thms(21))
  finally show "even (n²) ⟷ even n"
    by this
qed

(* 4ª demostración *)
lemma
  fixes n :: int
  shows "even (n²) ⟷ even n"
proof -
  have "even (n²) = (even n ∧ (0::nat) < 2)"
    by (simp only: even_power)
  also have "… = even n"
    by simp
  finally show "even (n²) ⟷ even n" .
qed

(* 5ª demostración *)
lemma
  fixes n :: int
  shows "even (n²) ⟷ even n"
  by simp

end

100

101

102

103

104

theory Un_numero_es_par_syss_lo_es_su_cuadrado

imports Main

begin

(* 1ª demostración *)

lemma

fixes n :: int

shows "even (n²) ⟷ even n"

proof (rule iffI)

assume "even (n²)"

show "even n"

proof (rule ccontr)

assume "odd n"

then obtain k where "n = 2*k+1"

by (rule oddE)

then have "n² = 2*(2*k*(k+1))+1"

proof -

have "n² = (2*k+1)²"

by (simp add: ‹n = 2 * k + 1›)

also have "… = 4*k²+4*k+1"

by algebra

also have "… = 2*(2*k*(k+1))+1"

by algebra

finally show "n² = 2*(2*k*(k+1))+1" .

qed

then have "∃k'. n² = 2*k'+1"

by (rule exI)

then have "odd (n²)"

by fastforce

then show False

using ‹even (n²)› by blast

qed

assume "even n"

then obtain k where "n = 2*k"

by (rule evenE)

then have "n² = 2*(2*k²)"

by simp

then show "even (n²)"

by simp

qed

(* 2ª demostración *)

lemma

fixes n :: int

shows "even (n²) ⟷ even n"

proof

assume "even (n²)"

show "even n"

proof (rule ccontr)

assume "odd n"

then obtain k where "n = 2*k+1"

by (rule oddE)

then have "n² = 2*(2*k*(k+1))+1"

by algebra

then have "odd (n²)"

by simp

then show False

using ‹even (n²)› by blast

qed

assume "even n"

then obtain k where "n = 2*k"

by (rule evenE)

then have "n² = 2*(2*k²)"

by simp

then show "even (n²)"

by simp

qed

(* 3ª demostración *)

lemma

fixes n :: int

shows "even (n²) ⟷ even n"

proof -

have "even (n²) = (even n ∧ (0::nat) < 2)"

by (simp only: even_power)

also have "… = (even n ∧ True)"

by (simp only: less_numeral_simps)

also have "… = even n"

by (simp only: HOL.simp_thms(21))

finally show "even (n²) ⟷ even n"

by this

qed

(* 4ª demostración *)

lemma

fixes n :: int

shows "even (n²) ⟷ even n"

proof -

have "even (n²) = (even n ∧ (0::nat) < 2)"

by (simp only: even_power)

also have "… = even n"

by simp

finally show "even (n²) ⟷ even n" .

qed

(* 5ª demostración *)

lemma

fixes n :: int

shows "even (n²) ⟷ even n"

by simp

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Los supremos de las sucesiones crecientes son sus límites

PorJosé A. Alonso 23 julio 202121 julio 2021

Demostrar que si M es un supremo de una sucesión creciente u, entonces el límite de u es M.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic

variable (u : ℕ → ℝ)
variable (M : ℝ)

notation `|`x`|` := abs x

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

-- (supremo u M) expresa que el supremo de u es M.
def supremo (u : ℕ → ℝ) (M : ℝ) :=
  (∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

example
  (hu : monotone u)
  (hM : supremo u M)
  : limite u M :=
sorry

import data.real.basic

variable (u : ℕ → ℝ)

variable (M : ℝ)

notation `|`x`|` := abs x

-- (limite u c) expresa que el límite de u es c.

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

-- (supremo u M) expresa que el supremo de u es M.

def supremo (u : ℕ → ℝ) (M : ℝ) :=

(∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

example

(hu : monotone u)

(hM : supremo u M)

: limite u M :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variable (u : ℕ → ℝ)
variable (M : ℝ)

notation `|`x`|` := abs x

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

-- (supremo u M) expresa que el supremo de u es M.
def supremo (u : ℕ → ℝ) (M : ℝ) :=
  (∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

-- 1ª demostración
example
  (hu : monotone u)
  (hM : supremo u M)
  : limite u M :=
begin
  -- unfold limite,
  intros ε hε,
  -- unfold supremo at h,
  cases hM with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split,
  { -- unfold monotone at h',
    specialize hu hn,
    calc -ε
         = (M - ε) - M : by ring
     ... ≤ u n₀ - M    : sub_le_sub_right hn₀ M
     ... ≤ u n - M     : sub_le_sub_right hu M },
  { calc u n - M
         ≤ M - M       : sub_le_sub_right (hM₁ n) M
     ... = 0           : sub_self M
     ... ≤ ε           : le_of_lt hε, },
end

-- 2ª demostración
example
  (hu : monotone u)
  (hM : supremo u M)
  : limite u M :=
begin
  intros ε hε,
  cases hM with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split,
  { linarith [hu hn] },
  { linarith [hM₁ n] },
end

-- 3ª demostración
example
  (hu : monotone u)
  (hM : supremo u M)
  : limite u M :=
begin
  intros ε hε,
  cases hM with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split ; linarith [hu hn, hM₁ n],
end

-- 4ª demostración
example
  (hu : monotone u)
  (hM : supremo u M)
  : limite u M :=
assume ε,
assume hε : ε > 0,
have hM₁ : ∀ (n : ℕ), u n ≤ M,
  from hM.left,
have hM₂ : ∀ (ε : ℝ), ε > 0 → (∃ (n₀ : ℕ), u n₀ ≥ M - ε),
  from hM.right,
exists.elim (hM₂ ε hε)
  ( assume n₀,
    assume hn₀ : u n₀ ≥ M - ε,
    have h1 : ∀ n, n ≥ n₀ → |u n - M| ≤ ε,
      { assume n,
        assume hn : n ≥ n₀,
        have h2 : -ε ≤ u n - M,
          { have h3 : u n₀ ≤ u n,
              from hu hn,
            calc -ε
                 = (M - ε) - M : by ring
             ... ≤ u n₀ - M    : sub_le_sub_right hn₀ M
             ... ≤ u n - M     : sub_le_sub_right h3 M },
        have h4 : u n - M ≤ ε,
          { calc u n - M
                 ≤ M - M       : sub_le_sub_right (hM₁ n) M
             ... = 0           : sub_self M
             ... ≤ ε           : le_of_lt hε },
        show |u n - M| ≤ ε,
          from abs_le.mpr (and.intro h2 h4) },
    show ∃ N, ∀ n, n ≥ N → |u n - M| ≤ ε,
      from exists.intro n₀ h1)

100

101

102

103

104

105

106

107

import data.real.basic

variable (u : ℕ → ℝ)

variable (M : ℝ)

notation `|`x`|` := abs x

-- (limite u c) expresa que el límite de u es c.

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

-- (supremo u M) expresa que el supremo de u es M.

def supremo (u : ℕ → ℝ) (M : ℝ) :=

(∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

-- 1ª demostración

example

(hu : monotone u)

(hM : supremo u M)

: limite u M :=

begin

-- unfold limite,

intros ε hε,

-- unfold supremo at h,

cases hM with hM₁ hM₂,

cases hM₂ ε hε with n₀ hn₀,

use n₀,

intros n hn,

rw abs_le,

split,

{ -- unfold monotone at h',

specialize hu hn,

calc -ε

= (M - ε) - M : by ring

... ≤ u n₀ - M : sub_le_sub_right hn₀ M

... ≤ u n - M : sub_le_sub_right hu M },

{ calc u n - M

≤ M - M : sub_le_sub_right (hM₁ n) M

... = 0 : sub_self M

... ≤ ε : le_of_lt hε, },

end

-- 2ª demostración

example

(hu : monotone u)

(hM : supremo u M)

: limite u M :=

begin

intros ε hε,

cases hM with hM₁ hM₂,

cases hM₂ ε hε with n₀ hn₀,

use n₀,

intros n hn,

rw abs_le,

split,

{ linarith [hu hn] },

{ linarith [hM₁ n] },

end

-- 3ª demostración

example

(hu : monotone u)

(hM : supremo u M)

: limite u M :=

begin

intros ε hε,

cases hM with hM₁ hM₂,

cases hM₂ ε hε with n₀ hn₀,

use n₀,

intros n hn,

rw abs_le,

split ; linarith [hu hn, hM₁ n],

end

-- 4ª demostración

example

(hu : monotone u)

(hM : supremo u M)

: limite u M :=

assume ε,

assume hε : ε > 0,

have hM₁ : ∀ (n : ℕ), u n ≤ M,

from hM.left,

have hM₂ : ∀ (ε : ℝ), ε > 0 → (∃ (n₀ : ℕ), u n₀ ≥ M - ε),

from hM.right,

exists.elim (hM₂ ε hε)

( assume n₀,

assume hn₀ : u n₀ ≥ M - ε,

have h1 : ∀ n, n ≥ n₀ → |u n - M| ≤ ε,

{ assume n,

assume hn : n ≥ n₀,

have h2 : -ε ≤ u n - M,

{ have h3 : u n₀ ≤ u n,

from hu hn,

calc -ε

= (M - ε) - M : by ring

... ≤ u n₀ - M : sub_le_sub_right hn₀ M

... ≤ u n - M : sub_le_sub_right h3 M },

have h4 : u n - M ≤ ε,

{ calc u n - M

≤ M - M : sub_le_sub_right (hM₁ n) M

... = 0 : sub_self M

... ≤ ε : le_of_lt hε },

show |u n - M| ≤ ε,

from abs_le.mpr (and.intro h2 h4) },

show ∃ N, ∀ n, n ≥ N → |u n - M| ≤ ε,

from exists.intro n₀ h1)

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Los_supremos_de_las_sucesiones_crecientes_son_sus_limites
imports Main HOL.Real
begin

(* (limite u c) expresa que el límite de u es c. *)
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where 
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

(* (supremo u M) expresa que el supremo de u es M. *)
definition supremo :: "(nat ⇒ real) ⇒ real ⇒ bool" where    
  "supremo u M ⟷ ((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"

(* 1ª demostración *)
lemma
  assumes "mono u"
          "supremo u M"
  shows   "limite u M"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"
    using assms(2) 
    by (simp add: supremo_def)
  then have "∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε"
    by (rule conjunct2)
  then have "∃k. ∀n≥k. u n ≥ M - ε"
    by (simp only: ‹0 < ε›) 
  then obtain n0 where "∀n≥n0. u n ≥ M - ε"
    by (rule exE)
  have "∀n≥n0. ¦u n - M¦ ≤ ε" 
  proof (intro allI impI)
    fix n
    assume "n ≥ n0"
    show "¦u n - M¦ ≤ ε" 
    proof (rule abs_leI)
      have "∀n. u n ≤ M"
        using hM by (rule conjunct1)
      then have "u n - M ≤ M - M" 
        by simp
      also have "… = 0" 
        by (simp only: diff_self)
      also have "… ≤ ε" 
        using ‹0 < ε› by (simp only: less_imp_le)
      finally show "u n - M ≤ ε" 
        by this
    next
      have "-ε = (M - ε) - M" 
        by simp
      also have "… ≤ u n - M" 
        using ‹∀n≥n0. M - ε ≤ u n› ‹n0 ≤ n› by auto
      finally have "-ε ≤ u n - M"
        by this
      then show "- (u n - M) ≤ ε" 
        by simp
    qed
  qed
  then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε"
    by (rule exI)
qed

(* 2ª demostración *)
lemma
  assumes "mono u"
          "supremo u M"
  shows   "limite u M"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"
    using assms(2) 
    by (simp add: supremo_def)
  then have "∃k. ∀n≥k. u n ≥ M - ε"
    using ‹0 < ε› by presburger
  then obtain n0 where "∀n≥n0. u n ≥ M - ε" 
    by (rule exE)
  then have "∀n≥n0. ¦u n - M¦ ≤ ε" 
    using hM by auto
  then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε"
    by (rule exI)
qed

end

theory Los_supremos_de_las_sucesiones_crecientes_son_sus_limites

imports Main HOL.Real

begin

(* (limite u c) expresa que el límite de u es c. *)

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

(* (supremo u M) expresa que el supremo de u es M. *)

definition supremo :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"supremo u M ⟷ ((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"

(* 1ª demostración *)

lemma

assumes "mono u"

"supremo u M"

shows "limite u M"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"

using assms(2)

by (simp add: supremo_def)

then have "∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε"

by (rule conjunct2)

then have "∃k. ∀n≥k. u n ≥ M - ε"

by (simp only: ‹0 < ε›)

then obtain n0 where "∀n≥n0. u n ≥ M - ε"

by (rule exE)

have "∀n≥n0. ¦u n - M¦ ≤ ε"

proof (intro allI impI)

fix n

assume "n ≥ n0"

show "¦u n - M¦ ≤ ε"

proof (rule abs_leI)

have "∀n. u n ≤ M"

using hM by (rule conjunct1)

then have "u n - M ≤ M - M"

by simp

also have "… = 0"

by (simp only: diff_self)

also have "… ≤ ε"

using ‹0 < ε› by (simp only: less_imp_le)

finally show "u n - M ≤ ε"

by this

have "-ε = (M - ε) - M"

by simp

also have "… ≤ u n - M"

using ‹∀n≥n0. M - ε ≤ u n› ‹n0 ≤ n› by auto

finally have "-ε ≤ u n - M"

by this

then show "- (u n - M) ≤ ε"

by simp

qed

then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε"

by (rule exI)

qed

(* 2ª demostración *)

lemma

assumes "mono u"

"supremo u M"

shows "limite u M"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"

using assms(2)

by (simp add: supremo_def)

then have "∃k. ∀n≥k. u n ≥ M - ε"

using ‹0 < ε› by presburger

then obtain n0 where "∀n≥n0. u n ≥ M - ε"

by (rule exE)

then have "∀n≥n0. ¦u n - M¦ ≤ ε"

using hM by auto

then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε"

by (rule exI)

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Si `f x ≤ f y → x ≤ y`, entonces f es inyectiva

PorJosé A. Alonso 22 julio 202122 julio 2021

Sea f una función de ℝ en ℝ tal que

   ∀ x y, f(x) ≤ f(y) → x ≤ y

1	∀ x y, f(x) ≤ f(y) → x ≤ y

Demostrar que f es inyectiva.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
open function

variable (f : ℝ → ℝ)

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : injective f :=
sorry

import data.real.basic

open function

variable (f : ℝ → ℝ)

example

(h : ∀ {x y}, f x ≤ f y → x ≤ y)

: injective f :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open function

variable (f : ℝ → ℝ)

-- 1ª demostración
example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : injective f :=
begin
  intros x y hxy,
  apply le_antisymm,
  { apply h,
    exact le_of_eq hxy, },
  { apply h,
    exact ge_of_eq hxy, },
end

-- 2ª demostración
example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : injective f :=
begin
  intros x y hxy,
  apply le_antisymm,
  { exact h (le_of_eq hxy), },
  { exact h (ge_of_eq hxy), },
end

-- 3ª demostración
example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : injective f :=
λ x y hxy, le_antisymm (h hxy.le) (h hxy.ge)

import data.real.basic

open function

variable (f : ℝ → ℝ)

-- 1ª demostración

example

(h : ∀ {x y}, f x ≤ f y → x ≤ y)

: injective f :=

begin

intros x y hxy,

apply le_antisymm,

{ apply h,

exact le_of_eq hxy, },

{ apply h,

exact ge_of_eq hxy, },

end

-- 2ª demostración

example

(h : ∀ {x y}, f x ≤ f y → x ≤ y)

: injective f :=

begin

intros x y hxy,

apply le_antisymm,

{ exact h (le_of_eq hxy), },

{ exact h (ge_of_eq hxy), },

end

-- 3ª demostración

example

(h : ∀ {x y}, f x ≤ f y → x ≤ y)

: injective f :=

λ x y hxy, le_antisymm (h hxy.le) (h hxy.ge)

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory "Si_f(x)_leq_f(y)_to_x_leq_y,_entonces_f_es_inyectiva"
imports Main HOL.Real
begin

(* 1ª demostración *)
lemma
  fixes f :: "real ⇒ real"
  assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"
  shows   "inj f"
proof (rule injI)
  fix x y
  assume "f x = f y"
  show "x = y"
  proof (rule antisym)
    show "x ≤ y" 
      by (simp only: assms ‹f x = f y›)
  next
    show "y ≤ x"
      by (simp only: assms ‹f x = f y›)
  qed
qed

(* 2ª demostración *)
lemma
  fixes f :: "real ⇒ real"
  assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"
  shows   "inj f"
proof (rule injI)
  fix x y
  assume "f x = f y"
  then show "x = y"
    using assms
    by (simp add: eq_iff)
qed

(* 3ª demostración *)
lemma
  fixes f :: "real ⇒ real"
  assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"
  shows   "inj f"
  by (smt (verit, ccfv_threshold) assms inj_on_def)

end

theory "Si_f(x)_leq_f(y)_to_x_leq_y,_entonces_f_es_inyectiva"

imports Main HOL.Real

begin

(* 1ª demostración *)

lemma

fixes f :: "real ⇒ real"

assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"

shows "inj f"

proof (rule injI)

fix x y

assume "f x = f y"

show "x = y"

proof (rule antisym)

show "x ≤ y"

by (simp only: assms ‹f x = f y›)

show "y ≤ x"

by (simp only: assms ‹f x = f y›)

qed

(* 2ª demostración *)

lemma

fixes f :: "real ⇒ real"

assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"

shows "inj f"

proof (rule injI)

fix x y

assume "f x = f y"

then show "x = y"

using assms

by (simp add: eq_iff)

qed

(* 3ª demostración *)

lemma

fixes f :: "real ⇒ real"

assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"

shows "inj f"

by (smt (verit, ccfv_threshold) assms inj_on_def)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]