Calculemus

Si R es un anillo y a, b ∈ R, entonces -a + (a + b) = b

PorJosé A. Alonso 29 agosto 202211 septiembre 2022

En Lean, se declara que R es un anillo mediante la expresión

   variables {R : Type*} [ring R]

1	variables {R : Type*} [ring R]

y, como consecuencia, se tienen los siguientes axiomas

   add_assoc    : ∀ a b c : R, (a + b) + c = a + (b + c)
   add_comm     : ∀ a b : R,   a + b = b + a
   zero_add     : ∀ a : R,     0 + a = a
   add_left_neg : ∀ a : R,     -a + a = 0
   mul_assoc    : ∀ a b c : R, a * b * c = a * (b * c)
   mul_one      : ∀ a : R,     a * 1 = a
   one_mul      : ∀ a : R,     1 * a = a
   mul_add      : ∀ a b c : R, a * (b + c) = a * b + a * c
   add_mul      : ∀ a b c : R, (a + b) * c = a * c + b * c

add_assoc : ∀ a b c : R, (a + b) + c = a + (b + c)

add_comm : ∀ a b : R, a + b = b + a

zero_add : ∀ a : R, 0 + a = a

add_left_neg : ∀ a : R, -a + a = 0

mul_assoc : ∀ a b c : R, a * b * c = a * (b * c)

mul_one : ∀ a : R, a * 1 = a

one_mul : ∀ a : R, 1 * a = a

mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c

add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c

Demostrar que si R es un anillo, entonces

   ∀ a b : R, -a + (a + b) = b

1	∀ a b : R, -a + (a + b) = b

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

import algebra.ring
import tactic

variables {R : Type*} [ring R]
variables a b : R

example
  : -a + (a + b) = b :=
sorry

import algebra.ring

import tactic

variables {R : Type*} [ring R]

variables a b : R

example

: -a + (a + b) = b :=

sorry

Si a y b son números reales, entonces (a + b) * (a – b) = a^2 – b^2

PorJosé A. Alonso 26 agosto 202211 septiembre 2022

Demostrar que si a y b son números reales, entonces

(a + b) * (a - b) = a^2 - b^2

1	(a + b) * (a - b) = a^2 - b^2

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

import data.real.basic

variables a b c d : ℝ

example : (a + b) * (a - b) = a^2 - b^2 :=
sorry

import data.real.basic

variables a b c d : ℝ

example : (a + b) * (a - b) = a^2 - b^2 :=

sorry

Si a, b, c y d son números reales, entonces (a + b) * (c + d) = a * c + a * d + b * c + b * d

PorJosé A. Alonso 25 agosto 202211 septiembre 2022

Demostrar que si a, b, c y d son números reales, entonces

(a + b) * (c + d) = a * c + a * d + b * c + b * d

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

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

import data.real.basic

variables a b c d : ℝ

example
  : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=
sorry

import data.real.basic

variables a b c d : ℝ

example

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

sorry

Si a y b son números reales, entonces (a + b) * (a + b) = a * a + 2 * (a * b) + b * b

PorJosé A. Alonso 24 agosto 202211 septiembre 2022

Demostrar que si a y b son números reales, entonces

(a + b) * (a + b) = a * a + 2 * (a * b) + b * b

1	(a + b) * (a + b) = a * a + 2 * (a * b) + b * b

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

import data.real.basic

variables a b : ℝ

example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
sorry

import data.real.basic

variables a b : ℝ

example :

(a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=

sorry

Si a, b, c, d, e y f son números reales tales que a * b = c * d y e = f entonces, a * (b * e) = c * (d * f)

PorJosé A. Alonso 23 agosto 202211 septiembre 2022

Demostrar que si a, b, c, d, e y f son números reales tales que

   a * b = c * d
   e = f

1 2	a * b = c * d e = f

Entonces,

   a * (b * e) = c * (d * f)

1	a * (b * e) = c * (d * f)

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

import data.real.basic

variables a b c d e f : ℝ

example
  (h1 : a * b = c * d)
  (h2 : e = f)
  : a * (b * e) = c * (d * f) :=

import data.real.basic

variables a b c d e f : ℝ

example

(h1 : a * b = c * d)

(h2 : e = f)

: a * (b * e) = c * (d * f) :=

Si a, b y c son números reales, entonces (a * b) * c = b * (a * c)

PorJosé A. Alonso 22 agosto 202211 septiembre 2022

Demostrar 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 Lean:

import data.real.basic

variables a b c : ℝ

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

import data.real.basic

variables a b c : ℝ

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

sorry

El producto por un par es par

PorJosé A. Alonso 21 agosto 202211 septiembre 2022

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 data.nat.parity
import tactic

open nat

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

import data.nat.parity

import tactic

open nat

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

sorry

Si f·f es biyectiva, entonces f es biyectiva

PorJosé A. Alonso 28 junio 202228 junio 2022

Demostrar que si f·f es biyectiva, entonces f es biyectiva.

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

import tactic
open function

variable {X: Type}

example
  (f : X → X)
  (Hff : bijective (f ∘ f))
  : bijective f :=
sorry

import tactic

open function

variable {X: Type}

example

(f : X → X)

(Hff : bijective (f ∘ f))

: bijective f :=

sorry

Si g·f es suprayectiva, entonces g es suprayectiva

PorJosé A. Alonso 27 junio 2022

Demostrar que si g·f es suprayectiva, entonces g es suprayectiva.

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

import tactic
open function

variables {X Y Z : Type}
variable  {f : X → Y}
variable  {g : Y → Z}

example
  (Hgf : surjective (g ∘ f))
  : surjective g :=
sorry

import tactic

open function

variables {X Y Z : Type}

variable {f : X → Y}

variable {g : Y → Z}

example

(Hgf : surjective (g ∘ f))

: surjective g :=

sorry

Si g·f es inyectiva, entonces f es inyectiva.

PorJosé A. Alonso 22 junio 202222 junio 2022

Demostrar que si g·f es inyectiva, entonces f es inyectiva.

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

import tactic
open function

variables {X Y Z : Type}
variable  {f : X → Y}
variable  {g : Y → Z}

example
  (Hgf : injective (g ∘ f))
  : injective f :=
sorry

import tactic

open function

variables {X Y Z : Type}

variable {f : X → Y}

variable {g : Y → Z}

example

(Hgf : injective (g ∘ f))

: injective f :=

sorry