Análisis – Página 2

Suma de potencias de dos

PorJosé A. Alonso 25 septiembre 202124 septiembre 2021

Demostrar que

   1 + 2 + 2² + 2³ + ... + 2⁽ⁿ⁻¹⁾ = 2ⁿ - 1

1	1 + 2 + 2² + 2³ + ... + 2⁽ⁿ⁻¹⁾ = 2ⁿ - 1

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

import algebra.big_operators
import tactic
open finset nat

open_locale big_operators

variable (n : ℕ)

example :
  ∑ k in range n, 2^k = 2^n - 1 :=
sorry

import algebra.big_operators

import tactic

open finset nat

open_locale big_operators

variable (n : ℕ)

example :

∑ k in range n, 2^k = 2^n - 1 :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.big_operators
import tactic
open finset nat

open_locale big_operators
set_option pp.structure_projections false

variable (n : ℕ)

example :
  ∑ k in range n, 2^k = 2^n - 1 :=
begin
  induction n with n HI,
  { simp, },
  { calc ∑ k in range (succ n), 2^k
         = ∑ k in range n, 2^k + 2^n
             : sum_range_succ (λ x, 2 ^ x) n
     ... = (2^n - 1) + 2^n
             : congr_arg2 (+) HI rfl
     ... = (2^n + 2^n) - 1
             : by omega
     ... = 2^n * 2 - 1
             : by {congr; simp}
     ... = 2^(succ n) - 1
             : by {congr' 1; ring_nf}, },
end

import algebra.big_operators

import tactic

open finset nat

open_locale big_operators

set_option pp.structure_projections false

variable (n : ℕ)

example :

∑ k in range n, 2^k = 2^n - 1 :=

begin

induction n with n HI,

{ simp, },

{ calc ∑ k in range (succ n), 2^k

= ∑ k in range n, 2^k + 2^n

: sum_range_succ (λ x, 2 ^ x) n

... = (2^n - 1) + 2^n

: congr_arg2 (+) HI rfl

... = (2^n + 2^n) - 1

: by omega

... = 2^n * 2 - 1

: by {congr; simp}

... = 2^(succ n) - 1

: by {congr' 1; ring_nf}, },

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 Suma_de_potencias_de_dos
imports Main
begin

(* 1ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1"
    by simp
next
  fix n
  assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
  have "(∑k≤Suc n. (2::nat)^k) =
        (∑k≤n. (2::nat)^k) + 2^Suc n"
    by simp
  also have "… = (2^(n+1) - 1) + 2^Suc n"
    using HI by simp
  also have "… = 2^(Suc n + 1) - 1"
    by simp
  finally show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1" .
qed

(* 2ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1"
    by simp
next
  fix n
  assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
  have "(∑k≤Suc n. (2::nat)^k) =
        (2^(n+1) - 1) + 2^Suc n"
    using HI by simp
  then show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1"
    by simp
qed

(* 3ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by simp
qed

(* 4ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
by (induct n) simp_all

theory Suma_de_potencias_de_dos

imports Main

begin

(* 1ª demostración *)

lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"

proof (induct n)

show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1"

by simp

fix n

assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"

have "(∑k≤Suc n. (2::nat)^k) =

(∑k≤n. (2::nat)^k) + 2^Suc n"

by simp

also have "… = (2^(n+1) - 1) + 2^Suc n"

using HI by simp

also have "… = 2^(Suc n + 1) - 1"

by simp

finally show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1" .

qed

(* 2ª demostración *)

lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"

proof (induct n)

show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1"

by simp

fix n

assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"

have "(∑k≤Suc n. (2::nat)^k) =

(2^(n+1) - 1) + 2^Suc n"

using HI by simp

then show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1"

by simp

qed

(* 3ª demostración *)

lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"

proof (induct n)

case 0

then show ?case by simp

case (Suc n)

then show ?case by simp

qed

(* 4ª demostración *)

lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"

by (induct n) simp_all

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]

Fórmula de Gauss de la suma de los primeros números naturales

PorJosé A. Alonso 24 septiembre 202120 septiembre 2021

La fórmula de Gauss para la suma de los primeros números naturales es

   0 + 1 + 2 + ... + (n-1) = n(n-1)/2

1	0 + 1 + 2 + ... + (n-1) = n(n-1)/2

En un ejercicio anterior se ha demostrado dicha fórmula por inducción. Otra forma de demostrarla, sin usar inducción, es la siguiente: La suma se puede escribir de dos maneras

   S = 0     + 1     + 2     + ... + (n-3) + (n-2) + (n-1)
   S = (n-1) + (n-2) + (n-3) + ... + 2     + 1     + 0

1 2	S = 0 + 1 + 2 + ... + (n-3) + (n-2) + (n-1) S = (n-1) + (n-2) + (n-3) + ... + 2 + 1 + 0

Al sumar, se observa que cada par de números de la misma columna da como suma (n-1), y puesto que hay n columnas en total, se sigue

   2S = n(n-1)

1	2S = n(n-1)

lo que prueba la fórmula.

Demostrar la fórmula de Gauss siguiendo el procedimiento anterior.

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

import algebra.big_operators.basic
import algebra.big_operators.intervals

open_locale big_operators
open finset nat

variables (n i : ℕ)

example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
sorry

import algebra.big_operators.basic

import algebra.big_operators.intervals

open_locale big_operators

open finset nat

variables (n i : ℕ)

example :

(∑ i in range n, i) * 2 = n * (n - 1) :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.big_operators.basic
import algebra.big_operators.intervals

open_locale big_operators
open finset nat

variables (n i : ℕ)

-- Lema auxiliar
-- =============

-- Se usará el siguiente lema auxiliar del que se presentan distintas
-- demostraciones.

-- 1ª demostración del lema auxiliar
example : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=
begin
  intros x hx,
  replace hx : x < n := mem_range.1 hx,
  replace hx : x ≤ n - 1 := le_pred_of_lt hx,
  exact nat.add_sub_cancel' hx,
end

-- 2ª demostración del lema auxiliar
example : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=
begin
  intros x hx,
  exact nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx)),
end

-- 3ª demostración del lema auxiliar
lemma auxiliar : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=
λ x hx, nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx))

-- Lema principal
-- ==============

-- 1ª demostración
example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
calc (∑ i in range n, i) * 2
     = (∑ i in range n, i) + (∑ i in range n, i)
         : mul_two _
 ... = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))
         : congr_arg2 (+) rfl (sum_range_reflect id n).symm
 ... = ∑ i in range n, (i + (n - 1 - i))
         : sum_add_distrib.symm
 ... = ∑ i in range n, (n - 1)
         : sum_congr rfl (auxiliar n)
 ... = card (range n) • (n - 1)
         : sum_const (n - 1)
 ... = card (range n) * (n - 1)
         : nat.nsmul_eq_mul _ _
 ... = n * (n - 1)
         : congr_arg2 (*) (card_range n) rfl

-- 2ª demostración
example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
calc (∑ i in range n, i) * 2
     = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))
         : by rw [sum_range_reflect (λ i, i) n, mul_two]
 ... = ∑ i in range n, (i + (n - 1 - i))
         : sum_add_distrib.symm
 ... = ∑ i in range n, (n - 1)
         : sum_congr rfl (auxiliar n)
 ... = n * (n - 1)
         : by rw [sum_const, card_range, nat.nsmul_eq_mul]

import algebra.big_operators.basic

import algebra.big_operators.intervals

open_locale big_operators

open finset nat

variables (n i : ℕ)

-- Lema auxiliar

-- =============

-- Se usará el siguiente lema auxiliar del que se presentan distintas

-- demostraciones.

-- 1ª demostración del lema auxiliar

example : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=

begin

intros x hx,

replace hx : x < n := mem_range.1 hx,

replace hx : x ≤ n - 1 := le_pred_of_lt hx,

exact nat.add_sub_cancel' hx,

end

-- 2ª demostración del lema auxiliar

example : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=

begin

intros x hx,

exact nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx)),

end

-- 3ª demostración del lema auxiliar

lemma auxiliar : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=

λ x hx, nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx))

-- Lema principal

-- ==============

-- 1ª demostración

example :

(∑ i in range n, i) * 2 = n * (n - 1) :=

calc (∑ i in range n, i) * 2

= (∑ i in range n, i) + (∑ i in range n, i)

: mul_two _

... = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))

: congr_arg2 (+) rfl (sum_range_reflect id n).symm

