DAO: La semana en Calculemus (4 de diciembre de 2022)

Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:

1. La suma de dos funciones acotadas superiormente también lo está
2. La suma de dos funciones acotadas inferiormente también lo está
3. Si c ≥ 0 y f está acotada superiormente, entonces c * f también lo está
4. Si x e y son sumas de dos cuadrados, entonces xy también lo es
5. La relación de divisibilidad es transitiva

A continuación se muestran las soluciones.

1. La suma de dos funciones acotadas superiormente también lo está

Demostrar que la suma de dos funciones acotadas superiormente también lo está.

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

import data.real.basic

variables {f g : ℝ → ℝ}
variables {a b : ℝ}

-- (cota_superior f a) se verifica si a es una cota superior de f.
def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a

-- (acotada_sup f) afirma que f tiene cota superior.
def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a

example
  (hf : acotada_sup f)
  (hg : acotada_sup g)
  : acotada_sup (f + g) :=
sorry

import data.real.basic

variables {f g : ℝ → ℝ}

variables {a b : ℝ}

-- (cota_superior f a) se verifica si a es una cota superior de f.

def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a

-- (acotada_sup f) afirma que f tiene cota superior.

def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a

example

(hf : acotada_sup f)

(hg : acotada_sup g)

: acotada_sup (f + g) :=

sorry

Soluciones con Lean

import data.real.basic

variables {f g : ℝ → ℝ}
variables {a b : ℝ}

-- (cota_superior f a) se verifica si a es una cota superior de f.
def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a

-- (acotada_sup f) afirma que f tiene cota superior.
def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a

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

lemma cota_superior_suma
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  : cota_superior (f + g) (a + b) :=
λ x, add_le_add (hfa x) (hgb x)

-- 1ª demostración
-- ===============

example
  (hf : acotada_sup f)
  (hg : acotada_sup g)
  : acotada_sup (f + g) :=
begin
  cases hf with a hfa,
  cases hg with b hgb,
  have h3 : cota_superior (f + g) (a + b) :=
    cota_superior_suma hfa hgb,
  have h4 : ∃ z, ∀ x, (f + g) x ≤ z,
    by exact Exists.intro (a + b) h3,
  show acotada_sup (f + g),
    by exact h4,
end

-- 2ª demostración
-- ===============

example
  (hf : acotada_sup f)
  (hg : acotada_sup g)
  : acotada_sup (f + g) :=
begin
  cases hf with a hfa,
  cases hg with b hfb,
  use a + b,
  apply cota_superior_suma hfa hfb,
end

-- 3ª demostración
-- ===============

example
  (hf : acotada_sup f)
  (hg : acotada_sup g)
  : acotada_sup (f + g) :=
begin
  rcases hf with ⟨a, hfa⟩,
  rcases hg with ⟨b, hfb⟩,
  exact ⟨a + b, cota_superior_suma hfa hfb⟩
end

-- 4ª demostración
-- ===============

example :
  acotada_sup f → acotada_sup g → acotada_sup (f + g) :=
begin
  rintros ⟨a, hfa⟩ ⟨b, hfb⟩,
  exact ⟨a + b, cota_superior_suma hfa hfb⟩,
end

-- 5ª demostración
-- ===============

example :
  acotada_sup f → acotada_sup g → acotada_sup (f + g) :=
λ ⟨a, hfa⟩ ⟨b, hfb⟩, ⟨a + b, cota_superior_suma hfa hfb⟩

import data.real.basic

variables {f g : ℝ → ℝ}

variables {a b : ℝ}

-- (cota_superior f a) se verifica si a es una cota superior de f.

def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a

-- (acotada_sup f) afirma que f tiene cota superior.

def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a

-- Lema auxiliar

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

lemma cota_superior_suma

(hfa : cota_superior f a)

(hgb : cota_superior g b)

: cota_superior (f + g) (a + b) :=

λ x, add_le_add (hfa x) (hgb x)

-- 1ª demostración

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

example

(hf : acotada_sup f)

(hg : acotada_sup g)

: acotada_sup (f + g) :=

begin

cases hf with a hfa,

cases hg with b hgb,

have h3 : cota_superior (f + g) (a + b) :=

cota_superior_suma hfa hgb,

have h4 : ∃ z, ∀ x, (f + g) x ≤ z,

