Skip to content

jaalonso/Matematicas_en_Lean

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Matemáticas en Lean

Contenido

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:

#

#

#

#

#

Presentación panorámica de Lean

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

Demostraciones en estructuras algebraicas

Demostraciones en anillos

Demostraciones en grupos

Uso de lemas y teoremas

Más sobre orden y divisibilidad

Mínimos y máximos

Divisibilidad

Demostraciones sobre estructuras algebraicas

Órdenes

Retículos

Anillos ordenados

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

El cuantificador existencial

La negación

Conjunción y bicondicional

Disyunción

Sucesiones y convergencia

Conjuntos y funciones

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

Conjuntos

Funciones

Bibliografía