Matemáticas en Lean

Contenido

• Introducción
  • Resumen
  • Presentación panorámica de Lean
• Aspectos básicos del razonamiento matemático en Lean
  • Cálculos
  • Demostraciones en estructuras algebraicas
  • Uso de lemas y teoremas
  • Más sobre orden y divisibilidad
  • Demostraciones sobre estructuras algebraicas
• Lógica
  • Implicación y cuantificación universal
  • El cuantificador existencial
  • La negación
  • Conjunción y bicondicional
  • Disyunción
  • Sucesiones y convergencia
• Conjuntos y funciones
  • Conjuntos
  • Funciones
• Bibliografía

Introducción

Resumen

El objetivo de este trabajo es presentar el uso de Lean mediante ejemplos matemáticos. Está basado en el libro Mathematics in Lean de Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis y Patrick Massot.

El trabajo se presenta en 3 formas:

• Como un libro en PDF
• Como una página HTML.
• Como un proyecto en GitHub.

#

#

#

#

#

Presentación panorámica de Lean

• Ejemplo de evaluación

• Ejemplo de comprobación con check

• Ejemplo de definición de funciones

• Ejemplo de proposiciones

• Ejemplo de teoremas

• Ejemplo de demostración

Aspectos básicos del razonamiento matemático en Lean

En este capítulo se presentan los aspectos básicos del razonamiento matemático en Lean:

• cálculos,
• aplicación de lemas y teoremas y
• razonamiento sobre estructuras genéricas.

Cálculos

• Asociativa conmutativa de los reales

• Ejercicios sobre aritmética real

• Ejemplo de rw con hipótesis

• Ejercicio de rw con hipótesis

• Reescritura con varios lemas

• Declaración de variables en secciones

• Demostración con calc

• Ejercicio con calc

• Ejercicio: Suma por diferencia

• Reescritura en hipótesis y táctica exact

• Demostraciones con ring

Demostraciones en estructuras algebraicas

Demostraciones en anillos

• Axiomas de anillos

• Propiedades de anillos conmutativos

• Propiedades básicas de anillos

• Lema neg_add_cancel_left

• Ejercicio neg_add_cancel_right

• Ejercicio: Cancelativas de la suma

• Lema mul_zero con have

• Ejercicio zero_mul

• Ejercicios sobre anillos

• Subtracción en anillos

• Ejercicio self_sub

• Ejercicio two_mul

Demostraciones en grupos

• Axiomas de grupo (versión aditiva)

• Axiomas de grupo multiplicativo

• Ejercicios sobre grupos

Uso de lemas y teoremas

• Propiedades reflexiva y transitiva

• Las tácticas apply y exact

• Propiedades del orden

• Ejercicio sobre orden

• Demostraciones por aritmética lineal

• Aritmética lineal con argumentos

• Lemas de desigualdades en R

• Desigualdad de exponenciales (reescritura con el bicondicional)

• Eliminación de bicondicional

• Ejercicio sobre desigualdades

• Uso de library_search

• Ejercicio con library_search

• Desigualdades con calc

• Ejercicio desigualdades absolutas

Más sobre orden y divisibilidad

Mínimos y máximos

• Caracterización del mínimo

• Caracterización del máximo

• Conmutatividad del mínimo

• Conmutatividad del máximo

• Ejercicio: Asociatividad del mínimo

• Ejercicio: Mínimo de suma

• Lema abs_add

• Ejercicio: abs_sub

Divisibilidad

• Propiedades de divisibilidad

• Ejercicio de divisibilidad

• Propiedades de gcd y lcm

• Conmutatividad del gcd

Demostraciones sobre estructuras algebraicas

Órdenes

• Órdenes parciales

• Orden estricto

Retículos

• Retículos

• Conmutatividad del ínfimo

• Conmutatividad del supremo

• Asociatividad del ínfimo

• Asociatividad del supremo

• Leyes de absorción

• Retículos distributivos

• Propiedades distributivas

• Anillos ordenados

Anillos ordenados

• Ejercicio sobre anillos ordenados

Espacios métricos

• Espacios métricos

• Ejercicio en espacios métricos

Lógica

En este capítulo se muestra el razonamiento con Lean sobre las conectivas y cuantificadores; es decir, las tácticas para introducirlos en la conclusión o eliminarlos de las hipótesis. Como aplicación, se demostrarán propiedades sobre límites de sucesiones.

Implicación y cuantificación universal

• Lema con implicaciones y cuantificador universal

• Lema con implicaciones y cuantificador universal implícitos

• La táctica intros

• Definiciones de cotas

