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]