Analysis I, Section 4.1

This file is a translation of Section 4.1 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 the "Section 4.1" integers, Section_4_1.Int, as formal differences a —— b of natural numbers a b:ℕ, up to equivalence. (This is a quotient of a scaffolding type Section_4_1.PreInt, which consists of formal differences without any equivalence imposed.)

• ring operations and order these integers, as well as an embedding of ℕ

• Equivalence with the Mathlib integers _root_.Int (or ℤ), which we will use going forward.

structure Section_4_1.PreInt : Type

• minuend : ℕ
• subtrahend : ℕ

instance Section_4_1.PreInt.instSetoid : Setoid PreInt

Definition 4.1.1

Equations

• Section_4_1.PreInt.instSetoid = { r := fun (a b : Section_4_1.PreInt) => a.minuend + b.subtrahend = b.minuend + a.subtrahend, iseqv := Section_4_1.PreInt.instSetoid._proof_1 }

@[simp]

theorem Section_4_1.PreInt.eq (a b c d : ℕ) : { minuend := a, subtrahend := b } ≈ { minuend := c, subtrahend := d } ↔ a + d = c + b

@[reducible, inline]

abbrev Section_4_1.Int : Type

Equations

• Section_4_1.Int = Quotient Section_4_1.PreInt.instSetoid

@[reducible, inline]

abbrev Section_4_1.Int.formalDiff (a b : ℕ) : Int

Equations

• a —— b = ⟦{ minuend := a, subtrahend := b }⟧

def Section_4_1.«term_——_» : Lean.TrailingParserDescr

Equations

• Section_4_1.«term_——_» = Lean.ParserDescr.trailingNode `Section_4_1.«term_——_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " —— ") (Lean.ParserDescr.cat `term 101))

theorem Section_4_1.Int.eq (a b c d : ℕ) : a —— b = c —— d ↔ a + d = c + b

Definition 4.1.1 (Integers)

theorem Section_4_1.Int.eq_diff (n : Int) : ∃ (a : ℕ) (b : ℕ), n = a —— b

Definition 4.1.1 (Integers)

instance Section_4_1.Int.instAdd : Add Int

Lemma 4.1.3 (Addition well-defined)

Equations

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

theorem Section_4_1.Int.add_eq (a b c d : ℕ) : a —— b + c —— d = (a + c) —— (b + d)

Definition 4.1.2 (Definition of addition)

theorem Section_4_1.Int.mul_congr_left (a b a' b' c d : ℕ) (h : a —— b = a' —— b') : (a * c + b * d) —— (a * d + b * c) = (a' * c + b' * d) —— (a' * d + b' * c)

Lemma 4.1.3 (Multiplication well-defined)

theorem Section_4_1.Int.mul_congr_right (a b c d c' d' : ℕ) (h : c —— d = c' —— d') : (a * c + b * d) —— (a * d + b * c) = (a * c' + b * d') —— (a * d' + b * c')

Lemma 4.1.3 (Multiplication well-defined)

theorem Section_4_1.Int.mul_congr {a b c d a' b' c' d' : ℕ} (h1 : a —— b = a' —— b') (h2 : c —— d = c' —— d') : (a * c + b * d) —— (a * d + b * c) = (a' * c' + b' * d') —— (a' * d' + b' * c')

Lemma 4.1.3 (Multiplication well-defined)

instance Section_4_1.Int.instMul : Mul Int

Equations

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

theorem Section_4_1.Int.mul_eq (a b c d : ℕ) : a —— b * c —— d = (a * c + b * d) —— (a * d + b * c)

Definition 4.1.2 (Multiplication of integers)

instance Section_4_1.Int.instOfNat {n : ℕ} : OfNat Int n

Equations

• Section_4_1.Int.instOfNat = { ofNat := n —— 0 }

instance Section_4_1.Int.instNatCast : NatCast Int

Equations

