Enderton.Set.Relation

A representation of a relation, i.e. a set of ordered pairs. Like Set, it is assumed a relation is homogeneous.

@[inline, reducible]

abbrev Set.HRelation (α : Type) (β : Type) : Type

A relation type as defined by Enderton.

We choose to use tuples to represent our ordered pairs, as opposed to Kuratowski's definition of a set.

Not to be confused with the Lean-provided Rel.

Equations

• Set.HRelation α β = Set (α × β)

@[inline, reducible]

abbrev Set.Relation (α : Type) : Type

A homogeneous variant of the HRelation type.

Equations

• Set.Relation α = Set.HRelation α α

Domain and Range

def Set.Relation.dom {α : Type} {β : Type} (R : Set.HRelation α β) : Set α

The domain of a Relation.

Equations

• Set.Relation.dom R = Prod.fst '' R

theorem Set.Relation.mem_pair_imp_fst_mem_dom {α : Type} {β : Type} {x : α} {y : β} {R : Set.HRelation α β} (h : (x, y) ∈ R) : x ∈ Set.Relation.dom R

The first component of any pair in a Relation must be a member of the Relation's domain.

theorem Set.Relation.dom_exists {α : Type} {β : Type} {x : α} {R : Set.HRelation α β} (hx : x ∈ Set.Relation.dom R) : ∃ (y : β), (x, y) ∈ R

If x ∈ dom R, there exists some y such that ⟨x, y⟩ ∈ R.

def Set.Relation.ran {α : Type} {β : Type} (R : Set.HRelation α β) : Set β

The range of a Relation.

Equations

• Set.Relation.ran R = Prod.snd '' R

theorem Set.Relation.mem_pair_imp_snd_mem_ran {α : Type} {β : Type} {x : α} {y : β} {R : Set.HRelation α β} (h : (x, y) ∈ R) : y ∈ Set.Relation.ran R

theorem Set.Relation.ran_exists {α : Type} {β : Type} {x : β} {R : Set.HRelation α β} (hx : x ∈ Set.Relation.ran R) : ∃ (t : α), (t, x) ∈ R

If x ∈ ran R, there exists some t such that ⟨t, x⟩ ∈ R.

def Set.Relation.fld {α : Type} (R : Set.Relation α) : Set α

The field of a Relation.

Equations

• Set.Relation.fld R = Set.Relation.dom R ∪ Set.Relation.ran R

def Set.Relation.inv {α : Type} {β : Type} (R : Set.HRelation α β) : Set.HRelation β α

The inverse of a Relation.

Equations

• Set.Relation.inv R = {x : β × α | ∃ p ∈ R, (p.2, p.1) = x}

@[simp]

theorem Set.Relation.mem_self_comm_mem_inv {α : Type} {β : Type} {y : β} {x : α} {R : Set.HRelation α β} : (y, x) ∈ Set.Relation.inv R ↔ (x, y) ∈ R

(x, y) is a member of relation R iff (y, x) is a member of R⁻¹.

@[simp]

theorem Set.Relation.inv_inv_eq_self {α : Type} {β : Type} (R : Set.HRelation α β) : Set.Relation.inv (Set.Relation.inv R) = R

The inverse of the inverse of a Relation is the Relation.

@[simp]

theorem Set.Relation.dom_inv_eq_ran_self {α : Type} {β : Type} {F : Set.HRelation α β} : Set.Relation.dom (Set.Relation.inv F) = Set.Relation.ran F

For a set F, dom F⁻¹ = ran F.

@[simp]

theorem Set.Relation.ran_inv_eq_dom_self {α : Type} {β : Type} {F : Set.HRelation α β} : Set.Relation.ran (Set.Relation.inv F) = Set.Relation.dom F

For a set F, ran F⁻¹ = dom F.

Restriction

def Set.Relation.restriction {α : Type} {β : Type} (R : Set.HRelation α β) (A : Set α) : Set.HRelation α β

The restriction of a Relation to a Set.