... = ∑ i in range n, (i + (n - 1 - i))

: sum_add_distrib.symm

... = ∑ i in range n, (n - 1)

: sum_congr rfl (auxiliar n)

... = card (range n) • (n - 1)

: sum_const (n - 1)

... = card (range n) * (n - 1)

: nat.nsmul_eq_mul _ _

... = n * (n - 1)

: congr_arg2 (*) (card_range n) rfl

-- 2ª demostración

example :

(∑ i in range n, i) * 2 = n * (n - 1) :=

calc (∑ i in range n, i) * 2

= (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))

: by rw [sum_range_reflect (λ i, i) n, mul_two]

... = ∑ i in range n, (i + (n - 1 - i))

: sum_add_distrib.symm

... = ∑ i in range n, (n - 1)

: sum_congr rfl (auxiliar n)

... = n * (n - 1)

: by rw [sum_const, card_range, nat.nsmul_eq_mul]

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 Formula_de_Gauss_de_la_suma
imports Main
begin

lemma
  fixes n :: nat
  shows "2 * (∑i<n. i) = n * (n - 1)"
proof -
  have "2 * (∑i<n. i) = (∑i<n. i) + (∑i<n. i)"
    by simp
  also have "… = (∑i<n. i) + (∑i<n. n - Suc i)"
    using sum.nat_diff_reindex [where g = id] by auto
  also have "… = (∑i<n. (i + (n - Suc i)))"
    using sum.distrib [where A = "{..<n}" and
                             g = id and
                             h = "λi. n - Suc i"] by auto
  also have "… = (∑i<n. n - 1)"
    by simp
  also have "… = n * (n -1)"
    using sum_constant by auto
  finally show "2 * (∑i<n. i) = n * (n - 1)" .
qed

end

theory Formula_de_Gauss_de_la_suma

imports Main

begin

lemma

fixes n :: nat

shows "2 * (∑i<n. i) = n * (n - 1)"

proof -

have "2 * (∑i<n. i) = (∑i<n. i) + (∑i<n. i)"

by simp

also have "… = (∑i<n. i) + (∑i<n. n - Suc i)"

using sum.nat_diff_reindex [where g = id] by auto

also have "… = (∑i<n. (i + (n - Suc i)))"

using sum.distrib [where A = "{..<n}" and

g = id and

h = "λi. n - Suc i"] by auto

also have "… = (∑i<n. n - 1)"

by simp

also have "… = n * (n -1)"

using sum_constant by auto

finally show "2 * (∑i<n. i) = n * (n - 1)" .

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]

Suma de los primeros cubos

PorJosé A. Alonso 22 septiembre 202117 septiembre 2021

Demostrar que la suma de los primeros cubos

   0³ + 1³ + 2³ + 3³ + ··· + n³

1	0³ + 1³ + 2³ + 3³ + ··· + n³

es (n(n+1)/2)²

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

import data.nat.basic
import tactic
open nat

variable (n : ℕ)

def sumaCubos : ℕ → ℕ
| 0     := 0
| (n+1) := sumaCubos n + (n+1)^3

example :
  4 * sumaCubos n = (n*(n+1))^2 :=
sorry

import data.nat.basic

import tactic

open nat

variable (n : ℕ)

def sumaCubos : ℕ → ℕ

| 0 := 0

| (n+1) := sumaCubos n + (n+1)^3

example :

4 * sumaCubos n = (n*(n+1))^2 :=

sorry

[expand title=»Soluciones con Lean»]

import data.nat.basic
import tactic
open nat

variable (n : ℕ)

set_option pp.structure_projections false

@[simp]
def sumaCubos : ℕ → ℕ
| 0     := 0
| (n+1) := sumaCubos n + (n+1)^3

-- 1ª demostración
example :
  4 * sumaCubos n = (n*(n+1))^2 :=
begin
  induction n with n HI,
  { simp,
    ring, },
  { calc 4 * sumaCubos (succ n)
         = 4 * (sumaCubos n + (n+1)^3)
           : by simp
     ... = 4 * sumaCubos n + 4*(n+1)^3
           : by ring
     ... = (n*(n+1))^2 + 4*(n+1)^3
           : by {congr; rw HI}
     ... = (n+1)^2*(n^2+4*n+4)
           : by ring
     ... = (n+1)^2*(n+2)^2
           : by ring
     ... = ((n+1)*(n+2))^2
           : by ring
     ... = (succ n * (succ n + 1)) ^ 2
           : by simp, },
end

-- 2ª demostración
example :
  4 * sumaCubos n = (n*(n+1))^2 :=
begin
  induction n with n HI,
  { simp,
    ring, },
  { calc 4 * sumaCubos (succ n)
         = 4 * sumaCubos n + 4*(n+1)^3
           : by {simp ; ring}
     ... = (n*(n+1))^2 + 4*(n+1)^3
           : by {congr; rw HI}
     ... = ((n+1)*(n+2))^2
           : by ring
     ... = (succ n * (succ n + 1)) ^ 2
           : by simp, },
end

import data.nat.basic

import tactic

open nat

variable (n : ℕ)

set_option pp.structure_projections false

@[simp]

def sumaCubos : ℕ → ℕ

| 0 := 0

| (n+1) := sumaCubos n + (n+1)^3

-- 1ª demostración

example :

4 * sumaCubos n = (n*(n+1))^2 :=

begin

induction n with n HI,

{ simp,

ring, },

{ calc 4 * sumaCubos (succ n)

= 4 * (sumaCubos n + (n+1)^3)

: by simp

... = 4 * sumaCubos n + 4*(n+1)^3

: by ring

... = (n*(n+1))^2 + 4*(n+1)^3

: by {congr; rw HI}

... = (n+1)^2*(n^2+4*n+4)

: by ring

... = (n+1)^2*(n+2)^2

: by ring

... = ((n+1)*(n+2))^2

: by ring

... = (succ n * (succ n + 1)) ^ 2

: by simp, },

end

-- 2ª demostración

example :

4 * sumaCubos n = (n*(n+1))^2 :=

begin

induction n with n HI,

{ simp,

ring, },

{ calc 4 * sumaCubos (succ n)

= 4 * sumaCubos n + 4*(n+1)^3

: by {simp ; ring}

... = (n*(n+1))^2 + 4*(n+1)^3

: by {congr; rw HI}

... = ((n+1)*(n+2))^2

: by ring

... = (succ n * (succ n + 1)) ^ 2

: by simp, },

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 Suma_de_los_primeros_cubos
imports Main
begin

fun sumaCubos :: "nat ⇒ nat" where
  "sumaCubos 0       = 0"
| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* 1ª demostración *)
lemma
  "4 * sumaCubos n = (n*(n+1))^2"
proof (induct n)
  show "4 * sumaCubos 0 = (0 * (0 + 1))^2"
    by simp
next
  fix n
  assume HI : "4 * sumaCubos n = (n * (n + 1))^2"
  have "4 * sumaCubos (Suc n) = 4 * (sumaCubos n + (n+1)^3)"
    by simp
  also have "… = 4 * sumaCubos n + 4*(n+1)^3"
    by simp
  also have "… = (n*(n+1))^2 + 4*(n+1)^3"
    using HI by simp
  also have "… = (n+1)^2*(n^2+4*n+4)"
    by algebra
  also have "… = (n+1)^2*(n+2)^2"
    by algebra
  also have "… = ((n+1)*((n+1)+1))^2"
    by algebra
  also have "… = (Suc n * (Suc n + 1))^2"
    by (simp only: Suc_eq_plus1)
  finally show "4 * sumaCubos (Suc n) = (Suc n * (Suc n + 1))^2"
    by this
qed

(* 2ª demostración *)
lemma
  "4 * sumaCubos n = (n*(n+1))^2"
proof (induct n)
  show "4 * sumaCubos 0 = (0 * (0 + 1))^2"
    by simp
next
  fix n
  assume HI : "4 * sumaCubos n = (n * (n + 1))^2"
  have "4 * sumaCubos (Suc n) = 4 * sumaCubos n + 4*(n+1)^3"
    by simp
  also have "… = (n*(n+1))^2 + 4*(n+1)^3"
    using HI by simp
  also have "… = ((n+1)*((n+1)+1))^2"
    by algebra
  also have "… = (Suc n * (Suc n + 1))^2"
    by (simp only: Suc_eq_plus1)
  finally show "4 * sumaCubos (Suc n) = (Suc n * (Suc n + 1))^2" .
