Introduction to Real Analysis, Volume I (Jiri Lebl, 2025) -- Chapter 00 -- Section 03 -- Part 4

open scoped BigOperatorssection Chap00section Section03universe u v wvariable {α : Type u} {β : Type v} {γ : Type w}

Definition 0.3.19: For a set Unknown identifier `A`A, a binary relation on Unknown identifier `A`A is a subset Unknown identifier `R`sorry × sorry : Type (max u_1 u_2)R ⊆ Unknown identifier `A`A × Unknown identifier `A`A of ordered pairs where the relation is said to hold; we write Unknown identifier `a`a R b instead of (sorry, sorry) ∈ sorry : Prop(Unknown identifier `a`a, Unknown identifier `b`b) ∈ Unknown identifier `R`R.

abbrev BinaryRelationOn (A : Set α) : Type _ := Set (Subtype A × Subtype A)

The book's binary relations on a set Unknown identifier `A`A correspond to mathlib relations on the subtype of Unknown identifier `A`A.

def binaryRelationOn_equiv_relation (A : Set α) : BinaryRelationOn A ≃ (Subtype A → Subtype A → Prop) := by classical refine { toFun := fun R x y => (x, y) ∈ R invFun := fun r => {p | r p.1 p.2} left_inv := ?_ right_inv := ?_ } · intro R; ext p; rfl · intro r; funext x y; rfl

Example 0.3.20: On the finite set Unknown identifier `A`sorry = {1, 2, 3} : PropA = {1,2,3} the relation corresponds to the set of pairs {(1, 2), (1, 3), (2, 3)} : ?m.20{(1,2), (1,3), (2,3)}, so 1 < 2 : Prop1 < 2 holds but 3 < 1 : Prop3 < 1 does not. The relation is given by {(1, 1), (2, 2), (3, 3)} : ?m.20{(1,1), (2,2), (3,3)}. Any subset of Unknown identifier `A`sorry × sorry : Type (max u_1 u_2)A × Unknown identifier `A`A is a relation; for example satisfies and but not .

def finiteExampleSet : Set ℕ := {x | x = 1 ∨ x = 2 ∨ x = 3}
def exampleLtRelationPairs : Set (ℕ × ℕ) := {p | p = (1, 2) ∨ p = (1, 3) ∨ p = (2, 3)}def exampleEqRelationPairs : Set (ℕ × ℕ) := {p | p = (1, 1) ∨ p = (2, 2) ∨ p = (3, 3)}def daggerRelationPairs : Set (ℕ × ℕ) := {p | p = (1, 2) ∨ p = (2, 1) ∨ p = (2, 3) ∨ p = (3, 1)}theorem example_relation_membership : (1, 2) ∈ exampleLtRelationPairs ∧ (3, 1) ∉ exampleLtRelationPairs ∧ (1, 1) ∈ exampleEqRelationPairs ∧ (3, 3) ∈ exampleEqRelationPairs ∧ (1, 2) ∈ daggerRelationPairs ∧ (3, 1) ∈ daggerRelationPairs ∧ (1, 3) ∉ daggerRelationPairs := by constructor · simp [exampleLtRelationPairs] constructor · simp [exampleLtRelationPairs] constructor · simp [exampleEqRelationPairs] constructor · simp [exampleEqRelationPairs] constructor · simp [daggerRelationPairs] constructor · simp [daggerRelationPairs] · simp [daggerRelationPairs]

Definition 0.3.21: A relation Unknown identifier `R`R on a set Unknown identifier `A`A is (i) reflexive if Unknown identifier `a`a R a for all Unknown identifier `a`sorry ∈ sorry : Propa ∈ Unknown identifier `A`A; (ii) symmetric if Unknown identifier `a`a R b implies Unknown identifier `b`b R a; (iii) transitive if Unknown identifier `a`a R b and Unknown identifier `b`b R c imply Unknown identifier `a`a R c. A relation that is reflexive, symmetric, and transitive is an equivalence relation.

abbrev ReflexiveRelationOn (A : Set α) (R : Subtype A → Subtype A → Prop) : Prop := Reflexive R

The book's reflexive relation on Unknown identifier `A`A is mathlib's Reflexive.{u_1} {α : Sort u_1} (r : α → α → Prop) : PropReflexive predicate on the underlying relation on Subtype sorry : Sort (max 1 u_1)Subtype Unknown identifier `A`A.

theorem reflexiveRelationOn_iff (A : Set α) (R : Subtype A → Subtype A → Prop) : ReflexiveRelationOn A R ↔ Reflexive R := by rfl

The book's symmetric relation on Unknown identifier `A`A is mathlib's Symmetric.{u_1} {α : Sort u_1} (r : α → α → Prop) : PropSymmetric predicate on the underlying relation on Subtype sorry : Sort (max 1 u_1)Subtype Unknown identifier `A`A.

