@[reducible, inline]

abbrev BinaryRelationOn {α : Type u} (A : Set α) : Type u

Definition 0.3.19: For a set A, a binary relation on A is a subset R ⊆ A × A of ordered pairs where the relation is said to hold; we write a R b instead of (a, b) ∈ R.

Equations

• BinaryRelationOn A = Set (Subtype A × Subtype A)

def binaryRelationOn_equiv_relation {α : Type u} (A : Set α) : BinaryRelationOn A ≃ (Subtype A → Subtype A → Prop)

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

Equations

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

def finiteExampleSet : Set ℕ

Example 0.3.20: On the finite set A = {1,2,3} the relation < corresponds to the set of pairs {(1,2), (1,3), (2,3)}, so 1 < 2 holds but 3 < 1 does not. The relation = is given by {(1,1), (2,2), (3,3)}. Any subset of A × A is a relation; for example † = {(1,2), (2,1), (2,3), (3,1)} satisfies 1 † 2 and 3 † 1 but not 1 † 3.

Equations

• finiteExampleSet = {x : ℕ | x = 1 ∨ x = 2 ∨ x = 3}

def exampleLtRelationPairs : Set (ℕ × ℕ)

Equations

• exampleLtRelationPairs = {p : ℕ × ℕ | p = (1, 2) ∨ p = (1, 3) ∨ p = (2, 3)}

def exampleEqRelationPairs : Set (ℕ × ℕ)

Equations

• exampleEqRelationPairs = {p : ℕ × ℕ | p = (1, 1) ∨ p = (2, 2) ∨ p = (3, 3)}

def daggerRelationPairs : Set (ℕ × ℕ)

Equations

• daggerRelationPairs = {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

@[reducible, inline]

abbrev ReflexiveRelationOn {α : Type u} (A : Set α) (R : Subtype A → Subtype A → Prop) : Prop

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

Equations

• ReflexiveRelationOn A R = Reflexive R

theorem reflexiveRelationOn_iff {α : Type u} (A : Set α) (R : Subtype A → Subtype A → Prop) : ReflexiveRelationOn A R ↔ Reflexive R

The book's reflexive relation on A is mathlib's Reflexive predicate on the underlying relation on Subtype A.

@[reducible, inline]

abbrev SymmetricRelationOn {α : Type u} (A : Set α) (R : Subtype A → Subtype A → Prop) : Prop

The book's symmetric relation on A is mathlib's Symmetric predicate on the underlying relation on Subtype A.

Equations

• SymmetricRelationOn A R = Symmetric R

theorem symmetricRelationOn_iff {α : Type u} (A : Set α) (R : Subtype A → Subtype A → Prop) : SymmetricRelationOn A R ↔ Symmetric R

@[reducible, inline]

abbrev TransitiveRelationOn {α : Type u} (A : Set α) (R : Subtype A → Subtype A → Prop) : Prop

The book's transitive relation on A is mathlib's Transitive predicate on the underlying relation on Subtype A.

Equations

• TransitiveRelationOn A R = Transitive R

theorem transitiveRelationOn_iff {α : Type u} (A : Set α) (R : Subtype A → Subtype A → Prop) : TransitiveRelationOn A R ↔ Transitive R

@[reducible, inline]

abbrev equivalenceRelationOn {α : Type u} (A : Set α) (R : Subtype A → Subtype A → Prop) : Prop

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

Equations

• equivalenceRelationOn A R = (ReflexiveRelationOn A R ∧ SymmetricRelationOn A R ∧ TransitiveRelationOn A R)

theorem equivalenceRelationOn_iff_equivalence {α : Type u} (A : Set α) (R : Subtype A → Subtype A → Prop) : equivalenceRelationOn A R ↔ Equivalence R

The book's equivalence relations on A coincide with mathlib's Equivalence structure for relations on Subtype A.

def exampleRelationLtOnA : Subtype finiteExampleSet → Subtype finiteExampleSet → Prop

Example 0.3.22: On A = {1,2,3}, the usual < is transitive but neither reflexive nor symmetric. The relation ≤ (restricted to A) given by {(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)} is an equivalence relation.

Equations

• exampleRelationLtOnA x y = (↑x < ↑y)

def exampleRelationLeOnA : Subtype finiteExampleSet → Subtype finiteExampleSet → Prop

Equations

• exampleRelationLeOnA x y = (↑x ≤ ↑y)

def exampleStarRelation (x y : Subtype finiteExampleSet) : Prop

Equations

• exampleStarRelation x y = (↑x ≤ 2 ∧ ↑y ≤ 2 ∨ ↑x = 3 ∧ ↑y = 3)

theorem finiteExampleSet_le2_or_eq3 (x : Subtype finiteExampleSet) : ↑x ≤ 2 ∨ ↑x = 3

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

theorem exampleRelationLt_properties : Transitive exampleRelationLtOnA ∧ ¬Reflexive exampleRelationLtOnA ∧ ¬Symmetric exampleRelationLtOnA

theorem exampleRelationLe_properties : Reflexive exampleRelationLeOnA ∧ Transitive exampleRelationLeOnA ∧ ¬Symmetric exampleRelationLeOnA

theorem exampleStarRelation_equivalence : Equivalence exampleStarRelation

def equivalenceClass {α : Type u} (A : Set α) (R : Subtype A → Subtype A → Prop) (a : Subtype A) : Set (Subtype A)

Definition 0.3.23: For a set A with an equivalence relation R and an element a ∈ A, the equivalence class of a, denoted [a], is the set { x ∈ A | a R x }.

Equations

• equivalenceClass A R a = {x : Subtype A | R a x}

theorem equivalenceClass_eq_setoid_r {α : Type u} (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 } a x}

The book's equivalence class agrees with the class coming from the Setoid built from the equivalence relation R on A.

theorem equivalenceClass_unique {α : Type u} (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

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

theorem related_iff_equivalenceClass_eq {α : Type u} (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

def RatPair : Type

Example 0.3.25: Rational numbers can be presented as equivalence classes of pairs (a, b) with a ∈ ℤ and a positive b ∈ ℕ under the relation (a, b) ∼ (c, d) when a * d = b * c. The class of (a, b) is typically written a / b.

Equations

• RatPair = { p : ℤ × ℕ // 0 < p.2 }

def ratPairRel (p q : RatPair) : Prop

Equations

• ratPairRel p q = ((↑p).1 * ↑(↑q).2 = (↑q).1 * ↑(↑p).2)

theorem ratPairRel_equivalence : Equivalence ratPairRel

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

def ratPairSetoid : Setoid RatPair

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

Equations

• ratPairSetoid = { r := ratPairRel, iseqv := ratPairRel_equivalence }

@[reducible, inline]

abbrev rationalNumbersQuot : Type

Rational numbers as the quotient of integer–natural pairs by the relation (a, b) ∼ (c, d) when a * d = b * c.

Equations

• rationalNumbersQuot = Quot ⇑ratPairSetoid

def ratPairToRat (p : RatPair) : ℚ

Interpret a numerator–denominator pair as a rational number.

Equations

• ratPairToRat p = ↑(↑p).1 / ↑(↑p).2

theorem ratPairRel_iff_toRat_eq (p q : RatPair) : ratPairRel p q ↔ ratPairToRat p = ratPairToRat q

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

noncomputable def rationalNumbersQuot_equiv_rat : rationalNumbersQuot ≃ ℚ

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

Equations

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