by exact Exists.intro (a + b) h3,

show acotada_sup (f + g),

by exact h4,

end

-- 2ª demostración

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

example

(hf : acotada_sup f)

(hg : acotada_sup g)

: acotada_sup (f + g) :=

begin

cases hf with a hfa,

cases hg with b hfb,

use a + b,

apply cota_superior_suma hfa hfb,

end

-- 3ª demostración

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

example

(hf : acotada_sup f)

(hg : acotada_sup g)

: acotada_sup (f + g) :=

begin

rcases hf with ⟨a, hfa⟩,

rcases hg with ⟨b, hfb⟩,

exact ⟨a + b, cota_superior_suma hfa hfb⟩

end

-- 4ª demostración

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

example :

acotada_sup f → acotada_sup g → acotada_sup (f + g) :=

begin

rintros ⟨a, hfa⟩ ⟨b, hfb⟩,

exact ⟨a + b, cota_superior_suma hfa hfb⟩,

end

-- 5ª demostración

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

example :

acotada_sup f → acotada_sup g → acotada_sup (f + g) :=

λ ⟨a, hfa⟩ ⟨b, hfb⟩, ⟨a + b, cota_superior_suma hfa hfb⟩

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

Referencias

J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 31.

2. La suma de dos funciones acotadas inferiormente también lo está

Demostrar que la suma de dos funciones acotadas inferiormente también lo está.

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

import data.real.basic

variables {f g : ℝ → ℝ}
variables {a b : ℝ}

-- (cota_inferior f a) se verifica si a es una cota inferior de f.
def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x

-- (acotada_inf f) se verifica si f tiene cota inferior.
def acotada_inf (f : ℝ → ℝ) := ∃ a, cota_inferior f a

example
  (hf : acotada_inf f)
  (hg : acotada_inf g)
  : acotada_inf (f + g) :=
sorry

import data.real.basic

variables {f g : ℝ → ℝ}

variables {a b : ℝ}

-- (cota_inferior f a) se verifica si a es una cota inferior de f.

def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x

-- (acotada_inf f) se verifica si f tiene cota inferior.

def acotada_inf (f : ℝ → ℝ) := ∃ a, cota_inferior f a

example

(hf : acotada_inf f)

(hg : acotada_inf g)

: acotada_inf (f + g) :=

sorry

Soluciones con Lean

import data.real.basic

variables {f g : ℝ → ℝ}
variables {a b : ℝ}

-- (cota_inferior f a) se verifica si a es una cota inferior de f.
def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x

-- (acotada_inf f) se verifica si f tiene cota inferior.
def acotada_inf (f : ℝ → ℝ) := ∃ a, cota_inferior f a

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

lemma cota_inferior_add
  (hfa : cota_inferior f a)
  (hgb : cota_inferior g b)
  : cota_inferior (f + g) (a + b) :=
λ x, add_le_add (hfa x) (hgb x)

-- 1ª demostración
-- ===============

example
  (hf : acotada_inf f)
  (hg : acotada_inf g)
  : acotada_inf (f + g) :=
begin
  cases hf with a ha,
  cases hg with b hb,
  have h1 : cota_inferior (f + g) (a + b) := cota_inferior_add ha hb,
  have h2 : ∃ z, ∀ x, z ≤ (f + g) x :=
    by exact Exists.intro (a + b) h1,
  show acotada_inf (f + g),
    by exact h2,
end

-- 2ª demostración
-- ===============

example
  (hf : acotada_inf f)
  (hg : acotada_inf g)
  : acotada_inf (f + g) :=
begin
  cases hf with a hfa,
  cases hg with b hgb,
  use a + b,
  apply cota_inferior_add hfa hgb,
end

-- 3ª demostración
-- ===============

example
  (hf : acotada_inf f)
  (hg : acotada_inf g)
  : acotada_inf (f + g) :=
begin
  rcases hf with ⟨a, hfa⟩,
  rcases hg with ⟨b, hfb⟩,
  exact ⟨a + b, cota_inferior_add hfa hfb⟩,
end

-- 4ª demostración
-- ===============

example :
  acotada_inf f → acotada_inf g → acotada_inf (f + g) :=
begin
  rintros ⟨a, hfa⟩ ⟨b, hfb⟩,
  exact ⟨a + b, cota_inferior_add hfa hfb⟩,
end