qed

end

theory Suma_de_los_primeros_cubos

imports Main

begin

fun sumaCubos :: "nat ⇒ nat" where

"sumaCubos 0 = 0"

| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* 1ª demostración *)

lemma

"4 * sumaCubos n = (n*(n+1))^2"

proof (induct n)

show "4 * sumaCubos 0 = (0 * (0 + 1))^2"

by simp

fix n

assume HI : "4 * sumaCubos n = (n * (n + 1))^2"

have "4 * sumaCubos (Suc n) = 4 * (sumaCubos n + (n+1)^3)"

by simp

also have "… = 4 * sumaCubos n + 4*(n+1)^3"

by simp

also have "… = (n*(n+1))^2 + 4*(n+1)^3"

using HI by simp

also have "… = (n+1)^2*(n^2+4*n+4)"

by algebra

also have "… = (n+1)^2*(n+2)^2"

by algebra

also have "… = ((n+1)*((n+1)+1))^2"

by algebra

also have "… = (Suc n * (Suc n + 1))^2"

by (simp only: Suc_eq_plus1)

finally show "4 * sumaCubos (Suc n) = (Suc n * (Suc n + 1))^2"

by this

qed

(* 2ª demostración *)

lemma

"4 * sumaCubos n = (n*(n+1))^2"

proof (induct n)

show "4 * sumaCubos 0 = (0 * (0 + 1))^2"

by simp

fix n

assume HI : "4 * sumaCubos n = (n * (n + 1))^2"

have "4 * sumaCubos (Suc n) = 4 * sumaCubos n + 4*(n+1)^3"

by simp

also have "… = (n*(n+1))^2 + 4*(n+1)^3"

using HI by simp

also have "… = ((n+1)*((n+1)+1))^2"

by algebra

also have "… = (Suc n * (Suc n + 1))^2"

by (simp only: Suc_eq_plus1)

finally show "4 * sumaCubos (Suc n) = (Suc n * (Suc n + 1))^2" .

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]

Suma de los primeros cuadrados

PorJosé A. Alonso 21 septiembre 202116 septiembre 2021

Demostrar que la suma de los primeros cuadrados

   0² + 1² + 2² + 3² + ··· + n²

1	0² + 1² + 2² + 3² + ··· + n²

es n(n+1)(2n+1)/6.

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

import data.nat.basic
import tactic
open nat

variable (n : ℕ)

@[simp]
def sumaCuadrados : ℕ → ℕ
| 0     := 0
| (n+1) := sumaCuadrados n + (n+1)^2

example :
  6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1) :=
sorry

import data.nat.basic

import tactic

open nat

variable (n : ℕ)

@[simp]

def sumaCuadrados : ℕ → ℕ

| 0 := 0

| (n+1) := sumaCuadrados n + (n+1)^2

example :

6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1) :=

sorry

[expand title=»Soluciones con Lean»]

import data.nat.basic
import tactic
open nat

variable (n : ℕ)

set_option pp.structure_projections false

@[simp]
def sumaCuadrados : ℕ → ℕ
| 0     := 0
| (n+1) := sumaCuadrados n + (n+1)^2

-- 1ª demostración
example :
  6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1) :=
begin
  induction n with n HI,
  { simp, },
  { calc 6 * sumaCuadrados (succ n)
         = 6 * (sumaCuadrados n + (n+1)^2)
           : by simp
     ... = 6 * sumaCuadrados n + 6 * (n+1)^2
           : by ring_nf
     ... = n * (n + 1) * (2 * n + 1) + 6 * (n+1)^2
           : by {congr; rw HI}
     ... = (n + 1) * (n * (2 * n + 1) + 6 * (n+1))
           : by ring_nf
     ... = (n + 1) * (2 * n^2 + 7 * n + 6)
           : by ring_nf
     ... = (n + 1) * (n + 2) * (2 * n + 3)
           : by ring_nf
     ... = succ n * (succ n + 1) * (2 * succ n + 1)
           : by refl, },
end

-- 2ª demostración
example :
  6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1) :=
begin
  induction n with n HI,
  { simp, },
  { calc 6 * sumaCuadrados (succ n)
         = 6 * (sumaCuadrados n + (n+1)^2)
           : by simp
     ... = 6 * sumaCuadrados n + 6 * (n+1)^2
           : by ring_nf
     ... = n * (n + 1) * (2 * n + 1) + 6 * (n+1)^2
           : by {congr; rw HI}
     ... = (n + 1) * (n + 2) * (2 * n + 3)
           : by ring_nf
     ... = succ n * (succ n + 1) * (2 * succ n + 1)
           : by refl, },
end

import data.nat.basic

import tactic

open nat

variable (n : ℕ)

set_option pp.structure_projections false

@[simp]

def sumaCuadrados : ℕ → ℕ

| 0 := 0

| (n+1) := sumaCuadrados n + (n+1)^2

-- 1ª demostración

example :

6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1) :=

begin

induction n with n HI,

{ simp, },

{ calc 6 * sumaCuadrados (succ n)

= 6 * (sumaCuadrados n + (n+1)^2)

: by simp

... = 6 * sumaCuadrados n + 6 * (n+1)^2

: by ring_nf

... = n * (n + 1) * (2 * n + 1) + 6 * (n+1)^2

: by {congr; rw HI}

... = (n + 1) * (n * (2 * n + 1) + 6 * (n+1))

: by ring_nf

... = (n + 1) * (2 * n^2 + 7 * n + 6)

: by ring_nf

... = (n + 1) * (n + 2) * (2 * n + 3)

: by ring_nf

... = succ n * (succ n + 1) * (2 * succ n + 1)

: by refl, },

end

-- 2ª demostración

example :

6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1) :=

begin

induction n with n HI,

{ simp, },

{ calc 6 * sumaCuadrados (succ n)

= 6 * (sumaCuadrados n + (n+1)^2)

: by simp

... = 6 * sumaCuadrados n + 6 * (n+1)^2

: by ring_nf

... = n * (n + 1) * (2 * n + 1) + 6 * (n+1)^2

: by {congr; rw HI}

... = (n + 1) * (n + 2) * (2 * n + 3)

: by ring_nf

... = succ n * (succ n + 1) * (2 * succ n + 1)

: by refl, },

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 Suma_de_los_primeros_cuadrados
imports Main
begin

fun sumaCuadrados :: "nat ⇒ nat" where
  "sumaCuadrados 0       = 0"
| "sumaCuadrados (Suc n) = sumaCuadrados n + (Suc n)^2"

(* 1ª demostración *)
lemma
  "6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1)"
proof (induct n)
  show "6 * sumaCuadrados 0 =  0 * (0 + 1) * (2 * 0 + 1)"
    by simp
next
  fix n
  assume HI : "6 * sumaCuadrados n = n * (n + 1) * (2 * n + 1)"
  have "6 * sumaCuadrados (Suc n) =
        6 * (sumaCuadrados n + (n + 1)^2)"
    by simp
  also have "… = 6 * sumaCuadrados n + 6 * (n + 1)^2"
    by simp
  also have "… = n * (n + 1) * (2 * n + 1) + 6 * (n + 1)^2"
    using HI by simp
  also have "… = (n + 1) * (n * (2 * n + 1) + 6 * (n+1))"
    by algebra
  also have "… = (n + 1) * (2 * n^2 + 7 * n + 6)"
    by algebra
  also have "… = (n + 1) * (n + 2) * (2 * n + 3)"
    by algebra
  also have "… = (n + 1) * ((n + 1) + 1) * (2 * (n + 1) + 1)"
    by algebra
  also have "… = Suc n * (Suc n + 1) * (2 * Suc n + 1)"
    by (simp only: Suc_eq_plus1)
  finally show "6 * sumaCuadrados (Suc n) =
        Suc n * (Suc n + 1) * (2 * Suc n + 1)"
    by this
qed

(* 2ª demostración *)
lemma
  "6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1)"
proof (induct n)
  show "6 * sumaCuadrados 0 =  0 * (0 + 1) * (2 * 0 + 1)"
    by simp
