https://hrmacbeth.github.io/math2001/index.html

The Mechanics of Proof
[                    ] 
  * Preface

  * 1. Proofs by calculation
  * 2. Proofs with structure
  * 3. Parity and divisibility
  * 4. Proofs with structure, II
  * 5. Logic
  * 6. Induction
  * 7. Number theory
  * 8. Functions
  * 9. Sets
  * 10. Relations

  * Index of Lean tactics
  * Transitioning to mainstream Lean

The Mechanics of Proof

  *  >>
  * The Mechanics of Proof
  * View page source

---------------------------------------------------------------------

The Mechanics of Proof

This is a book dealing with how to write careful, rigorous
mathematical proofs. The book is paired with code in the computer
formalization language Lean. Head over to the associated GitHub
repository, https://github.com/hrmacbeth/math2001, to download this
code to your own computer or to open it in the cloud on Gitpod.

This book is aimed at the early university level and has been written
for the course Math 2001, at Fordham University. Please reach out to
the author, Heather Macbeth, with comments and corrections.

  * Preface
      + About this book
      + Why Lean?
      + Contents and prerequisites
      + Note for instructors
      + Acknowledgements

  * 1. Proofs by calculation
      + 1.1. Proving equalities
      + 1.2. Proving equalities in Lean
      + 1.3. Tips and tricks
      + 1.4. Proving inequalities
      + 1.5. A shortcut
  * 2. Proofs with structure
      + 2.1. Intermediate steps
      + 2.2. Invoking lemmas
      + 2.3. "Or" and proof by cases
      + 2.4. "And"
      + 2.5. Existence proofs
  * 3. Parity and divisibility
      + 3.1. Definitions; parity
      + 3.2. Divisibility
      + 3.3. Modular arithmetic: theory
      + 3.4. Modular arithmetic: calculations
      + 3.5. Bezout's identity
  * 4. Proofs with structure, II
      + 4.1. "For all" and implication
      + 4.2. "If and only if"
      + 4.3. "There exists a unique"
      + 4.4. Contradictory hypotheses
      + 4.5. Proof by contradiction
  * 5. Logic
      + 5.1. Logical equivalence
      + 5.2. The law of the excluded middle
      + 5.3. Normal form for negations
  * 6. Induction
      + 6.1. Introduction
      + 6.2. Recurrence relations
      + 6.3. Two-step induction
      + 6.4. Strong induction
      + 6.5. Pascal's triangle
      + 6.6. The Division Algorithm
      + 6.7. The Euclidean algorithm
  * 7. Number theory
      + 7.1. Infinitely many primes
      + 7.2. Gauss' and Euclid's lemmas
      + 7.3. The square root of two
  * 8. Functions
      + 8.1. Injectivity and surjectivity
      + 8.2. Bijectivity
      + 8.3. Composition of functions
      + 8.4. Product types
  * 9. Sets
      + 9.1. Introduction
      + 9.2. Set operations
      + 9.3. The type of sets
  * 10. Relations
      + 10.1. Reflexive, symmetric, antisymmetric, transitive
      + 10.2. Equivalence relations

Appendices

  * Index of Lean tactics
  * Transitioning to mainstream Lean

Next
---------------------------------------------------------------------

(c) Copyright 2022-2024, Heather Macbeth. All rights reserved.

Built with Sphinx using a theme provided by Read the Docs.