jasonkyi / m4000x_lean_formalisation

Formalising lecture notes from 1st year Imperial Mathematics course.

M4000x LEAN Formalisation

Formalising lecture notes from 1st year Imperial Mathematics course.

Currently planning to refactor M40002 with comments.

M40001 Table of Contents (src/M40001)

Chapter 1 - Sets and Logic

• C1. Law of the Excluded Middle
• C1. De Morgan's Laws
• C1. Transitivity, Contrapositives, and Distirbutivity
• C1. De Morgan's Laws for Sets
• C1. "For all" and "There exists"

Chapter 2 - Functions and Equivalence Relations

• C2. Function Composition
• C2. Injective, Surjective, and Bijective
• C2. Binary Relations
• C2. Predicates on Binary Relations
• C2. Quotients and Equivalence Classes

M40002 Table of Contents (src/M40002)

Chapter 2 - Numbers

• C2. Well-Ordered Principle
• C2. Countability
• C2. Bounds, Supremums and Infimums
• C2. Completeness Axiom and its Corrollaries

Chapter 3 - Sequences

• C3. Convergence of Sequences
• C3. Some Properties of Sequences
• C3. Algebra of Limits for Sequences
• C3. Subsequences
• C3. Cauchy Sequence

Chapter 4 - Series

• C4. Definition of Convergent Series
• C4. Properties of Finite Sums
• C4. Properties of Infinite Sums
• C4. Different Tests for Convergence

Chapter 5 - Continuity

• C5. Definitions of Continuity
• C5. Sequential Continuity
• C5. Algebra of Limits for Functions
• C5. Continuity of Polynomials
• C5. Intermediate Value Theorem
• C5. Open and Closed Sets
• C5. Uniform Continuity and Convergence

Chapter 6 - Differentiation

• C6. Definition of Differentiation
• C6. Some Basic Propterties of Differentiation
• C6. Fermat's Theorem for Stationary Points

m4000x_lean_formalisation's Issues

Compiled html broken!

M400001_C1.html is not clickable
M400002_C2.html is neither clickable and is underlined for some reason!