next
  fix n
  assume HI : "6 * sumaCuadrados n = n * (n + 1) * (2 * n + 1)"
  have "6 * sumaCuadrados (Suc n) =
        6 * sumaCuadrados n + 6 * (n + 1)^2"
    by simp
  also have "… = n * (n + 1) * (2 * n + 1) + 6 * (n + 1)^2"
    using HI by simp
  also have "… = (n + 1) * ((n + 1) + 1) * (2 * (n + 1) + 1)"
    by algebra
  finally show "6 * sumaCuadrados (Suc n) =
        Suc n * (Suc n + 1) * (2 * Suc n + 1)"
    by (simp only: Suc_eq_plus1)
qed

end

theory Suma_de_los_primeros_cuadrados

imports Main

begin

fun sumaCuadrados :: "nat ⇒ nat" where

"sumaCuadrados 0 = 0"

| "sumaCuadrados (Suc n) = sumaCuadrados n + (Suc n)^2"

(* 1ª demostración *)

lemma

"6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1)"

proof (induct n)

show "6 * sumaCuadrados 0 = 0 * (0 + 1) * (2 * 0 + 1)"

by simp

fix n

assume HI : "6 * sumaCuadrados n = n * (n + 1) * (2 * n + 1)"

have "6 * sumaCuadrados (Suc n) =

6 * (sumaCuadrados n + (n + 1)^2)"

by simp

also have "… = 6 * sumaCuadrados n + 6 * (n + 1)^2"

by simp

also have "… = n * (n + 1) * (2 * n + 1) + 6 * (n + 1)^2"

using HI by simp

also have "… = (n + 1) * (n * (2 * n + 1) + 6 * (n+1))"

by algebra

also have "… = (n + 1) * (2 * n^2 + 7 * n + 6)"

by algebra

also have "… = (n + 1) * (n + 2) * (2 * n + 3)"

by algebra

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

by algebra

also have "… = Suc n * (Suc n + 1) * (2 * Suc n + 1)"

by (simp only: Suc_eq_plus1)

finally show "6 * sumaCuadrados (Suc n) =

Suc n * (Suc n + 1) * (2 * Suc n + 1)"

by this

qed

(* 2ª demostración *)

lemma

"6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1)"

proof (induct n)

show "6 * sumaCuadrados 0 = 0 * (0 + 1) * (2 * 0 + 1)"

by simp

fix n

assume HI : "6 * sumaCuadrados n = n * (n + 1) * (2 * n + 1)"

have "6 * sumaCuadrados (Suc n) =

6 * sumaCuadrados n + 6 * (n + 1)^2"

by simp

also have "… = n * (n + 1) * (2 * n + 1) + 6 * (n + 1)^2"

using HI by simp

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

by algebra

finally show "6 * sumaCuadrados (Suc n) =

Suc n * (Suc n + 1) * (2 * Suc n + 1)"

by (simp only: Suc_eq_plus1)

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]

Suma de progresión geométrica

PorJosé A. Alonso 20 septiembre 202120 septiembre 2021

Demostrar que la suma de los términos de la progresión geométrica

   a + aq + aq² + ··· + aqnⁿ

1	a + aq + aq² + ··· + aqnⁿ

     a(1 - qⁿ⁺¹)
    -------------
       1 - q

a(1 - qⁿ⁺¹)

-------------

1 - q

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

import data.real.basic
open nat

variable  (n : ℕ)
variables (a q : ℝ)

def sumaPG : ℝ → ℝ → ℕ → ℝ
| a q 0       := a
| a q (n + 1) := sumaPG a q n + (a * q^(n + 1))

example :
  (1 - q) * sumaPG a q n = a * (1 - q^(n + 1)) :=
sorry

import data.real.basic

open nat

variable (n : ℕ)

variables (a q : ℝ)

def sumaPG : ℝ → ℝ → ℕ → ℝ

| a q 0 := a

| a q (n + 1) := sumaPG a q n + (a * q^(n + 1))

example :

(1 - q) * sumaPG a q n = a * (1 - q^(n + 1)) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

variable  (n : ℕ)
variables (a q : ℝ)

set_option pp.structure_projections false

@[simp]
def sumaPG : ℝ → ℝ → ℕ → ℝ
| a q 0       := a
| a q (n + 1) := sumaPG a q n + (a * q^(n + 1))

example :
  (1 - q) * sumaPG a q n = a * (1 - q^(n + 1)) :=
begin
  induction n with n HI,
  { simp,
    ac_refl, },
  { calc (1 - q) * sumaPG a q (succ n)
         = (1 - q) * (sumaPG a q n + (a * q^(n + 1)))
           : rfl
     ... = (1 - q) * sumaPG a q n + (1 - q) * (a * q^(n + 1))
           : by ring_nf
     ... = a * (1 - q ^ (n + 1)) + (1 - q) * (a * q^(n + 1))
           : by {congr ; rw HI}
     ... = a * (1 - q ^ (succ n + 1))
           : by ring_nf },
end

import data.real.basic

open nat

variable (n : ℕ)

variables (a q : ℝ)

set_option pp.structure_projections false

@[simp]

def sumaPG : ℝ → ℝ → ℕ → ℝ

| a q 0 := a

| a q (n + 1) := sumaPG a q n + (a * q^(n + 1))

example :

(1 - q) * sumaPG a q n = a * (1 - q^(n + 1)) :=

begin

induction n with n HI,

{ simp,

ac_refl, },

{ calc (1 - q) * sumaPG a q (succ n)

= (1 - q) * (sumaPG a q n + (a * q^(n + 1)))

: rfl

... = (1 - q) * sumaPG a q n + (1 - q) * (a * q^(n + 1))

: by ring_nf

... = a * (1 - q ^ (n + 1)) + (1 - q) * (a * q^(n + 1))

: by {congr ; rw HI}

... = a * (1 - q ^ (succ n + 1))

: by ring_nf },

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 Suma_de_progresion_geometrica
imports Main HOL.Real
begin

fun sumaPG :: "real ⇒ real ⇒ nat ⇒ real" where
  "sumaPG a q 0 = a"
| "sumaPG a q (Suc n) = sumaPG a q n + (a * q^(n + 1))"

(* 1ª demostración *)
lemma
  "(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"
proof (induct n)
  show "(1 - q) * sumaPG a q 0 = a * (1 - q ^ (0 + 1))"
    by simp
next
  fix n
  assume HI : "(1 - q) * sumaPG a q n = a * (1 - q ^ (n + 1))"
  have "(1 - q) * sumaPG a q (Suc n) =
        (1 - q) * (sumaPG a q n + (a * q^(n + 1)))"
    by simp
  also have "… = (1 - q) * sumaPG a q n + (1 - q) * a * q^(n + 1)"
    by (simp add: algebra_simps)
  also have "… = a * (1 - q ^ (n + 1)) + (1 - q) * a * q^(n + 1)"
    using HI by simp
  also have "… = a * (1 - q ^ (n + 1) + (1 - q) * q^(n + 1))"
    by (simp add: algebra_simps)
  also have "… = a * (1 - q ^ (n + 1) +  q^(n + 1) - q^(n + 2))"
    by (simp add: algebra_simps)
  also have "… = a * (1 - q^(n + 2))"
    by simp
  also have "… = a * (1 - q ^ (Suc n + 1))"
    by simp
  finally show "(1 - q) * sumaPG a q (Suc n) = a * (1 - q ^ (Suc n + 1))"
    by this
qed

(* 2ª demostración *)
lemma
  "(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"
proof (induct n)
  show "(1 - q) * sumaPG a q 0 = a * (1 - q ^ (0 + 1))"
    by simp
next
  fix n
  assume HI : "(1 - q) * sumaPG a q n = a * (1 - q ^ (n + 1))"
  have "(1 - q) * sumaPG a q (Suc n) =
        (1 - q) * sumaPG a q n + (1 - q) * a * q^(n + 1)"
    by (simp add: algebra_simps)
  also have "… = a * (1 - q ^ (n + 1)) + (1 - q) * a * q^(n + 1)"
    using HI by simp
  also have "… = a * (1 - q ^ (n + 1) +  q^(n + 1) - q^(n + 2))"
    by (simp add: algebra_simps)
  finally show "(1 - q) * sumaPG a q (Suc n) = a * (1 - q ^ (Suc n + 1))"
    by simp
qed

(* 3ª demostración *)
lemma
  "(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"
  using power_add
  by (induct n) (auto simp: algebra_simps)

end

theory Suma_de_progresion_geometrica

imports Main HOL.Real

begin

fun sumaPG :: "real ⇒ real ⇒ nat ⇒ real" where

"sumaPG a q 0 = a"

