Analysis I, Section 2.2

This file is a translation of Section 2.2 of Analysis I to Lean 4. All numbering refers to the original text.

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• Definition of addition and order for the "Chapter 2" natural numbers, Chapter2.Nat
• Establishment of basic properties of addition and order

Note: at the end of this chapter, the Chapter2.Nat class will be deprecated in favor of the standard Mathlib class _root_.Nat, or ℕ. However, we will develop the properties of Chapter2.Nat "by hand" for pedagogical purposes.

@[reducible, inline]

abbrev Chapter2.Nat.add (n m : Nat) : Nat

Definition 2.2.1. (Addition of natural numbers).

Equations

• n.add m = Chapter2.Nat.recurse (fun (x sum : Chapter2.Nat) => sum++) m n

instance Chapter2.Nat.add_inst : Add Nat

Equations

• Chapter2.Nat.add_inst = { add := Chapter2.Nat.add }

theorem Chapter2.zero_add (m : Nat) : 0 + m = m

theorem Chapter2.succ_add (n m : Nat) : n++ + m = (n + m)++

theorem Chapter2.one_add (m : Nat) : 1 + m = m++

theorem Chapter2.two_add (m : Nat) : 2 + m = m++++

theorem Chapter2.add_zero (n : Nat) : n + 0 = n

Lemma 2.2.2 (n + 0 = n)

theorem Chapter2.add_succ (n m : Nat) : n + m++ = (n + m)++

Lemma 2.2.3 (n+(m++) = (n+m)++).

theorem Chapter2.succ_eq_add_one (n : Nat) : n++ = n + 1

n++ = n + 1 (Why?)

theorem Chapter2.add_comm (n m : Nat) : n + m = m + n

Proposition 2.2.4 (Addition is commutative)

theorem Chapter2.add_assoc (a b c : Nat) : a + b + c = a + (b + c)

Proposition 2.2.5 (Addition is associative) / Exercise 2.2.1

theorem Chapter2.add_cancel_left (a b c : Nat) (habc : a + b = a + c) : b = c

Proposition 2.2.6 (Cancellation law)

instance Chapter2.Nat.addCommMonoid : AddCommMonoid Nat

(Not from textbook) Nat can be given the structure of a commutative additive monoid.

Equations

• One or more equations did not get rendered due to their size.

def Chapter2.Nat.isPos (n : Nat) : Prop

Definition 2.2.7 (Positive natural numbers).

Equations

• n.isPos = (n ≠ 0)

theorem Chapter2.Nat.isPos_iff (n : Nat) : n.isPos ↔ n ≠ 0

theorem Chapter2.pos_add {a : Nat} (b : Nat) (ha : a.isPos) : (a + b).isPos

Proposition 2.2.8 (positive plus natural number is positive).

theorem Chapter2.add_pos {a : Nat} (b : Nat) (ha : a.isPos) : (b + a).isPos

theorem Chapter2.add_eq_zero (a b : Nat) (hab : a + b = 0) : a = 0 ∧ b = 0

Corollary 2.2.9 (if sum vanishes, then summands vanish).

theorem Chapter2.uniq_succ_eq (a : Nat) (ha : a.isPos) : ∃! b : Nat, b++ = a

Lemma 2.2.10 (unique predecessor) / Exercise 2.2.2

instance Chapter2.Nat.LE_inst : LE Nat

Definition 2.2.11 (Ordering of the natural numbers)

Equations

• Chapter2.Nat.LE_inst = { le := fun (n m : Chapter2.Nat) => ∃ (a : Chapter2.Nat), m = n + a }

instance Chapter2.Nat.LT_inst : LT Nat

Definition 2.2.11 (Ordering of the natural numbers)

Equations

• Chapter2.Nat.LT_inst = { lt := fun (n m : Chapter2.Nat) => (∃ (a : Chapter2.Nat), m = n + a) ∧ n ≠ m }

theorem Chapter2.Nat.le_iff (n m : Nat) : n ≤ m ↔ ∃ (a : Nat), m = n + a

theorem Chapter2.Nat.lt_iff (n m : Nat) : n < m ↔ (∃ (a : Nat), m = n + a) ∧ n ≠ m