abbrev SymmetricRelationOn (A : Set α) (R : Subtype A → Subtype A → Prop) : Prop := Symmetric R
theorem symmetricRelationOn_iff (A : Set α) (R : Subtype A → Subtype A → Prop) : SymmetricRelationOn A R ↔ Symmetric R := by rfl

The book's transitive relation on Unknown identifier `A`A is mathlib's Transitive.{u_1} {α : Sort u_1} (r : α → α → Prop) : PropTransitive predicate on the underlying relation on Subtype sorry : Sort (max 1 u_1)Subtype Unknown identifier `A`A.

abbrev TransitiveRelationOn (A : Set α) (R : Subtype A → Subtype A → Prop) : Prop := Transitive R
theorem transitiveRelationOn_iff (A : Set α) (R : Subtype A → Subtype A → Prop) : TransitiveRelationOn A R ↔ Transitive R := by rfl

The book's notion of equivalence relation collects reflexivity, symmetry, and transitivity.

abbrev equivalenceRelationOn (A : Set α) (R : Subtype A → Subtype A → Prop) : Prop := ReflexiveRelationOn A R ∧ SymmetricRelationOn A R ∧ TransitiveRelationOn A R

The book's equivalence relations on Unknown identifier `A`A coincide with mathlib's Equivalence.{u} {α : Sort u} (r : α → α → Prop) : PropEquivalence structure for relations on Subtype sorry : Sort (max 1 u_1)Subtype Unknown identifier `A`A.

theorem equivalenceRelationOn_iff_equivalence (A : Set α) (R : Subtype A → Subtype A → Prop) : equivalenceRelationOn A R ↔ Equivalence R := by constructor · rintro ⟨hR, hS, hT⟩ refine ⟨?_, ?_, ?_⟩ · exact hR · intro x y hxy exact hS hxy · intro x y z hxy hyz exact hT hxy hyz · intro h constructor · exact h.refl · constructor · intro x y hxy exact h.symm hxy · intro x y z hxy hyz exact h.trans hxy hyz

Example 0.3.22: On Unknown identifier `A`sorry = {1, 2, 3} : PropA = {1,2,3}, the usual is transitive but neither reflexive nor symmetric. The relation (restricted to Unknown identifier `A`A) given by {(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)} : ?m.47{(1,1),(1,2),(1,3),(2,2),(2,3),(3,3)} is reflexive and transitive but not symmetric. The relation with pairs {(1, 1), (1, 2), (2, 1), (2, 2), (3, 3)} : ?m.38{(1,1),(1,2),(2,1),(2,2),(3,3)} is an equivalence relation.

def exampleRelationLtOnA : Subtype finiteExampleSet → Subtype finiteExampleSet → Prop := fun x y => x.1 < y.1
def exampleRelationLeOnA : Subtype finiteExampleSet → Subtype finiteExampleSet → Prop := fun x y => x.1 ≤ y.1def exampleStarRelation (x y : Subtype finiteExampleSet) : Prop := (x.1 ≤ 2 ∧ y.1 ≤ 2) ∨ (x.1 = 3 ∧ y.1 = 3)

Any element of finiteExampleSet : Set ℕfiniteExampleSet is at most 2 : ℕ2 or equal to 3 : ℕ3.