• Suma de cotas superiores

• Operaciones con cotas

• Cota_doble

• Generalización a monoides

• Función monótona

• Suma de funciones monótonas

• Producto de un positivo por una función monótona

• Composición de funciones monótonas

• Funciones pares e impares

• Propiedad reflexiva del subconjunto

• Propiedad transitiva del subconjunto

• Cotas superiores de conjuntos

• Funciones inyectivas

• Composición de funciones inyectivas

El cuantificador existencial

• Existencia de valor intermedio

• Definición de funciones acotadas

• Suma de funciones acotadas

• Suma de funciones acotadas inferiormente

• Producto por función acotada superiormente

• Sumas de cotas superiores con rcases y rintros

• Producto_de_suma_de_cuadrados

• Transitividad de la divisibilidad

• Suma divisible

• Suma constante es suprayectiva

• Producto por no nula es suprayectiva

• Propiedad de suprayectivas

• Composición de suprayectivas

La negación

• Asimétrica implica irreflexiva

• Función no acotada superiormente

• Función no acotada inferiormente

• La identidad no está acotada superiormente

• Lemas sobre órdenes y negaciones

• Propiedades de funciones monótonas

• Condición para no positivo

• Negación de cuantificadores

• Doble negación

• CN no acotada superiormente

• CNS de acotada superiormente (uso de push_neg y simp only)

• CN de no monótona

• Principio de explosión

Conjunción y bicondicional

• Introducción de la conjunción

• Eliminación de la conjunción

• Uso de conjunción

• Existenciales y conjunciones anidadas

• Suma nula de dos cuadrados

• Acotación del valor absoluto

• Divisor del mcd

• Funciones no monótonas

• Caracterización de menor en órdenes parciales

• Irreflexiva y transitiva de menor en preórdenes

Disyunción

• Introducción de la disyunción (Tácticas left / right y lemas or.inl y or.inr)

• Eliminación de la disyunción (Táctica cases)

• Desigualdad triangular para valor absoluto

• Cotas del valor absoluto

• Eliminación de la disyunción con rcases

• CS de divisibilidad del producto

• Desigualdad con rcases

• Igualdad de cuadrados

• Igualdad de cuadrados en dominios de integridad

• Eliminación de la doble negación (Tácticas “cases em” y “by_cases”)

• Implicación mediante disyunción y negación

Sucesiones y convergencia

• Definicion de convergencia

• Demostración por extensionalidad (La táctica ext)

• Demostración por congruencia (La táctica congr)

• Demostración por conversión (La táctica convert)

• Convergencia de la función constante

• Convergencia de la suma

• Convergencia del producto por una constante

• Acotación de convergentes

• Producto por sucesión convergente a cero

• Convergencia del producto

• Unicidad del límite

Conjuntos y funciones

En este capítulo se muestra el razonamiento con Lean sobre las operaciones conjuntistas y sobre las funciones.

Conjuntos

• Monotonía de la intersección

• Distributiva de la intersección

• Diferencia de diferencia

• Conmutativa de la intersección

• Identidades conjuntistas

• Unión de pares e impares

• Pertenencia al vacío y al universal

• Primos mayores que dos

• Ejemplos con cuantificadores acotados

• Ejercicios con cuantificadores acotados

• Ejemplos de uniones e intersecciones generales

• Ejercicios de uniones e intersecciones generales

• Ejemplos de uniones e intersecciones generales (2)

• Ejemplos de uniones e intersecciones generales (3)

Funciones

• Preimagen de la intersección

• Imagen de la unión

• Primagen de imagen

• Inclusión de la imagen

• Ejercicios de imágenes y uniones

• Definición de inyectiva

• Inyectividad del logaritmo

• Rango de la exponencial

• Inyectividad del cuadrado

• Rango del cuadrado

• Ejercicios de imágenes y preimágenes

• Valor por defecto y elección de valores

• Función inversa

• Caracterización de las funciones inyectivas mediante la inversa por la izquierda

• Caracterización de las funciones suprayectivas mediante la inversa por la derecha

• Teorema de Cantor

Bibliografía

• Abstract algebra cheatsheet. de Matthias Vallentin.
• Basic guide to tactics de Kevin Buzzard.
• Lean mathlib documentation.
• Mathematics in Lean de Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis y Patrick Massot.
• Maths challenges for the Lean curious de Kevin Buzzard.
• The Lean reference manual de Jeremy Avigad, Gabriel Ebner y Sebastian Ullrich.
• Undergraduate mathematics in mathlib y Missing undergraduate mathematics in mathlib.