| "sumaPG a q (Suc n) = sumaPG a q n + (a * q^(n + 1))"

(* 1ª demostración *)

lemma

"(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"

proof (induct n)

show "(1 - q) * sumaPG a q 0 = a * (1 - q ^ (0 + 1))"

by simp

fix n

assume HI : "(1 - q) * sumaPG a q n = a * (1 - q ^ (n + 1))"

have "(1 - q) * sumaPG a q (Suc n) =

(1 - q) * (sumaPG a q n + (a * q^(n + 1)))"

by simp

also have "… = (1 - q) * sumaPG a q n + (1 - q) * a * q^(n + 1)"

by (simp add: algebra_simps)

also have "… = a * (1 - q ^ (n + 1)) + (1 - q) * a * q^(n + 1)"

using HI by simp

also have "… = a * (1 - q ^ (n + 1) + (1 - q) * q^(n + 1))"

by (simp add: algebra_simps)

also have "… = a * (1 - q ^ (n + 1) + q^(n + 1) - q^(n + 2))"

by (simp add: algebra_simps)

also have "… = a * (1 - q^(n + 2))"

by simp

also have "… = a * (1 - q ^ (Suc n + 1))"

by simp

finally show "(1 - q) * sumaPG a q (Suc n) = a * (1 - q ^ (Suc n + 1))"

by this

qed

(* 2ª demostración *)

lemma

"(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"

proof (induct n)

show "(1 - q) * sumaPG a q 0 = a * (1 - q ^ (0 + 1))"

by simp

fix n

assume HI : "(1 - q) * sumaPG a q n = a * (1 - q ^ (n + 1))"

have "(1 - q) * sumaPG a q (Suc n) =

(1 - q) * sumaPG a q n + (1 - q) * a * q^(n + 1)"

by (simp add: algebra_simps)

also have "… = a * (1 - q ^ (n + 1)) + (1 - q) * a * q^(n + 1)"

using HI by simp

also have "… = a * (1 - q ^ (n + 1) + q^(n + 1) - q^(n + 2))"

by (simp add: algebra_simps)

finally show "(1 - q) * sumaPG a q (Suc n) = a * (1 - q ^ (Suc n + 1))"

by simp

qed

(* 3ª demostración *)

lemma

"(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"

using power_add

by (induct n) (auto simp: algebra_simps)

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]

Suma de progresión aritmética

PorJosé A. Alonso 19 septiembre 202115 septiembre 2021

Demostrar que la suma de los términos de la progresión aritmética

   a + (a + d) + (a + 2 × d) + ··· + (a + n × d)

1	a + (a + d) + (a + 2 × d) + ··· + (a + n × d)

es (n + 1) × (2 × a + n × d) / 2.

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

import data.real.basic
open nat

variable  (n : ℕ)
variables (a d : ℝ)

@[simp]
def sumaPA : ℝ → ℝ → ℕ → ℝ
| a d 0       := a
| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :
  2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=
sorry

import data.real.basic

open nat

variable (n : ℕ)

variables (a d : ℝ)

@[simp]

def sumaPA : ℝ → ℝ → ℕ → ℝ

| a d 0 := a

| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :

2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

variable  (n : ℕ)
variables (a d : ℝ)

set_option pp.structure_projections false

@[simp]
def sumaPA : ℝ → ℝ → ℕ → ℝ
| a d 0       := a
| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :
  2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=
begin
  induction n with n HI,
  { simp, },
  { calc 2 * sumaPA a d (succ n)
         = 2 * (sumaPA a d n + (a + (n + 1) * d))
           : rfl
     ... = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)
           : by ring_nf
     ... = ((n + 1) * (2 * a + n * d)) + 2 * (a + (n + 1) * d)
           : by {congr; rw HI}
     ... = (n + 2) * (2 * a + (n + 1) * d)
           : by ring_nf
     ... = (succ n + 1) * (2 * a + succ n * d)
           : congr_arg2 (*) (by norm_cast) rfl, },
end

import data.real.basic

open nat

variable (n : ℕ)

variables (a d : ℝ)

set_option pp.structure_projections false

@[simp]

def sumaPA : ℝ → ℝ → ℕ → ℝ

| a d 0 := a

| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :

2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=

begin

induction n with n HI,

{ simp, },

{ calc 2 * sumaPA a d (succ n)

= 2 * (sumaPA a d n + (a + (n + 1) * d))

: rfl

... = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)

: by ring_nf

... = ((n + 1) * (2 * a + n * d)) + 2 * (a + (n + 1) * d)

: by {congr; rw HI}

... = (n + 2) * (2 * a + (n + 1) * d)

: by ring_nf

... = (succ n + 1) * (2 * a + succ n * d)

: congr_arg2 (*) (by norm_cast) rfl, },

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 Suma_de_progresion_aritmetica
imports Main HOL.Real
begin

fun sumaPA :: "real ⇒ real ⇒ nat ⇒ real" where
  "sumaPA a d 0 = a"
| "sumaPA a d (Suc n) = sumaPA a d n + (a + (n + 1) * d)"

(* 1ª demostración *)
lemma
  "2 * sumaPA a d n = (n + 1) * (2 * a + n * d)"
proof (induct n)
  show "2 * sumaPA a d 0 =
        (real 0 + 1) * (2 * a + real 0 * d)"
    by simp
next
  fix n
  assume HI : "2 * sumaPA a d n =
               (n + 1) * (2 * a + n * d)"
  have "2 * sumaPA a d (Suc n) =
        2 * (sumaPA a d n + (a + (n + 1) * d))"
    by simp
  also have "… = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)"
    by simp
  also have "… = (n + 1) * (2 * a + n * d) + 2 * (a + (n + 1) * d)"
    using HI by simp
  also have "… = (real (Suc n) + 1) * (2 * a + (Suc n) * d)"
    by (simp add: algebra_simps)
  finally show "2 * sumaPA a d (Suc n) =
                (real (Suc n) + 1) * (2 * a + (Suc n) * d)"
    by this
qed

(* 2ª demostración *)
lemma
  "2 * sumaPA a d n = (n + 1) * (2*a + n*d)"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by (simp add: algebra_simps)
qed

(* 3ª demostración *)
lemma
  "2 * sumaPA a d n = (n + 1) * (2*a + n*d)"
by (induct n) (simp_all add: algebra_simps)

end

theory Suma_de_progresion_aritmetica

imports Main HOL.Real

begin

fun sumaPA :: "real ⇒ real ⇒ nat ⇒ real" where

"sumaPA a d 0 = a"

| "sumaPA a d (Suc n) = sumaPA a d n + (a + (n + 1) * d)"

(* 1ª demostración *)

lemma

"2 * sumaPA a d n = (n + 1) * (2 * a + n * d)"

proof (induct n)

show "2 * sumaPA a d 0 =

(real 0 + 1) * (2 * a + real 0 * d)"

by simp

fix n

assume HI : "2 * sumaPA a d n =

(n + 1) * (2 * a + n * d)"

have "2 * sumaPA a d (Suc n) =

2 * (sumaPA a d n + (a + (n + 1) * d))"

by simp

also have "… = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)"

by simp

also have "… = (n + 1) * (2 * a + n * d) + 2 * (a + (n + 1) * d)"

using HI by simp

also have "… = (real (Suc n) + 1) * (2 * a + (Suc n) * d)"

by (simp add: algebra_simps)

finally show "2 * sumaPA a d (Suc n) =

(real (Suc n) + 1) * (2 * a + (Suc n) * d)"

by this

qed

(* 2ª demostración *)

lemma

"2 * sumaPA a d n = (n + 1) * (2*a + n*d)"

proof (induct n)

case 0

then show ?case by simp

case (Suc n)

then show ?case by (simp add: algebra_simps)

qed

(* 3ª demostración *)

lemma

"2 * sumaPA a d n = (n + 1) * (2*a + n*d)"

by (induct n) (simp_all add: algebra_simps)

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 es continua en a y el límite de u(n) es a, entonces el límite de f(u(n)) es f(a)

PorJosé A. Alonso 17 septiembre 202114 septiembre 2021

En Lean, se puede definir que a es el límite de la sucesión u por

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

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

y que f es continua en a por

   def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

