Mathematics in Lean¶

  • 1. Introduction
    • 1.1. Getting Started
    • 1.2. Overview
  • 2. Basics
    • 2.1. Calculating
    • 2.2. Proving Identities in Algebraic Structures
    • 2.3. Using Theorems and Lemmas
    • 2.4. More on Order and Divisibility
    • 2.5. Proving Facts about Algebraic Structures
  • 3. Logic
    • 3.1. Implication and the Universal Quantifier
    • 3.2. The Existential Quantifier
    • 3.3. Negation
    • 3.4. Conjunction and Bi-implication
    • 3.5. Disjunction
    • 3.6. Sequences and Convergence
  • 4. Sets and Functions
    • 4.1. Sets
    • 4.2. Functions

Mathematics in Lean

  • 1. Introduction
  • 2. Basics
  • 3. Logic
  • 4. Sets and Functions

  • Index
  • PDF version
  • Lean Home

Quick search

©2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot. | Powered by Sphinx 3.2.1 & Alabaster 0.7.12 | Page source