-- 5ª demostración
-- ===============

example :
  acotada_inf f → acotada_inf g → acotada_inf (f + g) :=
λ ⟨a, hfa⟩ ⟨b, hfb⟩, ⟨a + b, cota_inferior_add hfa hfb⟩

import data.real.basic

variables {f g : ℝ → ℝ}

variables {a b : ℝ}

-- (cota_inferior f a) se verifica si a es una cota inferior de f.

def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x

-- (acotada_inf f) se verifica si f tiene cota inferior.

def acotada_inf (f : ℝ → ℝ) := ∃ a, cota_inferior f a

-- Lema auxiliar

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

lemma cota_inferior_add

(hfa : cota_inferior f a)

(hgb : cota_inferior g b)

: cota_inferior (f + g) (a + b) :=

λ x, add_le_add (hfa x) (hgb x)

-- 1ª demostración

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

example

(hf : acotada_inf f)

(hg : acotada_inf g)

: acotada_inf (f + g) :=

begin

cases hf with a ha,

cases hg with b hb,

have h1 : cota_inferior (f + g) (a + b) := cota_inferior_add ha hb,

have h2 : ∃ z, ∀ x, z ≤ (f + g) x :=

by exact Exists.intro (a + b) h1,

show acotada_inf (f + g),

by exact h2,

end

-- 2ª demostración

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

example

(hf : acotada_inf f)

(hg : acotada_inf g)

: acotada_inf (f + g) :=

begin

cases hf with a hfa,

cases hg with b hgb,

use a + b,

apply cota_inferior_add hfa hgb,

end

-- 3ª demostración

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

example

(hf : acotada_inf f)

(hg : acotada_inf g)

: acotada_inf (f + g) :=

begin

rcases hf with ⟨a, hfa⟩,

rcases hg with ⟨b, hfb⟩,

exact ⟨a + b, cota_inferior_add hfa hfb⟩,

end

-- 4ª demostración

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

example :

acotada_inf f → acotada_inf g → acotada_inf (f + g) :=

begin

rintros ⟨a, hfa⟩ ⟨b, hfb⟩,

exact ⟨a + b, cota_inferior_add hfa hfb⟩,

end

-- 5ª demostración

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

example :

acotada_inf f → acotada_inf g → acotada_inf (f + g) :=

λ ⟨a, hfa⟩ ⟨b, hfb⟩, ⟨a + b, cota_inferior_add hfa hfb⟩

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

Referencias

J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 31.

3. Si c ≥ 0 y f está acotada superiormente, entonces c * f también lo está

Demostrar que si c ≥ 0 y f está acotada superiormente, entonces c * f también lo está.

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

import data.real.basic

variables {f : ℝ → ℝ}
variables {a c : ℝ}

-- (cota_superior f a) se verifica si a es una cota superior de f.
def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a

-- (acotada_sup f) se verifica si f tiene cota superior.
def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a

example
  (hf : acotada_sup f)
  (h : c ≥ 0)
  : acotada_sup (λ x, c * f x) :=
sorry

import data.real.basic

variables {f : ℝ → ℝ}

variables {a c : ℝ}

-- (cota_superior f a) se verifica si a es una cota superior de f.

def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a

-- (acotada_sup f) se verifica si f tiene cota superior.

def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a

example

(hf : acotada_sup f)

(h : c ≥ 0)

: acotada_sup (λ x, c * f x) :=

sorry

Soluciones con Lean

import data.real.basic

variables {f : ℝ → ℝ}
variables {a c : ℝ}

-- (cota_superior f a) se verifica si a es una cota superior de f.
def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a

-- (acotada_sup f) se verifica si f tiene cota superior.
def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a

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

lemma cota_superior_mul
  (hfa : cota_superior f a)
  (h : c ≥ 0)
  : cota_superior (λ x, c * f x) (c * a) :=
λ x, mul_le_mul_of_nonneg_left (hfa x) h

-- 1ª demostración
-- ===============

example
  (hf : acotada_sup f)
  (h : c ≥ 0)
  : acotada_sup (λ x, c * f x) :=
begin
  cases hf with a ha,
  have h1 : cota_superior (λ x, c * f x) (c * a) := cota_superior_mul ha h,
  have h2 : ∃ z, ∀ x, (λ x, c * f x) x ≤ z,
    by exact Exists.intro (c * a) h1,
  show acotada_sup (λ x, c * f x),
    by exact h2,