theorem Chapter2.Nat.ge_iff_le (n m : Nat) : n ≥ m ↔ m ≤ n

theorem Chapter2.Nat.gt_iff_lt (n m : Nat) : n > m ↔ m < n

theorem Chapter2.Nat.le_of_lt {n m : Nat} (hnm : n < m) : n ≤ m

theorem Chapter2.Nat.le_iff_lt_or_eq (n m : Nat) : n ≤ m ↔ n < m ∨ n = m

theorem Chapter2.Nat.succ_gt (n : Nat) : n++ > n

theorem Chapter2.ge_refl (a : Nat) : a ≥ a

Proposition 2.2.12 (Basic properties of order for natural numbers) / Exercise 2.2.3

(a) (Order is reflexive).

theorem Chapter2.ge_trans {a b c : Nat} (hab : a ≥ b) (hbc : b ≥ c) : a ≥ c

(b) (Order is transitive)

theorem Chapter2.ge_antisymm {a b : Nat} (hab : a ≥ b) (hba : b ≥ a) : a = b

(c) (Order is anti-symmetric)

theorem Chapter2.add_ge_add_right (a b c : Nat) : a ≥ b ↔ a + c ≥ b + c

(d) (Addition preserves order)

theorem Chapter2.add_ge_add_left (a b c : Nat) : a ≥ b ↔ c + a ≥ c + b

(d) (Addition preserves order)

theorem Chapter2.add_le_add_right (a b c : Nat) : a ≤ b ↔ a + c ≤ b + c

(d) (Addition preserves order)

theorem Chapter2.add_le_add_left (a b c : Nat) : a ≤ b ↔ c + a ≤ c + b

(d) (Addition preserves order)

theorem Chapter2.lt_iff_succ_le (a b : Nat) : a < b ↔ a++ ≤ b

(e) a < b iff a++ ≤ b.

theorem Chapter2.lt_iff_add_pos (a b : Nat) : a < b ↔ ∃ (d : Nat), d.isPos ∧ b = a + d

(f) a < b if and only if b = a + d for positive d.

theorem Chapter2.ne_of_lt (a b : Nat) : a < b → a ≠ b

If a < b then a ̸= b,

theorem Chapter2.ne_of_gt (a b : Nat) : a > b → a ≠ b

if a > b then a ̸= b.

theorem Chapter2.not_lt_of_gt (a b : Nat) : a < b ∧ a > b → False

If a > b and a < b then contradiction

theorem Chapter2.trichotomous (a b : Nat) : a < b ∨ a = b ∨ a > b

Proposition 2.2.13 (Trichotomy of order for natural numbers) / Exercise 2.2.4

instance Chapter2.Nat.decidableRel : DecidableRel fun (x1 x2 : Nat) => x1 ≤ x2

(Not from textbook) The order is decidable. This exercise is only recommended for Lean experts.

Equations

• Chapter2.Nat.decidableRel = sorry

instance Chapter2.Nat.linearOrder : LinearOrder Nat

(Not from textbook) Nat has the structure of a linear ordering.

Equations

• One or more equations did not get rendered due to their size.

instance Chapter2.Nat.isOrderedAddMonoid : IsOrderedAddMonoid Nat

(Not from textbook) Nat has the structure of an ordered monoid.

theorem Chapter2.strong_induction {m₀ : Nat} {P : Nat → Prop} (hind : ∀ m ≥ m₀, (∀ (m' : Nat), m₀ ≤ m' ∧ m' < m → P m') → P m) (m : Nat) : m ≥ m₀ → P m

Proposition 2.2.14 (Strong principle of induction) / Exercise 2.2.5

theorem Chapter2.backwards_induction {n : Nat} {P : Nat → Prop} (hind : ∀ (m : Nat), P (m++) → P m) (hn : P n) (m : Nat) : m ≤ n → P m

Exercise 2.2.6 (backwards induction)

theorem Chapter2.induction_from {n : Nat} {P : Nat → Prop} (hind : ∀ (m : Nat), P m → P (m++)) : P n → ∀ m ≥ n, P m

Exercise 2.2.7 (induction from a starting point)