Equations

• Set.Relation.restriction R A = {p : α × β | p ∈ R ∧ p.1 ∈ A}

Image

def Set.Relation.image {α : Type} {β : Type} (R : Set.HRelation α β) (A : Set α) : Set β

The image of a Relation under a Set.

Equations

• Set.Relation.image R A = {y : β | ∃ u ∈ A, (u, y) ∈ R}

Single-Rooted and Single-Valued

def Set.Relation.isSingleRooted {α : Type} {β : Type} (R : Set.HRelation α β) : Prop

A Relation R is said to be single-rooted iff for all y ∈ ran R, there exists exactly one x such that ⟨x, y⟩ ∈ R.

Equations

• Set.Relation.isSingleRooted R = ∀ y ∈ Set.Relation.ran R, ∃! (x : α), x ∈ Set.Relation.dom R ∧ (x, y) ∈ R

theorem Set.Relation.single_rooted_eq_unique {α : Type} {β : Type} {R : Set.HRelation α β} {x₁ : α} {x₂ : α} {y : β} (hR : Set.Relation.isSingleRooted R) : (x₁, y) ∈ R → (x₂, y) ∈ R → x₁ = x₂

A single-rooted Relation should map the same output to the same input.

def Set.Relation.isSingleValued {α : Type} {β : Type} (R : Set.HRelation α β) : Prop

A Relation R is said to be single-valued iff for all x ∈ dom R, there exists exactly one y such that ⟨x, y⟩ ∈ R.

Notice, a Relation that is single-valued is a function.

Equations

• Set.Relation.isSingleValued R = ∀ x ∈ Set.Relation.dom R, ∃! (y : β), y ∈ Set.Relation.ran R ∧ (x, y) ∈ R

theorem Set.Relation.single_valued_eq_unique {α : Type} {β : Type} {R : Set.HRelation α β} {x : α} {y₁ : β} {y₂ : β} (hR : Set.Relation.isSingleValued R) : (x, y₁) ∈ R → (x, y₂) ∈ R → y₁ = y₂

A single-valued Relation should map the same input to the same output.

theorem Set.Relation.single_valued_inv_iff_single_rooted_self {α : Type} {β : Type} {F : Set.HRelation α β} : Set.Relation.isSingleValued (Set.Relation.inv F) ↔ Set.Relation.isSingleRooted F

For a set F, F⁻¹ is a function iff F is single-rooted.

theorem Set.Relation.single_valued_self_iff_single_rooted_inv {α : Type} {β : Type} {F : Set.HRelation α β} : Set.Relation.isSingleValued F ↔ Set.Relation.isSingleRooted (Set.Relation.inv F)

For a relation F, F is a function iff F⁻¹ is single-rooted.

theorem Set.Relation.single_valued_subset {α : Type} {β : Type} {F : Set.HRelation α β} {G : Set.HRelation α β} (hG : Set.Relation.isSingleValued G) (h : F ⊆ G) : Set.Relation.isSingleValued F

The subset of a function must also be a function.

Injections

def Set.Relation.isOneToOne {α : Type} {β : Type} (R : Set.HRelation α β) : Prop

A Relation R is one-to-one if it is a single-rooted function.

Equations

• Set.Relation.isOneToOne R = (Set.Relation.isSingleValued R ∧ Set.Relation.isSingleRooted R)

theorem Set.Relation.one_to_one_self_iff_one_to_one_inv {α : Type} {β : Type} {R : Set.HRelation α β} : Set.Relation.isOneToOne R ↔ Set.Relation.isOneToOne (Set.Relation.inv R)

A Relation is one-to-one iff it's inverse is.

Surjections

structure Set.Relation.mapsInto {α : Type} {β : Type} (F : Set.HRelation α β) (A : Set α) (B : Set β) : Prop

Indicates Relation F is a function from A to B.

This is usually denoted as F : A → B.