1 2	def continua_en_punto (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, \|x - a\| ≤ δ → \|f x - f a\| ≤ ε

Demostrar que si f es continua en a y el límite de uₙ es a, entonces el límite de f(uₙ) es f(a).

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

import data.real.basic

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

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

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
sorry

import data.real.basic

variable {f : ℝ → ℝ}

variable {a : ℝ}

variable {u : ℕ → ℝ}

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

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

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

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

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

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

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

-- 1ª demostración
example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
begin
  intros ε hε,
  rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,
  cases hu δ hδ1 with k hk,
  use k,
  intros n hn,
  apply hδ2,
  exact hk n hn,
end

-- 2ª demostración
example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
begin
  intros ε hε,
  rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,
  cases hu δ hδ1 with k hk,
  exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩,
end

-- 3ª demostración
example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
begin
  intros ε hε,
  obtain ⟨δ, hδ1, hδ2⟩ := hf ε hε,
  obtain ⟨k, hk⟩ := hu δ hδ1,
  exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩,
end

import data.real.basic

variable {f : ℝ → ℝ}

variable {a : ℝ}

variable {u : ℕ → ℝ}

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

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

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

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

-- 1ª demostración

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

begin

intros ε hε,

rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,

cases hu δ hδ1 with k hk,

use k,

intros n hn,

apply hδ2,

exact hk n hn,

end

-- 2ª demostración

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

begin

intros ε hε,

rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,

cases hu δ hδ1 with k hk,

exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩,

end

-- 3ª demostración

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

begin

intros ε hε,

obtain ⟨δ, hδ1, hδ2⟩ := hf ε hε,

obtain ⟨k, hk⟩ := hu δ hδ1,

exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩,

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 CS_de_continuidad
imports Main HOL.Real
begin

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

definition continua_en_punto :: "(real ⇒ real) ⇒ real ⇒ bool" where
  "continua_en_punto f a ⟷
   (∀ε>0. ∃δ>0. ∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

(* 1ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where hδ1 : "δ > 0" and
                      hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def hδ1 by auto
  have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
  proof (intro allI impI)
    fix n
    assume "n ≥ k"
    then have "¦u n - a¦ ≤ δ"
      using hk by auto
    then show "¦(f ∘ u) n - f a¦ ≤ ε"
      using hδ2 by simp
  qed
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    by auto
qed

(* 2ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where hδ1 : "δ > 0" and
                      hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def hδ1 by auto
  have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    using hk hδ2 by simp
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    by auto
qed

(* 3ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where hδ1 : "δ > 0" and
                      hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def hδ1 by auto
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    using hk hδ2 by auto
qed

(* 4ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where
              hδ : "δ > 0 ∧ (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  then obtain k where "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def by auto
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    using hδ by auto
qed

(* 5ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
  using assms continua_en_punto_def limite_def
  by force

end

theory CS_de_continuidad

imports Main HOL.Real

begin

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

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

definition continua_en_punto :: "(real ⇒ real) ⇒ real ⇒ bool" where

"continua_en_punto f a ⟷

(∀ε>0. ∃δ>0. ∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

(* 1ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where hδ1 : "δ > 0" and

hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

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

using assms(2) limite_def hδ1 by auto

have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

proof (intro allI impI)

fix n

assume "n ≥ k"

then have "¦u n - a¦ ≤ δ"

using hk by auto

then show "¦(f ∘ u) n - f a¦ ≤ ε"

using hδ2 by simp

qed

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

by auto

qed

(* 2ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where hδ1 : "δ > 0" and

hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

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

using assms(2) limite_def hδ1 by auto

have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

using hk hδ2 by simp

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

by auto

qed

(* 3ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where hδ1 : "δ > 0" and

hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

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

using assms(2) limite_def hδ1 by auto

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

using hk hδ2 by auto

qed

(* 4ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where

hδ : "δ > 0 ∧ (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

then obtain k where "∀n≥k. ¦u n - a¦ ≤ δ"

using assms(2) limite_def by auto

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

using hδ by auto

qed

(* 5ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

using assms continua_en_punto_def limite_def

by force

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 límites son menores o iguales que las cotas superiores

PorJosé A. Alonso 16 septiembre 202111 septiembre 2021

En Lean, se puede definir que a es el límite de la sucesión u por

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

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

y que a es una cota superior de u por

   def cota_superior (u : ℕ → ℝ) (a : ℝ) :=
     ∀ n, u n ≤ a

1 2	def cota_superior (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a

Demostrar que si x es el límite de la sucesión u e y es una cota superior de u, entonces x ≤ y.

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

import data.real.basic

variable  (u : ℕ → ℝ)
variables (x y : ℝ)

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

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

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=
  ∀ n, u n ≤ a

example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
sorry

import data.real.basic

variable (u : ℕ → ℝ)

variables (x y : ℝ)

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

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

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=

∀ n, u n ≤ a

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variable  (u : ℕ → ℝ)
variables (x y : ℝ)

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

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

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=
  ∀ n, u n ≤ a

lemma aux :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  contrapose!,
  intro h,
  use (y-x)/2,
  split ; linarith,
end

-- 1º demostración
example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
begin
  apply aux,
  intros ε hε,
  cases hx ε hε with k hk,
  specialize hk k rfl.ge,
  replace hk : -ε < u k - x := neg_lt_of_abs_lt hk,
  replace hk : x < u k + ε := neg_lt_sub_iff_lt_add'.mp hk,
  apply le_of_lt,
  exact lt_add_of_lt_add_right hk (hy k),
end

-- 2º demostración
example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
begin
  apply aux,
  intros ε hε,
  cases hx ε hε with k hk,
  specialize hk k rfl.ge,
  apply le_of_lt,
  calc x < u k + ε : neg_lt_sub_iff_lt_add'.mp (neg_lt_of_abs_lt hk)
     ... ≤ y + ε   : add_le_add_right (hy k) ε,
end

-- 3º demostración
example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
begin
  apply aux,
  intros ε hε,
  cases hx ε hε with k hk,
  specialize hk k (by linarith),
  rw abs_lt at hk,
  linarith [hy k],
end

import data.real.basic

variable (u : ℕ → ℝ)

variables (x y : ℝ)

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

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

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=

∀ n, u n ≤ a

lemma aux :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

contrapose!,

intro h,

use (y-x)/2,

split ; linarith,

end

-- 1º demostración

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

begin

apply aux,

intros ε hε,

cases hx ε hε with k hk,

specialize hk k rfl.ge,

replace hk : -ε < u k - x := neg_lt_of_abs_lt hk,

replace hk : x < u k + ε := neg_lt_sub_iff_lt_add'.mp hk,

apply le_of_lt,

exact lt_add_of_lt_add_right hk (hy k),

end

-- 2º demostración

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

begin

apply aux,

intros ε hε,

cases hx ε hε with k hk,

specialize hk k rfl.ge,

apply le_of_lt,

calc x < u k + ε : neg_lt_sub_iff_lt_add'.mp (neg_lt_of_abs_lt hk)

... ≤ y + ε : add_le_add_right (hy k) ε,

end

-- 3º demostración

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

begin

apply aux,

intros ε hε,

cases hx ε hε with k hk,

specialize hk k (by linarith),

rw abs_lt at hk,

linarith [hy k],

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 Los_limites_son_menores_o_iguales_que_las_cotas_superiores
imports Main HOL.Real
begin

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

definition cota_superior :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "cota_superior u c ⟷ (∀n. u n ≤ c)"

(* 1ª demostración *)
lemma
  fixes x y :: real
  assumes "limite u x"
          "cota_superior u y"
  shows   "x ≤ y"
proof (rule field_le_epsilon)
  fix ε :: real
  assume "0 < ε"
  then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"
    using assms(1) limite_def by auto
  then have "¦u k - x¦ < ε"
    by simp
  then have "-ε < u k - x"
    by simp
  then have "x < u k + ε"
    by simp
  moreover have "u k ≤ y"
    using assms(2) cota_superior_def by simp
  ultimately show "x ≤ y + ε"
    by simp
qed

(* 2ª demostración *)
lemma
  fixes x y :: real
  assumes "limite u x"
          "cota_superior u y"
  shows   "x ≤ y"
proof (rule field_le_epsilon)
  fix ε :: real
  assume "0 < ε"
  then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"
    using assms(1) limite_def by auto
  then have "x < u k + ε"
    by auto
  moreover have "u k ≤ y"
    using assms(2) cota_superior_def by simp
  ultimately show "x ≤ y + ε"
    by simp
qed

(* 3ª demostración *)
lemma
  fixes x y :: real
  assumes "limite u x"
          "cota_superior u y"
  shows   "x ≤ y"
proof (rule field_le_epsilon)
  fix ε :: real
  assume "0 < ε"
  then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"
    using assms(1) limite_def by auto
  then show "x ≤ y + ε"
    using assms(2) cota_superior_def
    by (smt (verit) order_refl)
qed

end

theory Los_limites_son_menores_o_iguales_que_las_cotas_superiores

imports Main HOL.Real

begin

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

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

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

"cota_superior u c ⟷ (∀n. u n ≤ c)"

(* 1ª demostración *)

lemma

fixes x y :: real

assumes "limite u x"

"cota_superior u y"

shows "x ≤ y"

proof (rule field_le_epsilon)

fix ε :: real

assume "0 < ε"

then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"

using assms(1) limite_def by auto

then have "¦u k - x¦ < ε"

by simp

then have "-ε < u k - x"

by simp

then have "x < u k + ε"

by simp

moreover have "u k ≤ y"

using assms(2) cota_superior_def by simp

ultimately show "x ≤ y + ε"

by simp

qed

(* 2ª demostración *)

lemma

fixes x y :: real

assumes "limite u x"

"cota_superior u y"

shows "x ≤ y"

proof (rule field_le_epsilon)

fix ε :: real

assume "0 < ε"

then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"

using assms(1) limite_def by auto

then have "x < u k + ε"

by auto

moreover have "u k ≤ y"

using assms(2) cota_superior_def by simp

ultimately show "x ≤ y + ε"

by simp

qed

(* 3ª demostración *)

lemma

fixes x y :: real

assumes "limite u x"

"cota_superior u y"

shows "x ≤ y"

proof (rule field_le_epsilon)

fix ε :: real

assume "0 < ε"

then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"

using assms(1) limite_def by auto

then show "x ≤ y + ε"

using assms(2) cota_superior_def

by (smt (verit) order_refl)

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]

Pruebas de «(∀ ε > 0, y ≤ x + ε) → y ≤ x»

PorJosé A. Alonso 15 septiembre 202110 septiembre 2021

Sean x, y ∈ ℝ. Demostrar que

   (∀ ε > 0, y ≤ x + ε) →  y ≤ x

1	(∀ ε > 0, y ≤ x + ε) → y ≤ x

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

import data.real.basic

variables {x y : ℝ}

example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
sorry

import data.real.basic

variables {x y : ℝ}

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variables {x y : ℝ}

-- 1ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  contrapose!,
  intro h,
  use (y-x)/2,
  split,
  { apply half_pos,
    exact sub_pos.mpr h, },
  { calc x + (y - x) / 2
         = (x + y) / 2   : by ring_nf
     ... < (y + y) / 2   : div_lt_div_of_lt zero_lt_two (add_lt_add_right h y)
     ... = (2 * y) / 2   : congr_arg2 (/) (two_mul y).symm rfl
     ... = y             : by ring_nf, },
end

-- 2ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  contrapose!,
  intro h,
  use (y-x)/2,
  split,
  { exact half_pos (sub_pos.mpr h), },
  { calc x + (y - x) / 2
         = (x + y) / 2   : by ring_nf
     ... < (y + y) / 2   : by linarith
     ... = (2 * y) / 2   : by ring_nf
     ... = y             : by ring_nf, },
end

-- 3ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  contrapose!,
  intro h,
  use (y-x)/2,
  split,
  { linarith },
  { linarith },
end

-- 4ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  contrapose!,
  intro h,
  use (y-x)/2,
  split ; linarith,
end

-- 5ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  intro h1,
  by_contradiction h2,
  replace h2 : x < y := not_le.mp h2,
  rcases (exists_between h2) with ⟨z, h3, h4⟩,
  replace h3 : 0 < z - x := sub_pos.mpr h3,
  replace h1 : y ≤ x + (z - x) := h1 (z - x) h3,
  replace h1 : y ≤ z := by finish,
  have h4 : y < y := gt_of_gt_of_ge h4 h1,
  exact absurd h4 (irrefl y),
end

-- 6ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  intro h1,
  by_contradiction h2,
  replace h2 : x < y := not_le.mp h2,
  rcases (exists_between h2) with ⟨z, hxz, hzy⟩,
  apply lt_irrefl y,
  calc y ≤ x + (z - x) : h1 (z - x) (sub_pos.mpr hxz)
     ... = z           : by ring
     ... < y           : hzy,
end

import data.real.basic

variables {x y : ℝ}

-- 1ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

contrapose!,

intro h,

use (y-x)/2,

split,

{ apply half_pos,

exact sub_pos.mpr h, },

{ calc x + (y - x) / 2

= (x + y) / 2 : by ring_nf

... < (y + y) / 2 : div_lt_div_of_lt zero_lt_two (add_lt_add_right h y)

... = (2 * y) / 2 : congr_arg2 (/) (two_mul y).symm rfl

... = y : by ring_nf, },

end

-- 2ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

contrapose!,

intro h,

use (y-x)/2,

split,

{ exact half_pos (sub_pos.mpr h), },

{ calc x + (y - x) / 2

= (x + y) / 2 : by ring_nf

... < (y + y) / 2 : by linarith

... = (2 * y) / 2 : by ring_nf

... = y : by ring_nf, },

end

-- 3ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

contrapose!,

intro h,

use (y-x)/2,

split,

{ linarith },

end

-- 4ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

contrapose!,

intro h,

use (y-x)/2,

split ; linarith,

end

-- 5ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

intro h1,

by_contradiction h2,

replace h2 : x < y := not_le.mp h2,

rcases (exists_between h2) with ⟨z, h3, h4⟩,

replace h3 : 0 < z - x := sub_pos.mpr h3,

replace h1 : y ≤ x + (z - x) := h1 (z - x) h3,

replace h1 : y ≤ z := by finish,

have h4 : y < y := gt_of_gt_of_ge h4 h1,

exact absurd h4 (irrefl y),

end

-- 6ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

intro h1,

by_contradiction h2,

replace h2 : x < y := not_le.mp h2,

rcases (exists_between h2) with ⟨z, hxz, hzy⟩,

apply lt_irrefl y,

calc y ≤ x + (z - x) : h1 (z - x) (sub_pos.mpr hxz)

... = z : by ring

... < y : hzy,

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 CS_de_y_le_x
imports Main HOL.Real
begin

(* 1ª demostración *)
lemma
  fixes x y :: real
  shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"
proof (rule impI)
  assume h1 : "(∀ε>0. y ≤ x + ε)"
  show "y ≤ x"
  proof (rule ccontr)
    assume "¬ (y ≤ x)"
    then have "x < y"
      by simp
    then have "(y - x) / 2 > 0"
      by simp
    then have "y ≤ x + (y - x) / 2"
      using h1 by blast
    then have "2 * y ≤ 2 * x + (y - x)"
      by argo
    then have "y ≤ x"
      by simp
    then show False
      using ‹¬ (y ≤ x)› by simp
  qed
qed

(* 2ª demostración *)
lemma
  fixes x y :: real
  shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"
proof (rule impI)
  assume h1 : "(∀ε>0. y ≤ x + ε)"
  show "y ≤ x"
  proof (rule ccontr)
    assume "¬ (y ≤ x)"
    then have "x < y"
      by simp
    then obtain z where hz : "x < z ∧ z < y"
      using Rats_dense_in_real by blast
    then have "0 < z -x"
      by simp
    then have "y ≤ x + (z - x)"
      using h1 by blast
    then have "y ≤ z"
      by simp
    then show False
      using hz by simp
  qed
qed

(* 3ª demostración *)
lemma
  fixes x y :: real
  shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"
proof (rule impI)
  assume h1 : "(∀ε>0. y ≤ x + ε)"
  show "y ≤ x"
  proof (rule dense_le)
    fix z
    assume "z < y"
    then have "0 < y - z"
      by simp
    then have "y ≤ x + (y - z)"
      using h1 by simp
    then have "0 ≤ x - z"
      by simp
    then show "z ≤ x"
      by simp
  qed
qed

(* 4ª demostración *)
lemma
  fixes x y :: real
  shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"
  by (simp add: field_le_epsilon)

end

theory CS_de_y_le_x

imports Main HOL.Real

begin

(* 1ª demostración *)

lemma

fixes x y :: real

shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"

proof (rule impI)

assume h1 : "(∀ε>0. y ≤ x + ε)"

show "y ≤ x"

proof (rule ccontr)

assume "¬ (y ≤ x)"

then have "x < y"

by simp

then have "(y - x) / 2 > 0"

by simp

then have "y ≤ x + (y - x) / 2"

using h1 by blast

then have "2 * y ≤ 2 * x + (y - x)"

by argo

then have "y ≤ x"

by simp

then show False

using ‹¬ (y ≤ x)› by simp

qed

(* 2ª demostración *)

lemma

fixes x y :: real

shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"

proof (rule impI)

assume h1 : "(∀ε>0. y ≤ x + ε)"

show "y ≤ x"

proof (rule ccontr)

assume "¬ (y ≤ x)"

then have "x < y"

by simp

then obtain z where hz : "x < z ∧ z < y"

using Rats_dense_in_real by blast

then have "0 < z -x"

by simp

then have "y ≤ x + (z - x)"

using h1 by blast

then have "y ≤ z"

by simp

then show False

using hz by simp

qed

(* 3ª demostración *)

lemma

fixes x y :: real

shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"

proof (rule impI)

assume h1 : "(∀ε>0. y ≤ x + ε)"

show "y ≤ x"

proof (rule dense_le)

fix z

assume "z < y"

then have "0 < y - z"

by simp

then have "y ≤ x + (y - z)"

using h1 by simp

then have "0 ≤ x - z"

by simp

then show "z ≤ x"

by simp

qed

(* 4ª demostración *)

lemma

fixes x y :: real

shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"

by (simp add: field_le_epsilon)

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 x es el supremo de A, entonces ∀ y, y < x → ∃ a ∈ A, y < a

PorJosé A. Alonso 14 septiembre 20218 septiembre 2021

En Lean se puede definir que x es una cota superior de A por

   def cota_superior (A : set ℝ) (x : ℝ) :=
     ∀ a ∈ A, a ≤ x

1 2	def cota_superior (A : set ℝ) (x : ℝ) := ∀ a ∈ A, a ≤ x

y x es el supremo de A por

   def es_supremo (A : set ℝ) (x : ℝ) :=
     cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

1 2	def es_supremo (A : set ℝ) (x : ℝ) := cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

Demostrar que si x es el supremo de A, entonces

   ∀ y, y < x → ∃ a ∈ A, y < a

1	∀ y, y < x → ∃ a ∈ A, y < a

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

import data.real.basic
variable {A : set ℝ}
variable {x : ℝ}

def cota_superior (A : set ℝ) (x : ℝ) :=
  ∀ a ∈ A, a ≤ x

def es_supremo (A : set ℝ) (x : ℝ) :=
  cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
sorry

import data.real.basic

variable {A : set ℝ}

variable {x : ℝ}

def cota_superior (A : set ℝ) (x : ℝ) :=

∀ a ∈ A, a ≤ x

def es_supremo (A : set ℝ) (x : ℝ) :=

cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
variable {A : set ℝ}
variable {x : ℝ}

def cota_superior (A : set ℝ) (x : ℝ) :=
  ∀ a ∈ A, a ≤ x

def es_supremo (A : set ℝ) (x : ℝ) :=
  cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

-- 1ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  by_contradiction,
  push_neg at h,
  have h1 : x ≤ y := hx.2 y h,
  replace h1 : ¬(y < x) := not_lt_of_le h1,
  exact h1 hy,
end

-- 2ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  by_contradiction,
  push_neg at h,
  apply absurd hy,
  apply not_lt_of_le,
  apply hx.2 y,
  exact h,
end

-- 3ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  by_contradiction,
  push_neg at h,
  exact absurd hy (not_lt_of_le (hx.2 y h)),
end

-- 4ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  contrapose hy,
  push_neg at hy,
  push_neg,
  unfold es_supremo at hx,
  cases hx with h1 h2,
  apply h2 y,
  unfold cota_superior,
  exact hy,
end

-- 5ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  contrapose hy,
  push_neg at hy,
  push_neg,
  cases hx with h1 h2,
  exact h2 y hy,
end

-- 6ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  contrapose hy,
  push_neg at hy,
  push_neg,
  exact hx.right y hy,
end

-- 7ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intro y,
  contrapose!,
  exact hx.right y,
end

import data.real.basic

variable {A : set ℝ}

variable {x : ℝ}

def cota_superior (A : set ℝ) (x : ℝ) :=

∀ a ∈ A, a ≤ x

def es_supremo (A : set ℝ) (x : ℝ) :=

cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

-- 1ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

by_contradiction,

push_neg at h,

have h1 : x ≤ y := hx.2 y h,

replace h1 : ¬(y < x) := not_lt_of_le h1,

exact h1 hy,

end

-- 2ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

by_contradiction,

push_neg at h,

apply absurd hy,

apply not_lt_of_le,

apply hx.2 y,

exact h,

end

-- 3ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

by_contradiction,

push_neg at h,

exact absurd hy (not_lt_of_le (hx.2 y h)),

end

-- 4ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

contrapose hy,

push_neg at hy,

push_neg,

unfold es_supremo at hx,

cases hx with h1 h2,

apply h2 y,

unfold cota_superior,

exact hy,

end

-- 5ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

contrapose hy,

push_neg at hy,

push_neg,

cases hx with h1 h2,

exact h2 y hy,

end

-- 6ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

contrapose hy,

push_neg at hy,

push_neg,

exact hx.right y hy,

end

-- 7ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intro y,

contrapose!,

exact hx.right y,

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 "Si_x_es_el_supremo_de_A_entonces_forall_y_y_lt_x_to_exists_a_in_A_y_lt_a"
  imports Main HOL.Real
begin

definition cota_superior :: "(real set) ⇒ real ⇒ bool" where
  "cota_superior A x ⟷ (∀a∈A. a ≤ x)"

definition es_supremo :: "(real set) ⇒ real ⇒ bool" where
  "es_supremo A x ⟷ (cota_superior A x ∧
                       (∀ y. cota_superior A y ⟶ x ≤ y))"

(* 1ª demostración *)
lemma
  assumes "es_supremo A x"
  shows   "∀y<x. ∃a∈A. y < a"
proof (intro allI impI)
  fix y
  assume "y < x"
  show "∃a∈A. y < a"
  proof (rule ccontr)
    assume "¬ (∃a∈A. y < a)"
    then have "∀a∈A. a ≤ y"
      by auto
    then have "cota_superior A y"
      using cota_superior_def by simp
    then have "x ≤ y"
      using assms es_supremo_def by simp
    then have "x < x"
      using ‹y < x› by simp
    then show False by simp
  qed
qed

(* 2ª demostración *)
lemma
  assumes "es_supremo A x"
  shows   "∀y<x. ∃a∈A. y < a"
proof (intro allI impI)
  fix y
  assume "y < x"
  show "∃a∈A. y < a"
  proof (rule ccontr)
    assume "¬ (∃a∈A. y < a)"
    then have "cota_superior A y"
      using cota_superior_def by auto
    then show "False"
      using assms es_supremo_def ‹y < x› by auto
  qed
qed


end

theory "Si_x_es_el_supremo_de_A_entonces_forall_y_y_lt_x_to_exists_a_in_A_y_lt_a"

imports Main HOL.Real

begin

definition cota_superior :: "(real set) ⇒ real ⇒ bool" where

"cota_superior A x ⟷ (∀a∈A. a ≤ x)"

definition es_supremo :: "(real set) ⇒ real ⇒ bool" where

"es_supremo A x ⟷ (cota_superior A x ∧

(∀ y. cota_superior A y ⟶ x ≤ y))"

(* 1ª demostración *)

lemma

assumes "es_supremo A x"

shows "∀y<x. ∃a∈A. y < a"

proof (intro allI impI)

fix y

assume "y < x"

show "∃a∈A. y < a"

proof (rule ccontr)

assume "¬ (∃a∈A. y < a)"

then have "∀a∈A. a ≤ y"

by auto

then have "cota_superior A y"

using cota_superior_def by simp

then have "x ≤ y"

using assms es_supremo_def by simp

then have "x < x"

using ‹y < x› by simp

then show False by simp

qed

(* 2ª demostración *)

lemma

assumes "es_supremo A x"

shows "∀y<x. ∃a∈A. y < a"

proof (intro allI impI)

fix y

assume "y < x"

show "∃a∈A. y < a"

proof (rule ccontr)

assume "¬ (∃a∈A. y < a)"

then have "cota_superior A y"

using cota_superior_def by auto

then show "False"

using assms es_supremo_def ‹y < x› 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]