Calculemus

∀ a b c ∈ ℝ, (ab)c = b(ac)

PorJosé A. Alonso 11 julio 202319 julio 2023

Demostrar con Lean4 que los números reales tienen la siguiente propiedad

(a * b) * c = b * (a * c)

1	(a * b) * c = b * (a * c)

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

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

example (a b c : ℝ) : (a * b) * c = b * (a * c) := by
sorry

import Mathlib.Tactic

import Mathlib.Data.Real.Basic

example (a b c : ℝ) : (a * b) * c = b * (a * c) := by

sorry

Demostración en lenguaje natural

Por la siguiente cadena de igualdades
\begin{align*}
(ab)c &= (ba)c &&\text{[por la conmutativa]} \\
&= b(ac) &&\text{[por la asociativa]}
\end{align*}

Demostraciones con Lean4

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

-- 1ª demostración
example
  (a b c : ℝ)
  : (a * b) * c = b * (a * c) :=
calc
  (a * b) * c = (b * a) * c := by rw [mul_comm a b]
            _ = b * (a * c) := by rw [mul_assoc b a c]

-- 2ª demostración
example (a b c : ℝ) : (a * b) * c = b * (a * c) := by
  rw [mul_comm a b]
  rw [mul_assoc b a c]

-- 3ª demostración
example (a b c : ℝ) : (a * b) * c = b * (a * c) :=
by ring

import Mathlib.Tactic

import Mathlib.Data.Real.Basic

-- 1ª demostración

example

(a b c : ℝ)

: (a * b) * c = b * (a * c) :=

calc

(a * b) * c = (b * a) * c := by rw [mul_comm a b]

_ = b * (a * c) := by rw [mul_assoc b a c]

-- 2ª demostración

example (a b c : ℝ) : (a * b) * c = b * (a * c) := by

rw [mul_comm a b]

rw [mul_assoc b a c]

-- 3ª demostración

example (a b c : ℝ) : (a * b) * c = b * (a * c) :=

by ring

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 5.

∀ m n : ℕ, Even n → Even (m * n)

PorJosé A. Alonso 10 julio 202319 julio 2023

Demostrar que los productos de los números naturales por números pares son pares.

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

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Parity
import Mathlib.Tactic

open Nat

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  sorry

import Mathlib.Data.Nat.Basic

import Mathlib.Data.Nat.Parity

import Mathlib.Tactic

open Nat

example : ∀ m n : ℕ, Even n → Even (m * n) := by

sorry

Demostración en lenguaje natural

Si \(n\) es par, entonces (por la definición de Even) existe un \(k\) tal que
\[
\begin{align*}
n = k + k && (1)
\end{align*}
\]
Por tanto,
\[
\begin{align*}
mn &= m(k + k) && (\text{por (1)})\\
&= mk + mk && (\text{por la propiedad distributiva})
\end{align*}
\]
Por consiguiente, \(mn\) es par.

Soluciones con Lean4

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Parity
import Mathlib.Tactic

open Nat

-- 1ª demostración
example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk]
  ring

-- 2ª demostración
example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk]
  rw [mul_add]

-- 3ª demostración
example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk, mul_add]

-- 4ª demostración
example : ∀ m n : Nat, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩; use m * k; rw [hk, mul_add]

-- 5ª demostración
example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  exact ⟨m * k, by rw [hk, mul_add]⟩

-- 6ª demostración
example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩

-- 7ª demostración
example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk]
  exact mul_add m k k

-- 8ª demostración
example : ∀ m n : ℕ, Even n → Even (m * n) := by
  intros m n hn
  unfold Even at *
  cases hn with
  | intro k hk =>
    use m * k
    rw [hk, mul_add]

-- 9ª demostración
example : ∀ m n : ℕ, Even n → Even (m * n) := by
  intros m n hn
  unfold Even at *
  cases hn with
  | intro k hk =>
    use m * k
    calc m * n
       = m * (k + k)   := by exact congrArg (HMul.hMul m) hk
     _ = m * k + m * k := by exact mul_add m k k

-- 10ª demostración
example : ∀ m n : Nat, Even n → Even (m * n) := by
  intros; simp [*, parity_simps]