end

-- 2ª demostración
-- ===============

example
  (hf : acotada_sup f)
  (h : c ≥ 0)
  : acotada_sup (λ x, c * f x) :=
begin
  cases hf with a ha,
  use c * a,
  apply cota_superior_mul ha h,
end

-- 3ª demostración
-- ===============

example
  (hf : acotada_sup f)
  (h : c ≥ 0)
  : acotada_sup (λ x, c * f x) :=
begin
  rcases hf with ⟨a, ha⟩,
  exact ⟨c * a, cota_superior_mul ha h⟩,
end

-- 4ª demostración
-- ===============

example
  (h : c ≥ 0)
  : acotada_sup f → acotada_sup (λ x, c * f x) :=
begin
  rintro ⟨a, ha⟩,
  exact ⟨c * a, cota_superior_mul ha h⟩,
end

-- 5ª demostración
-- ===============

example
  (h : c ≥ 0)
  : acotada_sup f → acotada_sup (λ x, c * f x) :=
λ ⟨a, ha⟩, ⟨c * a, cota_superior_mul ha h⟩

import data.real.basic

variables {f : ℝ → ℝ}

variables {a c : ℝ}

-- (cota_superior f a) se verifica si a es una cota superior de f.

def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a

-- (acotada_sup f) se verifica si f tiene cota superior.

def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a

-- Lema auxiliar

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

lemma cota_superior_mul

(hfa : cota_superior f a)

(h : c ≥ 0)

: cota_superior (λ x, c * f x) (c * a) :=

λ x, mul_le_mul_of_nonneg_left (hfa x) h

-- 1ª demostración

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

example

(hf : acotada_sup f)

(h : c ≥ 0)

: acotada_sup (λ x, c * f x) :=

begin

cases hf with a ha,

have h1 : cota_superior (λ x, c * f x) (c * a) := cota_superior_mul ha h,

have h2 : ∃ z, ∀ x, (λ x, c * f x) x ≤ z,

by exact Exists.intro (c * a) h1,

show acotada_sup (λ x, c * f x),

by exact h2,

end

-- 2ª demostración

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

example

(hf : acotada_sup f)

(h : c ≥ 0)

: acotada_sup (λ x, c * f x) :=

begin

cases hf with a ha,

use c * a,

apply cota_superior_mul ha h,

end

-- 3ª demostración

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

example

(hf : acotada_sup f)

(h : c ≥ 0)

: acotada_sup (λ x, c * f x) :=

begin

rcases hf with ⟨a, ha⟩,

exact ⟨c * a, cota_superior_mul ha h⟩,

end

-- 4ª demostración

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

example

(h : c ≥ 0)

: acotada_sup f → acotada_sup (λ x, c * f x) :=

begin

rintro ⟨a, ha⟩,

exact ⟨c * a, cota_superior_mul ha h⟩,

end

-- 5ª demostración

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

example

(h : c ≥ 0)

: acotada_sup f → acotada_sup (λ x, c * f x) :=

λ ⟨a, ha⟩, ⟨c * a, cota_superior_mul ha h⟩

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

Referencias

J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 31.

4. Si x e y son sumas de dos cuadrados, entonces xy también lo es

Demostrar que si x e y son sumas de dos cuadrados, entonces xy también lo es.

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

import tactic
variables {α : Type*} [comm_ring α]
variables {x y : α}

-- (es_suma_de_cuadrados x) se verifica si x se puede escribir como la
-- suma de dos cuadrados.
def es_suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2

example
  (hx : es_suma_de_cuadrados x)
  (hy : es_suma_de_cuadrados y)
  : es_suma_de_cuadrados (x * y) :=
sorry

import tactic

variables {α : Type*} [comm_ring α]

variables {x y : α}

-- (es_suma_de_cuadrados x) se verifica si x se puede escribir como la

-- suma de dos cuadrados.

def es_suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2

example

(hx : es_suma_de_cuadrados x)

(hy : es_suma_de_cuadrados y)

: es_suma_de_cuadrados (x * y) :=

sorry

Soluciones con Lean

import tactic
variables {α : Type*} [comm_ring α]
variables {x y : α}

-- (es_suma_de_cuadrados x) se verifica si x se puede escribir como la
-- suma de dos cuadrados.
def es_suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2