• is_func : Set.Relation.isSingleValued F
• dom_eq : Set.Relation.dom F = A
• ran_ss : Set.Relation.ran F ⊆ B

structure Set.Relation.mapsOnto {α : Type} {β : Type} (F : Set.HRelation α β) (A : Set α) (B : Set β) : Prop

Indicates Relation F is a function from A to ran F = B.

• is_func : Set.Relation.isSingleValued F
• dom_eq : Set.Relation.dom F = A
• ran_eq : Set.Relation.ran F = B

Composition

def Set.Relation.comp {β : Type} {γ : Type} {α : Type} (F : Set.HRelation β γ) (G : Set.HRelation α β) : Set.HRelation α γ

The composition of two Relations.

Equations

• Set.Relation.comp F G = {p : α × γ | ∃ (t : β), (p.1, t) ∈ G ∧ (t, p.2) ∈ F}

theorem Set.Relation.dom_comp_imp_dom_self {β : Type} {γ : Type} {α : Type} {x : α} {F : Set.HRelation β γ} {G : Set.HRelation α β} : x ∈ Set.Relation.dom (Set.Relation.comp F G) → x ∈ Set.Relation.dom G

If x ∈ dom (F ∘ G), then x ∈ dom G.

theorem Set.Relation.ran_comp_imp_ran_self {β : Type} {γ : Type} {α : Type} {y : γ} {F : Set.HRelation β γ} {G : Set.HRelation α β} : y ∈ Set.Relation.ran (Set.Relation.comp F G) → y ∈ Set.Relation.ran F

If y ∈ ran (F ∘ G), then y ∈ ran F.

theorem Set.Relation.comp_assoc {γ : Type} {δ : Type} {β : Type} {α : Type} {R : Set.HRelation γ δ} {S : Set.HRelation β γ} {T : Set.HRelation α β} : Set.Relation.comp (Set.Relation.comp R S) T = Set.Relation.comp R (Set.Relation.comp S T)

Composition of functions is associative.

theorem Set.Relation.single_valued_comp_is_single_valued {β : Type} {γ : Type} {α : Type} {F : Set.HRelation β γ} {G : Set.HRelation α β} (hF : Set.Relation.isSingleValued F) (hG : Set.Relation.isSingleValued G) : Set.Relation.isSingleValued (Set.Relation.comp F G)

The composition of two functions is itself a function.

theorem Set.Relation.one_to_one_comp_is_one_to_one {β : Type} {γ : Type} {α : Type} {F : Set.HRelation β γ} {G : Set.HRelation α β} (hF : Set.Relation.isOneToOne F) (hG : Set.Relation.isOneToOne G) : Set.Relation.isOneToOne (Set.Relation.comp F G)

The composition of two one-to-one Relations is one-to-one.

theorem Set.Relation.comp_inv_eq_inv_comp_inv {β : Type} {γ : Type} {α : Type} {F : Set.HRelation β γ} {G : Set.HRelation α β} : Set.Relation.inv (Set.Relation.comp F G) = Set.Relation.comp (Set.Relation.inv G) (Set.Relation.inv F)

For Relations F and G, (F ∘ G)⁻¹ = G⁻¹ ∘ F⁻¹.

Ordered Pairs

def Set.Relation.toOrderedPairs {α : Type} (R : Set.Relation α) : Set (Set (Set α))

Convert a Relation into an equivalent representation using OrderedPairs.

Equations

• Set.Relation.toOrderedPairs R = (fun (x : α × α) => match x with | (x, y) => OrderedPair x y) '' R

Equivalence Classes

def Set.Relation.isReflexive {α : Type} (R : Set.Relation α) (A : Set α) : Prop

A binary Relation R is reflexive on A iff xRx for all x ∈ A.

Equations

• Set.Relation.isReflexive R A = ∀ x ∈ A, (x, x) ∈ R

def Set.Relation.isSymmetric {α : Type} (R : Set.Relation α) : Prop

A binary Relation R is symmetric iff whenever xRy then yRx.

Equations