import Mathlib.Data.Nat.Basic

import Mathlib.Data.Nat.Parity

import Mathlib.Tactic

open Nat

-- 1ª demostración

example : ∀ m n : ℕ, Even n → Even (m * n) := by

rintro m n ⟨k, hk⟩

use m * k

rw [hk]

ring

-- 2ª demostración

example : ∀ m n : ℕ, Even n → Even (m * n) := by

rintro m n ⟨k, hk⟩

use m * k

rw [hk]

rw [mul_add]

-- 3ª demostración

example : ∀ m n : ℕ, Even n → Even (m * n) := by

rintro m n ⟨k, hk⟩

use m * k

rw [hk, mul_add]

-- 4ª demostración

example : ∀ m n : Nat, Even n → Even (m * n) := by

rintro m n ⟨k, hk⟩; use m * k; rw [hk, mul_add]

-- 5ª demostración

example : ∀ m n : ℕ, Even n → Even (m * n) := by

rintro m n ⟨k, hk⟩

exact ⟨m * k, by rw [hk, mul_add]⟩

-- 6ª demostración

example : ∀ m n : Nat, Even n → Even (m * n) :=

fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩

-- 7ª demostración

example : ∀ m n : ℕ, Even n → Even (m * n) := by

rintro m n ⟨k, hk⟩

use m * k

rw [hk]

exact mul_add m k k

-- 8ª demostración

example : ∀ m n : ℕ, Even n → Even (m * n) := by

intros m n hn

unfold Even at *

cases hn with

| intro k hk =>

use m * k

rw [hk, mul_add]

-- 9ª demostración

example : ∀ m n : ℕ, Even n → Even (m * n) := by

intros m n hn

unfold Even at *

cases hn with

| intro k hk =>

use m * k

calc m * n

= m * (k + k) := by exact congrArg (HMul.hMul m) hk

_ = m * k + m * k := by exact mul_add m k k

-- 10ª demostración

example : ∀ m n : Nat, Even n → Even (m * n) := by

intros; simp [*, parity_simps]

Se puede interactuar con las pruebas anteriores en Lean 4 Web.

Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 3.

Si a divide a b y a c, entonces también divide a b + c

PorJosé A. Alonso 5 diciembre 20224 diciembre 2022

Demostrar que si a divide a b y a c, entonces también divide a b + c.

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

import tactic

variables {a b c : ℕ}

example
  (divab : a ∣ b)
  (divac : a ∣ c)
  : a ∣ (b + c) :=
sorry

import tactic

variables {a b c : ℕ}

example

(divab : a ∣ b)

(divac : a ∣ c)

: a ∣ (b + c) :=

sorry

La relación de divisibilidad es transitiva

PorJosé A. Alonso 2 diciembre 20221 diciembre 2022

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

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

PorJosé A. Alonso 1 diciembre 202230 noviembre 2022

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

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

PorJosé A. Alonso 30 noviembre 20224 diciembre 2022

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

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

PorJosé A. Alonso 29 noviembre 2022

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

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

PorJosé A. Alonso 28 noviembre 202228 noviembre 2022

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

∃ x ∈ ℝ, 2 < x < 3

PorJosé A. Alonso 25 noviembre 2022

Demostrar que ∃ x ∈ ℝ, 2 < x < 3

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

import data.real.basic

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
sorry

import data.real.basic

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=

sorry

Si f: A → B y g: B → C son inyectiva, entonces g ∘ f es inyectiva

PorJosé A. Alonso 24 noviembre 202223 noviembre 2022

Demostrar que si f: A → B y g: B → C son inyectiva, entonces g ∘ f es inyectiva.

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

import tactic

open function

variables {A : Type*} {B : Type*} {C : Type*}
variables {f : A → B} {g : B → C}

example
  (hg : injective g)
  (hf : injective f) :
  injective (g ∘ f) :=
sorry

import tactic

open function

variables {A : Type*} {B : Type*} {C : Type*}

variables {f : A → B} {g : B → C}

example

(hg : injective g)

(hf : injective f) :

injective (g ∘ f) :=

sorry