-- 1ª demostración
-- ===============

example
  (hx : es_suma_de_cuadrados x)
  (hy : es_suma_de_cuadrados y)
  : es_suma_de_cuadrados (x * y) :=
begin
  rcases hx with ⟨a, b, hab : x = a^2 + b^2⟩,
  rcases hy with ⟨c, d, hcd : y = c^2 + d^2⟩,
  have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2,
    calc x * y
         = (a^2 + b^2) * (c^2 + d^2)     : by rw [hab, hcd]
     ... = (a*c - b*d)^2 + (a*d + b*c)^2 : by ring,
  have h2 : ∃ f, x * y = (a*c - b*d)^2 + f^2,
    by exact Exists.intro (a*d + b*c) h1,
  have h3 : ∃ e f, x * y = e^2 + f^2,
    by exact Exists.intro (a*c - b*d) h2,
  show es_suma_de_cuadrados (x * y),
    by exact h3,
end

-- 2ª demostración
-- ===============

example
  (hx : es_suma_de_cuadrados x)
  (hy : es_suma_de_cuadrados y)
  : es_suma_de_cuadrados (x * y) :=
begin
  rcases hx with ⟨a, b, hab : x = a^2 + b^2⟩,
  rcases hy with ⟨c, d, hcd : y = c^2 + d^2⟩,
  have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2,
    calc x * y
         = (a^2 + b^2) * (c^2 + d^2)     : by rw [hab, hcd]
     ... = (a*c - b*d)^2 + (a*d + b*c)^2 : by ring,
  have h2 : ∃ e f, x * y = e^2 + f^2,
    by tauto,
  show es_suma_de_cuadrados (x * y),
    by exact h2,
end

-- 3ª demostración
-- ===============

example
  (hx : es_suma_de_cuadrados x)
  (hy : es_suma_de_cuadrados y)
  : es_suma_de_cuadrados (x * y) :=
begin
  rcases hx with ⟨a, b, hab⟩,
  rcases hy with ⟨c, d, hcd⟩,
  rw [hab, hcd],
  use [a*c - b*d, a*d + b*c],
  ring,
end

-- 3ª demostración
-- ===============

example
  (hx : es_suma_de_cuadrados x)
  (hy : es_suma_de_cuadrados y)
  : es_suma_de_cuadrados (x * y) :=
begin
  rcases hx with ⟨a, b, rfl⟩,
  rcases hy with ⟨c, d, rfl⟩,
  use [a*c - b*d, a*d + b*c],
  ring
end

import tactic

variables {α : Type*} [comm_ring α]

variables {x y : α}

-- (es_suma_de_cuadrados x) se verifica si x se puede escribir como la

-- suma de dos cuadrados.

def es_suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2

-- 1ª demostración

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

example

(hx : es_suma_de_cuadrados x)

(hy : es_suma_de_cuadrados y)

: es_suma_de_cuadrados (x * y) :=

begin

rcases hx with ⟨a, b, hab : x = a^2 + b^2⟩,

rcases hy with ⟨c, d, hcd : y = c^2 + d^2⟩,

have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2,

calc x * y

= (a^2 + b^2) * (c^2 + d^2) : by rw [hab, hcd]

... = (a*c - b*d)^2 + (a*d + b*c)^2 : by ring,

have h2 : ∃ f, x * y = (a*c - b*d)^2 + f^2,

by exact Exists.intro (a*d + b*c) h1,

have h3 : ∃ e f, x * y = e^2 + f^2,

by exact Exists.intro (a*c - b*d) h2,

show es_suma_de_cuadrados (x * y),

by exact h3,

end

-- 2ª demostración

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

example

(hx : es_suma_de_cuadrados x)

(hy : es_suma_de_cuadrados y)

: es_suma_de_cuadrados (x * y) :=

begin

rcases hx with ⟨a, b, hab : x = a^2 + b^2⟩,

rcases hy with ⟨c, d, hcd : y = c^2 + d^2⟩,

have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2,

calc x * y

= (a^2 + b^2) * (c^2 + d^2) : by rw [hab, hcd]

... = (a*c - b*d)^2 + (a*d + b*c)^2 : by ring,

have h2 : ∃ e f, x * y = e^2 + f^2,

by tauto,