lemma finiteExampleSet_le2_or_eq3 (x : Subtype finiteExampleSet) : x.1 ≤ 2 ∨ x.1 = 3 := by rcases x.property with hx | hx | hx · left; nlinarith [hx] · left; nlinarith [hx] · right; exact hx
theorem exampleRelationLt_properties : Transitive exampleRelationLtOnA ∧ ¬ Reflexive exampleRelationLtOnA ∧ ¬ Symmetric exampleRelationLtOnA := by refine ⟨?_, ?_, ?_⟩ · intro x y z hxy hyz exact lt_trans hxy hyz · intro h have h1mem : finiteExampleSet 1 := by left; rfl have h1 := h ⟨1, h1mem⟩ exact (lt_irrefl _ h1) · intro h have h1mem : finiteExampleSet 1 := by left; rfl have h2mem : finiteExampleSet 2 := by right; left; rfl have h12 : exampleRelationLtOnA ⟨1, h1mem⟩ ⟨2, h2mem⟩ := by simp [exampleRelationLtOnA] have h21 : (2 : ℕ) < 1 := h h12 have : ¬ (2 : ℕ) < 1 := by decide exact this h21theorem exampleRelationLe_properties : Reflexive exampleRelationLeOnA ∧ Transitive exampleRelationLeOnA ∧ ¬ Symmetric exampleRelationLeOnA := by refine ⟨?_, ?_, ?_⟩ · intro x simp [exampleRelationLeOnA] · intro x y z hxy hyz exact le_trans hxy hyz · intro h have h1mem : finiteExampleSet 1 := by left; rfl have h2mem : finiteExampleSet 2 := by right; left; rfl have h12 : exampleRelationLeOnA ⟨1, h1mem⟩ ⟨2, h2mem⟩ := by simp [exampleRelationLeOnA] have h21 : (2 : ℕ) ≤ 1 := h h12 have : ¬ (2 : ℕ) ≤ 1 := by decide exact this h21theorem exampleStarRelation_equivalence : Equivalence exampleStarRelation := by refine ⟨?_, ?_, ?_⟩ · intro x rcases finiteExampleSet_le2_or_eq3 x with hx | hx · left; exact ⟨hx, hx⟩ · right; exact ⟨hx, hx⟩ · intro x y hxy rcases hxy with ⟨hx, hy⟩ | ⟨hx, hy⟩ · left; exact ⟨hy, hx⟩ · right; exact ⟨hy, hx⟩ · intro x y z hxy hyz rcases hxy with ⟨hx2, hy2⟩ | ⟨hx3, hy3⟩ · rcases hyz with ⟨hy2', hz2⟩ | ⟨hy3', hz3⟩ · left; exact ⟨hx2, hz2⟩ · have : False := by have hnot : ¬ (3 : ℕ) ≤ 2 := by decide exact hnot (by simp [hy3'] at hy2) exact this.elim · rcases hyz with ⟨hy2', hz2⟩ | ⟨hy3', hz3⟩ · have : False := by have hnot : ¬ (3 : ℕ) ≤ 2 := by decide exact hnot (by simp [hy3] at hy2') exact this.elim · right; exact ⟨hx3, hz3⟩

Definition 0.3.23: For a set Unknown identifier `A`A with an equivalence relation Unknown identifier `R`R and an element Unknown identifier `a`sorry ∈ sorry : Propa ∈ Unknown identifier `A`A, the equivalence class of Unknown identifier `a`a, denoted [sorry] : List ?m.2[Unknown identifier `a`a], is the set {x | x ∈ sorry ∧ sorry} : Set ?m.1{ x ∈ Unknown identifier `A`A | Unknown identifier `a`a R x }.

def equivalenceClass (A : Set α) (R : Subtype A → Subtype A → Prop) (a : Subtype A) : Set (Subtype A) := {x | R a x}

The book's equivalence class agrees with the class coming from the Setoid.{u} (α : Sort u) : Sort (max 1 u)Setoid built from the equivalence relation Unknown identifier `R`R on Unknown identifier `A`A.

theorem equivalenceClass_eq_setoid_r (A : Set α) (R : Subtype A → Subtype A → Prop) (hR : Equivalence R) (a : Subtype A) : equivalenceClass A R a = {x : Subtype A | ({ r := R, iseqv := hR } : Setoid (Subtype A)).r a x} := by rfl

Proposition 0.3.24: If Unknown identifier `R`R is an equivalence relation on Unknown identifier `A`A, then every Unknown identifier `a`sorry ∈ sorry : Propa ∈ Unknown identifier `A`A lies in exactly one equivalence class. Moreover, Unknown identifier `a`a R b if and only if [sorry] = [sorry] : Prop[Unknown identifier `a`a] = [Unknown identifier `b`b].

theorem equivalenceClass_unique (A : Set α) (R : Subtype A → Subtype A → Prop) (hR : Equivalence R) (a : Subtype A) : a ∈ equivalenceClass A R a ∧ ∀ b : Subtype A, a ∈ equivalenceClass A R b → equivalenceClass A R b = equivalenceClass A R a := by constructor · exact hR.refl a · intro b hab apply Set.ext intro x constructor · intro hx have hba : R a b := hR.symm hab exact hR.trans hba hx · intro hx exact hR.trans hab hx
theorem related_iff_equivalenceClass_eq (A : Set α) (R : Subtype A → Subtype A → Prop) (hR : Equivalence R) (a b : Subtype A) : R a b ↔ equivalenceClass A R a = equivalenceClass A R b := by constructor · intro h apply Set.ext intro x constructor · intro hx have hba : R b a := hR.symm h exact hR.trans hba hx · intro hx exact hR.trans h hx · intro h have ha : a ∈ equivalenceClass A R a := hR.refl a have : a ∈ equivalenceClass A R b := by simpa [h] using ha exact hR.symm this

Example 0.3.25: Rational numbers can be presented as equivalence classes of pairs (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `a`a, Unknown identifier `b`b) with failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `a`a ∈ ℤ and a positive failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `b`b ∈ ℕ under the relation when Unknown identifier `a`sorry * sorry = sorry * sorry : Propa * Unknown identifier `d`d = Unknown identifier `b`b * Unknown identifier `c`c. The class of (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `a`a, Unknown identifier `b`b) is typically written Unknown identifier `a`sorry / sorry : ?m.5a / Unknown identifier `b`b.

def RatPair : Type := {p : ℤ × ℕ // 0 < p.2}
def ratPairRel (p q : RatPair) : Prop := p.1.1 * (q.1.2 : ℤ) = q.1.1 * (p.1.2 : ℤ)

The relation used to define rationals as pairs is an equivalence relation.

theorem ratPairRel_equivalence : Equivalence ratPairRel := by refine ⟨?_, ?_, ?_⟩ · intro p dsimp [ratPairRel] · intro p q h simpa [ratPairRel] using Eq.symm h · intro p q r h1 h2 dsimp [ratPairRel] at h1 h2 ⊢ have h1' := congrArg (fun t => t * (r.1.2 : ℤ)) h1 have h2' := congrArg (fun t => t * (p.1.2 : ℤ)) h2 have h2'' : q.1.1 * (p.1.2 : ℤ) * (r.1.2 : ℤ) = r.1.1 * (q.1.2 : ℤ) * (p.1.2 : ℤ) := by simpa [mul_comm, mul_left_comm, mul_assoc] using h2' have h : p.1.1 * (q.1.2 : ℤ) * (r.1.2 : ℤ) = r.1.1 * (q.1.2 : ℤ) * (p.1.2 : ℤ) := by calc p.1.1 * (q.1.2 : ℤ) * (r.1.2 : ℤ) = q.1.1 * (p.1.2 : ℤ) * (r.1.2 : ℤ) := h1' _ = r.1.1 * (q.1.2 : ℤ) * (p.1.2 : ℤ) := h2'' have hq : (q.1.2 : ℤ) ≠ 0 := by exact_mod_cast (ne_of_gt q.2) exact mul_left_cancel₀ hq (by simpa [mul_comm, mul_left_comm, mul_assoc] using h)

The setoid of rational-number representatives as pairs of an integer and a natural number with positive denominator.

def ratPairSetoid : Setoid RatPair := { r := ratPairRel iseqv := ratPairRel_equivalence }

Rational numbers as the quotient of integer–natural pairs by the relation when Unknown identifier `a`sorry * sorry = sorry * sorry : Propa * Unknown identifier `d`d = Unknown identifier `b`b * Unknown identifier `c`c.

abbrev rationalNumbersQuot : Type := Quot ratPairSetoid

Interpret a numerator–denominator pair as a rational number.

def ratPairToRat (p : RatPair) : ℚ := (p.1.1 : ℚ) / (p.1.2 : ℚ)

Cross-multiplication characterizes when two pairs represent the same rational.

lemma ratPairRel_iff_toRat_eq (p q : RatPair) : ratPairRel p q ↔ ratPairToRat p = ratPairToRat q := by constructor · intro h have hp : (p.1.2 : ℚ) ≠ 0 := by exact_mod_cast (ne_of_gt p.2) have hq : (q.1.2 : ℚ) ≠ 0 := by exact_mod_cast (ne_of_gt q.2) have h' : (p.1.1 : ℚ) * q.1.2 = (q.1.1 : ℚ) * p.1.2 := by exact_mod_cast h dsimp [ratPairToRat] field_simp [hp, hq] simpa [mul_comm] using h' · intro h have hp : (p.1.2 : ℚ) ≠ 0 := by exact_mod_cast (ne_of_gt p.2) have hq : (q.1.2 : ℚ) ≠ 0 := by exact_mod_cast (ne_of_gt q.2) dsimp [ratPairToRat] at h field_simp [hp, hq] at h norm_cast at h simpa [ratPairRel, mul_comm] using h

The quotient of integer–natural pairs is equivalent to mathlib's rationals ℚ : Typeℚ.

noncomputable def rationalNumbersQuot_equiv_rat : rationalNumbersQuot ≃ ℚ := by classical refine { toFun := Quot.lift ratPairToRat (fun p q h => (ratPairRel_iff_toRat_eq p q).1 h) invFun := fun q => Quot.mk _ ⟨(q.num, q.den), by have h := Rat.den_pos q simpa using h⟩ left_inv := ?_ right_inv := ?_ } · intro x refine Quot.induction_on x ?_ intro p apply Quot.sound have h : ratPairToRat ⟨((ratPairToRat p).num, (ratPairToRat p).den), by have h := Rat.den_pos (ratPairToRat p) simpa using h⟩ = ratPairToRat p := by simpa [ratPairToRat] using (Rat.num_div_den (ratPairToRat p)) exact (ratPairRel_iff_toRat_eq _ _).2 h · intro q simp [ratPairToRat, Rat.num_div_den]
end Section03end Chap00