• Section_4_1.Int.instNatCast = { natCast := fun (n : ℕ) => n —— 0 }

theorem Section_4_1.Int.ofNat_eq (n : ℕ) : OfNat.ofNat n = n —— 0

theorem Section_4_1.Int.natCast_eq (n : ℕ) : ↑n = n —— 0

@[simp]

theorem Section_4_1.Int.natCast_ofNat (n : ℕ) : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Section_4_1.Int.ofNat_inj (n m : ℕ) : OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m

@[simp]

theorem Section_4_1.Int.natCast_inj (n m : ℕ) : ↑n = ↑m ↔ n = m

instance Section_4_1.Int.instNeg : Neg Int

Definition 4.1.4 (Negation of integers) / Exercise 4.1.2

Equations

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

theorem Section_4_1.Int.neg_eq (a b : ℕ) : -a —— b = b —— a

@[reducible, inline]

abbrev Section_4_1.Int.isPos (x : Int) : Prop

Equations

• x.isPos = ∃ n > 0, x = ↑n

@[reducible, inline]

abbrev Section_4_1.Int.isNeg (x : Int) : Prop

Equations

• x.isNeg = ∃ n > 0, x = -↑n

theorem Section_4_1.Int.trichotomous (x : Int) : x = 0 ∨ x.isPos ∨ x.isNeg

Lemma 4.1.5 (trichotomy of integers )

theorem Section_4_1.Int.not_pos_zero (x : Int) : x = 0 ∧ x.isPos → False

Lemma 4.1.5 (trichotomy of integers)

theorem Section_4_1.Int.not_neg_zero (x : Int) : x = 0 ∧ x.isNeg → False

Lemma 4.1.5 (trichotomy of integers)

theorem Section_4_1.Int.not_pos_neg (x : Int) : x.isPos ∧ x.isNeg → False

Lemma 4.1.5 (trichotomy of integers)

instance Section_4_1.Int.instAddGroup : AddGroup Int

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

Equations

• Section_4_1.Int.instAddGroup = AddGroup.ofLeftAxioms Section_4_1.Int.instAddGroup._proof_8 Section_4_1.Int.instAddGroup._proof_9 Section_4_1.Int.instAddGroup._proof_10

instance Section_4_1.Int.instAddCommGroup : AddCommGroup Int

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

Equations

• Section_4_1.Int.instAddCommGroup = { toAddGroup := Section_4_1.Int.instAddGroup, add_comm := Section_4_1.Int.instAddCommGroup._proof_11 }

instance Section_4_1.Int.instCommMonoid : CommMonoid Int

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

Equations

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

instance Section_4_1.Int.instCommRing : CommRing Int

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

Equations

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

theorem Section_4_1.Int.sub_eq (a b : Int) : a - b = a + -b

Definition of subtraction

theorem Section_4_1.Int.sub_eq_formal_sub (a b : ℕ) : ↑a - ↑b = a —— b

theorem Section_4_1.Int.mul_eq_zero {a b : Int} (h : a * b = 0) : a = 0 ∨ b = 0

Proposition 4.1.8 (No zero divisors) / Exercise 4.1.5

theorem Section_4_1.Int.mul_right_cancel₀ (a b c : Int) (h : a * c = b * c) (hc : c ≠ 0) : a = b

Corollary 4.1.9 (Cancellation law) / Exercise 4.1.6

instance Section_4_1.Int.instLE : LE Int

Definition 4.1.10 (Ordering of the integers)

Equations

• Section_4_1.Int.instLE = { le := fun (n m : Section_4_1.Int) => ∃ (a : ℕ), m = n + ↑a }

instance Section_4_1.Int.instLT : LT Int

Definition 4.1.10 (Ordering of the integers)

Equations

• Section_4_1.Int.instLT = { lt := fun (n m : Section_4_1.Int) => (∃ (a : ℕ), m = n + ↑a) ∧ n ≠ m }