• Set.Relation.isSymmetric R = ∀ {x y : α}, (x, y) ∈ R → (y, x) ∈ R

def Set.Relation.isTransitive {α : Type} (R : Set.Relation α) : Prop

A binary Relation R is transitive iff whenever xRy and yRz, then xRz.

Equations

• Set.Relation.isTransitive R = ∀ {x y z : α}, (x, y) ∈ R → (y, z) ∈ R → (x, z) ∈ R

structure Set.Relation.isEquivalence {α : Type} (R : Set.Relation α) (A : Set α) : Prop

Relation R is an equivalence relation on set A iff R is a binary relation on A that is relexive on A, symmetric, and transitive.

• b_on : Set.Relation.fld R ⊆ A
• refl : Set.Relation.isReflexive R A
• symm : Set.Relation.isSymmetric R
• trans : Set.Relation.isTransitive R

def Set.Relation.neighborhood {α : Type} (R : Set.Relation α) (x : α) : Set α

A set of members related to x via Relation R.

The term "neighborhood" here was chosen to reflect this relationship between x and the members of the set. It isn't standard in anyway.

Equations

• Set.Relation.neighborhood R x = {t : α | (x, t) ∈ R}

theorem Set.Relation.neighborhood_self_mem {α : Type} {x : α} {R : Set.Relation α} {A : Set α} (hR : Set.Relation.isEquivalence R A) (hx : x ∈ A) : x ∈ Set.Relation.neighborhood R x

The neighborhood with some respect to an equivalence relation R on set A and member x contains x.

theorem Set.Relation.neighborhood_eq_iff_mem_relate {α : Type} {x : α} {y : α} {R : Set.Relation α} {A : Set α} (hR : Set.Relation.isEquivalence R A) : x ∈ A → y ∈ A → (Set.Relation.neighborhood R x = Set.Relation.neighborhood R y ↔ (x, y) ∈ R)

Assume that R is an equivalence relation on A and that x and y belong to A. Then [x]_R = [y]_R ↔ xRy.

theorem Set.Relation.neighborhood_mem_imp_relate {α : Type} {x : α} {z : α} {y : α} {R : Set.Relation α} {A : Set α} (hR : Set.Relation.isEquivalence R A) (hx : x ∈ Set.Relation.neighborhood R z) (hy : y ∈ Set.Relation.neighborhood R z) : (x, y) ∈ R

Assume that R is an equivalence relation on A. If two sets x and y belong to the same neighborhood, then xRy.

structure Set.Relation.Partition {α : Type u_1} (P : Set (Set α)) (A : Set α) : Prop

A partition Π of a set A is a set of nonempty subsets of A that is disjoint and exhaustive.

• p_subset : ∀ p ∈ P, p ⊆ A
• nonempty : ∀ p ∈ P, Set.Nonempty p
• disjoint : ∀ a ∈ P, ∀ b ∈ P, a ≠ b → a ∩ b = ∅
• exhaustive : ∀ a ∈ A, ∃ p ∈ P, a ∈ p

theorem Set.Relation.partition_mem_mem_eq {α : Type u_1} {x : α} {P : Set (Set α)} {A : Set α} (hP : Set.Relation.Partition P A) (hx : x ∈ A) : ∃! (B : Set α), B ∈ P ∧ x ∈ B

Membership of sets within P is unique.

def Set.Relation.modEquiv {α : Type} {A : Set α} {R : Set.Relation α} : Set.Relation.isEquivalence R A → Set (Set α)

The partition A / R induced by an equivalence relation R.

Equations

• Set.Relation.modEquiv x = {x : Set α | ∃ x_1 ∈ A, Set.Relation.neighborhood R x_1 = x}

theorem Set.Relation.modEquiv_partition {α : Type} {A : Set α} {R : Set.Relation α} (hR : Set.Relation.isEquivalence R A) : Set.Relation.Partition (Set.Relation.modEquiv hR) A

Show the sets formed by modEquiv do indeed form a partition.