show es_suma_de_cuadrados (x * y),

by exact h2,

end

-- 3ª demostración

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

example

(hx : es_suma_de_cuadrados x)

(hy : es_suma_de_cuadrados y)

: es_suma_de_cuadrados (x * y) :=

begin

rcases hx with ⟨a, b, hab⟩,

rcases hy with ⟨c, d, hcd⟩,

rw [hab, hcd],

use [a*c - b*d, a*d + b*c],

ring,

end

-- 3ª demostración

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

example

(hx : es_suma_de_cuadrados x)

(hy : es_suma_de_cuadrados y)

: es_suma_de_cuadrados (x * y) :=

begin

rcases hx with ⟨a, b, rfl⟩,

rcases hy with ⟨c, d, rfl⟩,

use [a*c - b*d, a*d + b*c],

ring

end

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

Referencias

J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 32.

5. La relación de divisibilidad es transitiva

Demostrar que la relación de divisibilidad es transitiva.

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

import tactic

variables {a b c : ℕ}

example
  (hab : a ∣ b)
  (hbc : b ∣ c)
  : a ∣ c :=
sorry

import tactic

variables {a b c : ℕ}

example

(hab : a ∣ b)

(hbc : b ∣ c)

: a ∣ c :=

sorry

Soluciones con Lean

import tactic

variables {a b c : ℕ}

-- 1ª demostración
-- ===============

example
  (hab : a ∣ b)
  (hbc : b ∣ c)
  : a ∣ c :=
begin
  rcases hab with ⟨d, hd : b = a * d⟩,
  rcases hbc with ⟨e, he : c = b * e⟩,
  have h1 : c = a * (d * e),
    calc c = b * e       : he
       ... = (a * d) * e : congr_arg (* e) hd
       ... = a * (d * e) : mul_assoc a d e,
  show a ∣ c,
    by exact dvd.intro (d * e) (eq.symm h1),
end

-- 2ª demostración
-- ===============

example
  (hab : a ∣ b)
  (hbc : b ∣ c)
  : a ∣ c :=
begin
  cases hab with d hd,
  cases hbc with e he,
  rw [he, hd],
  use (d * e),
  exact mul_assoc a d e,
end

-- 3ª demostración
-- ===============

example
  (hab : a ∣ b)
  (hbc : b ∣ c)
  : a ∣ c :=
begin
  rcases hbc with ⟨e, rfl⟩,
  rcases hab with ⟨d, rfl⟩,
  use (d * e),
  ring,
end

-- 4ª demostración
-- ===============

example
  (hab : a ∣ b)
  (hbc : b ∣ c)
  : a ∣ c :=
-- by library_search
dvd_trans hab hbc

import tactic

variables {a b c : ℕ}

-- 1ª demostración

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

example

(hab : a ∣ b)

(hbc : b ∣ c)

: a ∣ c :=

begin

rcases hab with ⟨d, hd : b = a * d⟩,

rcases hbc with ⟨e, he : c = b * e⟩,

have h1 : c = a * (d * e),

calc c = b * e : he

... = (a * d) * e : congr_arg (* e) hd

... = a * (d * e) : mul_assoc a d e,

show a ∣ c,

by exact dvd.intro (d * e) (eq.symm h1),

end

-- 2ª demostración

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

example

(hab : a ∣ b)

(hbc : b ∣ c)

: a ∣ c :=

begin

cases hab with d hd,

cases hbc with e he,

rw [he, hd],

use (d * e),

exact mul_assoc a d e,

end

-- 3ª demostración

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

example

(hab : a ∣ b)

(hbc : b ∣ c)

: a ∣ c :=

begin

rcases hbc with ⟨e, rfl⟩,

rcases hab with ⟨d, rfl⟩,

use (d * e),

ring,

end

-- 4ª demostración

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

example

(hab : a ∣ b)

(hbc : b ∣ c)

: a ∣ c :=

-- by library_search

dvd_trans hab hbc

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

Referencias

J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 32.

1. La suma de dos funciones acotadas superiormente también lo está

2. La suma de dos funciones acotadas inferiormente también lo está

3. Si c ≥ 0 y f está acotada superiormente, entonces c * f también lo está

4. Si x e y son sumas de dos cuadrados, entonces xy también lo es

5. La relación de divisibilidad es transitiva

Se puede imprimir o compartir con