theorem Section_4_1.Int.le_iff (n m : Int) : n ≤ m ↔ ∃ (a : ℕ), m = n + ↑a

theorem Section_4_1.Int.lt_iff (n m : Int) : n < m ↔ (∃ (a : ℕ), m = n + ↑a) ∧ n ≠ m

theorem Section_4_1.Int.gt_iff (a b : Int) : a > b ↔ ∃ (n : ℕ), n ≠ 0 ∧ a = b + ↑n

Lemma 4.1.11(a) (Properties of order) / Exercise 4.1.7

theorem Section_4_1.Int.add_gt_add_right {a b : Int} (c : Int) (h : a > b) : a + c > b + c

Lemma 4.1.11(b) (Addition preserves order) / Exercise 4.1.7

theorem Section_4_1.Int.mul_lt_mul_of_pos_left {a b c : Int} (hab : a > b) (hc : c > 0) : a * c > b * c

Lemma 4.1.11(c) (Positive multiplication preserves order) / Exercise 4.1.7

theorem Section_4_1.Int.neg_gt_neg {a b : Int} (h : a > b) : -a < -b

Lemma 4.1.11(d) (Negation reverses order) / Exercise 4.1.7

theorem Section_4_1.Int.gt_trans {a b c : Int} (hab : a > b) (hbc : b > c) : a > c

Lemma 4.1.11(e) (Order is transitive) / Exercise 4.1.7

theorem Section_4_1.Int.trichotomous' (a b c : Int) : a > b ∨ a < b ∨ a = b

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

theorem Section_4_1.Int.not_gt_and_lt (a b : Int) : ¬(a > b ∧ a < b)

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

theorem Section_4_1.Int.not_gt_and_eq (a b : Int) : ¬(a > b ∧ a = b)

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

theorem Section_4_1.Int.not_lt_and_eq (a b : Int) : ¬(a < b ∧ a = b)

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

instance Section_4_1.Int.decidableRel : DecidableRel fun (x1 x2 : Int) => x1 ≤ x2

(Not from textbook) The order is decidable. This exercise is only recommended for Lean experts. Alternatively, one can establish this fact in classical logic via classical; exact Classical.decRel _.

Equations

• Section_4_1.Int.decidableRel = sorry

instance Section_4_1.Int.instLinearOrder : LinearOrder Int

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

Equations

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

theorem Section_4_1.Int.neg_one_mul (a : Int) : -1 * a = -a

Exercise 4.1.3

theorem Section_4_1.Int.no_induction : ∃ (P : Int → Prop), P 0 ∧ ∀ (n : Int), P n → P (n + 1) ∧ ¬∀ (n : Int), P n

Exercise 4.1.8

theorem Section_4_1.Int.sq_nonneg (n : Int) : n * n ≥ 0

Exercise 4.1.9

theorem Section_4_1.Int.sq_nonneg' (n : Int) : ∃ (m : ℕ), n * n = ↑m

Exercise 4.1.9

@[reducible, inline]

abbrev Section_4_1.Int.equivInt : Int ≃ ℤ

Not in textbook: create an equivalence between Int and ℤ. This requires some familiarity with the API for Mathlib's version of the integers.

Equations

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

@[reducible, inline]

abbrev Section_4_1.Int.equivInt_order : Int ≃o ℤ

Not in textbook: equivalence preserves order

Equations

• Section_4_1.Int.equivInt_order = { toEquiv := Section_4_1.Int.equivInt, map_rel_iff' := @Section_4_1.Int.equivInt_order._proof_47 }

@[reducible, inline]

abbrev Section_4_1.Int.equivInt_ring : Int ≃+* ℤ

Not in textbook: equivalence preserves ring operations

Equations

• Section_4_1.Int.equivInt_ring = { toEquiv := Section_4_1.Int.equivInt, map_mul' := Section_4_1.Int.equivInt_ring._proof_48, map_add' := Section_4_1.Int.equivInt_ring._proof_49 }