2023-06-29 21:25:59 +00:00
|
|
|
|
import Bookshelf.Enderton.Set.OrderedPair
|
2023-06-20 21:02:09 +00:00
|
|
|
|
|
2023-06-29 21:30:48 +00:00
|
|
|
|
/-! # Enderton.Set.Relation
|
2023-06-20 21:02:09 +00:00
|
|
|
|
|
|
|
|
|
A representation of a relation, i.e. a set of ordered pairs. Like `Set`, it is
|
|
|
|
|
assumed a relation is homogeneous.
|
|
|
|
|
-/
|
|
|
|
|
|
|
|
|
|
namespace Set
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
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`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
abbrev HRelation (α β : Type ) := Set (α × β)
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
A homogeneous variant of the `HRelation` type.
|
|
|
|
|
-/
|
|
|
|
|
abbrev Relation (α : Type _) := HRelation α α
|
2023-06-20 21:02:09 +00:00
|
|
|
|
|
|
|
|
|
namespace Relation
|
|
|
|
|
|
2023-06-25 13:27:35 +00:00
|
|
|
|
/-! ## Domain and Range -/
|
|
|
|
|
|
2023-06-20 21:02:09 +00:00
|
|
|
|
/--
|
|
|
|
|
The domain of a `Relation`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
def dom (R : HRelation α β) : Set α := Prod.fst '' R
|
2023-06-20 21:02:09 +00:00
|
|
|
|
|
2023-06-25 13:27:35 +00:00
|
|
|
|
/--
|
|
|
|
|
The first component of any pair in a `Relation` must be a member of the
|
|
|
|
|
`Relation`'s domain.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem mem_pair_imp_fst_mem_dom {R : HRelation α β} (h : (x, y) ∈ R)
|
2023-06-25 13:27:35 +00:00
|
|
|
|
: x ∈ dom R := by
|
|
|
|
|
unfold dom Prod.fst
|
|
|
|
|
simp only [mem_image, Prod.exists, exists_and_right, exists_eq_right]
|
|
|
|
|
exact ⟨y, h⟩
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
If `x ∈ dom R`, there exists some `y` such that `⟨x, y⟩ ∈ R`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem dom_exists {R : HRelation α β} (hx : x ∈ dom R)
|
|
|
|
|
: ∃ y : β, (x, y) ∈ R := by
|
2023-06-25 13:27:35 +00:00
|
|
|
|
unfold dom at hx
|
|
|
|
|
simp only [mem_image, Prod.exists, exists_and_right, exists_eq_right] at hx
|
|
|
|
|
exact hx
|
|
|
|
|
|
2023-06-20 21:02:09 +00:00
|
|
|
|
/--
|
|
|
|
|
The range of a `Relation`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
def ran (R : HRelation α β) : Set β := Prod.snd '' R
|
2023-06-20 21:02:09 +00:00
|
|
|
|
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem mem_pair_imp_snd_mem_ran {R : HRelation α β} (h : (x, y) ∈ R)
|
2023-06-25 13:27:35 +00:00
|
|
|
|
: y ∈ ran R := by
|
|
|
|
|
unfold ran Prod.snd
|
|
|
|
|
simp only [mem_image, Prod.exists, exists_eq_right]
|
|
|
|
|
exact ⟨x, h⟩
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
If `x ∈ ran R`, there exists some `t` such that `⟨t, x⟩ ∈ R`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem ran_exists {R : HRelation α β} (hx : x ∈ ran R)
|
2023-06-26 13:08:25 +00:00
|
|
|
|
: ∃ t : α, (t, x) ∈ R := by
|
2023-06-25 13:27:35 +00:00
|
|
|
|
unfold ran at hx
|
|
|
|
|
simp only [mem_image, Prod.exists, exists_eq_right] at hx
|
|
|
|
|
exact hx
|
|
|
|
|
|
2023-06-20 21:02:09 +00:00
|
|
|
|
/--
|
|
|
|
|
The field of a `Relation`.
|
|
|
|
|
-/
|
|
|
|
|
def fld (R : Relation α) : Set α := dom R ∪ ran R
|
|
|
|
|
|
2023-06-23 21:47:55 +00:00
|
|
|
|
/--
|
|
|
|
|
The inverse of a `Relation`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
def inv (R : HRelation α β) : HRelation β α := { (p.2, p.1) | p ∈ R }
|
2023-06-23 21:47:55 +00:00
|
|
|
|
|
2023-06-25 13:27:35 +00:00
|
|
|
|
/--
|
|
|
|
|
`(x, y)` is a member of relation `R` **iff** `(y, x)` is a member of `R⁻¹`.
|
|
|
|
|
-/
|
|
|
|
|
@[simp]
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem mem_self_comm_mem_inv {R : HRelation α β}
|
|
|
|
|
: (y, x) ∈ inv R ↔ (x, y) ∈ R := by
|
2023-06-25 13:27:35 +00:00
|
|
|
|
unfold inv
|
|
|
|
|
simp only [Prod.exists, mem_setOf_eq, Prod.mk.injEq]
|
|
|
|
|
apply Iff.intro
|
|
|
|
|
· intro ⟨x', y', hxy⟩
|
|
|
|
|
rw [← hxy.right.left, ← hxy.right.right]
|
|
|
|
|
exact hxy.left
|
|
|
|
|
· intro hxy
|
|
|
|
|
exact ⟨x, y, hxy, rfl, rfl⟩
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
The inverse of the inverse of a `Relation` is the `Relation`.
|
|
|
|
|
-/
|
|
|
|
|
@[simp]
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem inv_inv_eq_self (R : HRelation α β)
|
|
|
|
|
: inv (inv R) = R := by
|
2023-06-26 21:11:19 +00:00
|
|
|
|
unfold inv
|
2023-06-25 13:27:35 +00:00
|
|
|
|
simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq]
|
|
|
|
|
ext x
|
|
|
|
|
apply Iff.intro
|
|
|
|
|
· intro hx
|
|
|
|
|
have ⟨a₁, b₁, ⟨⟨a₂, b₂, h₁⟩, h₂⟩⟩ := hx
|
|
|
|
|
rw [← h₂, ← h₁.right.right, ← h₁.right.left]
|
|
|
|
|
exact h₁.left
|
|
|
|
|
· intro hx
|
|
|
|
|
have (p, q) := x
|
|
|
|
|
refine ⟨q, p, ⟨?_, ?_⟩⟩
|
|
|
|
|
· exact ⟨p, q, hx, rfl, rfl⟩
|
|
|
|
|
· rfl
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
For a set `F`, `dom F⁻¹ = ran F`.
|
|
|
|
|
-/
|
|
|
|
|
@[simp]
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem dom_inv_eq_ran_self {F : HRelation α β}
|
|
|
|
|
: dom (inv F) = ran F := by
|
2023-06-25 13:27:35 +00:00
|
|
|
|
ext x
|
2023-06-26 21:11:19 +00:00
|
|
|
|
unfold dom ran inv
|
2023-06-25 13:27:35 +00:00
|
|
|
|
simp only [
|
|
|
|
|
Prod.exists,
|
|
|
|
|
Set.mem_image,
|
|
|
|
|
Set.mem_setOf_eq,
|
|
|
|
|
Prod.mk.injEq,
|
|
|
|
|
exists_and_right,
|
|
|
|
|
exists_eq_right
|
|
|
|
|
]
|
|
|
|
|
apply Iff.intro
|
|
|
|
|
· intro ⟨y, a, _, h⟩
|
|
|
|
|
rw [← h.right.left]
|
|
|
|
|
exact ⟨a, h.left⟩
|
|
|
|
|
· intro ⟨y, hy⟩
|
|
|
|
|
exact ⟨y, y, x, hy, rfl, rfl⟩
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
For a set `F`, `ran F⁻¹ = dom F`.
|
|
|
|
|
-/
|
|
|
|
|
@[simp]
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem ran_inv_eq_dom_self {F : HRelation α β}
|
|
|
|
|
: ran (inv F) = dom F := by
|
2023-06-25 13:27:35 +00:00
|
|
|
|
ext x
|
2023-06-26 21:11:19 +00:00
|
|
|
|
unfold dom ran inv
|
2023-06-25 13:27:35 +00:00
|
|
|
|
simp only [
|
|
|
|
|
Prod.exists,
|
|
|
|
|
Set.mem_image,
|
|
|
|
|
Set.mem_setOf_eq,
|
|
|
|
|
Prod.mk.injEq,
|
|
|
|
|
exists_eq_right,
|
|
|
|
|
exists_and_right
|
|
|
|
|
]
|
|
|
|
|
apply Iff.intro
|
|
|
|
|
· intro ⟨a, y, b, h⟩
|
|
|
|
|
rw [← h.right.right]
|
|
|
|
|
exact ⟨b, h.left⟩
|
|
|
|
|
· intro ⟨y, hy⟩
|
|
|
|
|
exact ⟨y, x, y, hy, rfl, rfl⟩
|
|
|
|
|
|
|
|
|
|
/-! ## Restriction -/
|
|
|
|
|
|
2023-06-23 21:47:55 +00:00
|
|
|
|
/--
|
|
|
|
|
The restriction of a `Relation` to a `Set`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
def restriction (R : HRelation α β) (A : Set α) : HRelation α β :=
|
2023-11-11 22:15:03 +00:00
|
|
|
|
{ p ∈ R | p.1 ∈ A }
|
2023-06-23 21:47:55 +00:00
|
|
|
|
|
2023-06-25 13:27:35 +00:00
|
|
|
|
/-! ## Image -/
|
|
|
|
|
|
2023-06-23 21:47:55 +00:00
|
|
|
|
/--
|
|
|
|
|
The image of a `Relation` under a `Set`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
def image (R : HRelation α β) (A : Set α) : Set β :=
|
2023-06-23 21:47:55 +00:00
|
|
|
|
{ y | ∃ u ∈ A, (u, y) ∈ R }
|
|
|
|
|
|
2023-06-25 13:27:35 +00:00
|
|
|
|
/-! ## Single-Rooted and Single-Valued -/
|
|
|
|
|
|
2023-06-23 21:47:55 +00:00
|
|
|
|
/--
|
|
|
|
|
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`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
def isSingleRooted (R : HRelation α β) : Prop :=
|
2023-07-05 18:45:51 +00:00
|
|
|
|
∀ y ∈ ran R, ∃! x, x ∈ dom R ∧ (x, y) ∈ R
|
2023-06-23 21:47:55 +00:00
|
|
|
|
|
2023-06-26 13:08:25 +00:00
|
|
|
|
/--
|
|
|
|
|
A single-rooted `Relation` should map the same output to the same input.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem single_rooted_eq_unique {R : HRelation α β} {x₁ x₂ : α} {y : β}
|
|
|
|
|
(hR : isSingleRooted R)
|
2023-06-26 13:08:25 +00:00
|
|
|
|
: (x₁, y) ∈ R → (x₂, y) ∈ R → x₁ = x₂ := by
|
|
|
|
|
intro hx₁ hx₂
|
|
|
|
|
unfold isSingleRooted at hR
|
|
|
|
|
have := hR y (mem_pair_imp_snd_mem_ran hx₁)
|
|
|
|
|
have ⟨y₁, hy₁⟩ := this
|
|
|
|
|
simp only [and_imp] at hy₁
|
|
|
|
|
have h₁ := hy₁.right x₁ (mem_pair_imp_fst_mem_dom hx₁) hx₁
|
|
|
|
|
have h₂ := hy₁.right x₂ (mem_pair_imp_fst_mem_dom hx₂) hx₂
|
|
|
|
|
rw [h₁, h₂]
|
|
|
|
|
|
2023-06-23 21:47:55 +00:00
|
|
|
|
/--
|
|
|
|
|
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.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
def isSingleValued (R : HRelation α β) : Prop :=
|
2023-07-05 18:45:51 +00:00
|
|
|
|
∀ x ∈ dom R, ∃! y, y ∈ ran R ∧ (x, y) ∈ R
|
2023-06-23 21:47:55 +00:00
|
|
|
|
|
2023-06-26 13:08:25 +00:00
|
|
|
|
/--
|
|
|
|
|
A single-valued `Relation` should map the same input to the same output.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem single_valued_eq_unique {R : HRelation α β} {x : α} {y₁ y₂ : β}
|
|
|
|
|
(hR : isSingleValued R)
|
2023-06-26 13:08:25 +00:00
|
|
|
|
: (x, y₁) ∈ R → (x, y₂) ∈ R → y₁ = y₂ := by
|
|
|
|
|
intro hy₁ hy₂
|
|
|
|
|
unfold isSingleValued at hR
|
|
|
|
|
have := hR x (mem_pair_imp_fst_mem_dom hy₁)
|
|
|
|
|
have ⟨x₁, hx₁⟩ := this
|
|
|
|
|
simp only [and_imp] at hx₁
|
|
|
|
|
have h₁ := hx₁.right y₁ (mem_pair_imp_snd_mem_ran hy₁) hy₁
|
|
|
|
|
have h₂ := hx₁.right y₂ (mem_pair_imp_snd_mem_ran hy₂) hy₂
|
|
|
|
|
rw [h₁, h₂]
|
|
|
|
|
|
2023-06-25 13:27:35 +00:00
|
|
|
|
/--
|
|
|
|
|
For a set `F`, `F⁻¹` is a function **iff** `F` is single-rooted.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem single_valued_inv_iff_single_rooted_self {F : HRelation α β}
|
|
|
|
|
: isSingleValued (inv F) ↔ isSingleRooted F := by
|
2023-06-25 13:27:35 +00:00
|
|
|
|
apply Iff.intro
|
|
|
|
|
· intro hF
|
|
|
|
|
unfold isSingleValued at hF
|
|
|
|
|
simp only [
|
|
|
|
|
dom_inv_eq_ran_self,
|
|
|
|
|
ran_inv_eq_dom_self,
|
|
|
|
|
mem_self_comm_mem_inv
|
|
|
|
|
] at hF
|
2023-07-07 12:15:17 +00:00
|
|
|
|
suffices ∀ x ∈ ran F, ∃! y, (y, x) ∈ F from hF
|
2023-06-25 13:27:35 +00:00
|
|
|
|
intro x hx
|
|
|
|
|
have ⟨y, hy⟩ := hF x hx
|
|
|
|
|
simp only [
|
|
|
|
|
ran_inv_eq_dom_self,
|
|
|
|
|
mem_self_comm_mem_inv,
|
|
|
|
|
and_imp
|
|
|
|
|
] at hy
|
|
|
|
|
refine ⟨y, hy.left.right, ?_⟩
|
|
|
|
|
intro y₁ hy₁
|
|
|
|
|
exact hy.right y₁ (mem_pair_imp_fst_mem_dom hy₁) hy₁
|
|
|
|
|
· intro hF
|
|
|
|
|
unfold isSingleRooted at hF
|
|
|
|
|
unfold isSingleValued
|
|
|
|
|
simp only [
|
|
|
|
|
dom_inv_eq_ran_self,
|
|
|
|
|
ran_inv_eq_dom_self,
|
|
|
|
|
mem_self_comm_mem_inv
|
|
|
|
|
]
|
|
|
|
|
exact hF
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
For a relation `F`, `F` is a function **iff** `F⁻¹` is single-rooted.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem single_valued_self_iff_single_rooted_inv {F : HRelation α β}
|
|
|
|
|
: isSingleValued F ↔ isSingleRooted (inv F) := by
|
2023-06-25 13:27:35 +00:00
|
|
|
|
conv => lhs; rw [← inv_inv_eq_self F]
|
|
|
|
|
rw [single_valued_inv_iff_single_rooted_self]
|
|
|
|
|
|
2023-07-05 18:45:51 +00:00
|
|
|
|
/--
|
|
|
|
|
The subset of a function must also be a function.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem single_valued_subset {F G : HRelation α β}
|
|
|
|
|
(hG : isSingleValued G) (h : F ⊆ G)
|
|
|
|
|
: isSingleValued F := by
|
2023-07-05 18:45:51 +00:00
|
|
|
|
unfold isSingleValued
|
|
|
|
|
intro x hx
|
|
|
|
|
have ⟨y, hy⟩ := dom_exists hx
|
|
|
|
|
unfold ExistsUnique
|
|
|
|
|
simp only
|
|
|
|
|
refine ⟨y, ⟨mem_pair_imp_snd_mem_ran hy, hy⟩, ?_⟩
|
|
|
|
|
intro y₁ hy₁
|
|
|
|
|
exact single_valued_eq_unique hG (h hy₁.right) (h hy)
|
|
|
|
|
|
2023-07-06 21:31:09 +00:00
|
|
|
|
/-! ## Injections -/
|
|
|
|
|
|
2023-06-25 13:27:35 +00:00
|
|
|
|
/--
|
|
|
|
|
A `Relation` `R` is one-to-one if it is a single-rooted function.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
def isOneToOne (R : HRelation α β) : Prop :=
|
|
|
|
|
isSingleValued R ∧ isSingleRooted R
|
2023-06-25 13:27:35 +00:00
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
A `Relation` is one-to-one **iff** it's inverse is.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem one_to_one_self_iff_one_to_one_inv {R : HRelation α β}
|
|
|
|
|
: isOneToOne R ↔ isOneToOne (inv R) := by
|
2023-06-25 13:27:35 +00:00
|
|
|
|
unfold isOneToOne isSingleValued isSingleRooted
|
|
|
|
|
conv => rhs; simp only [
|
|
|
|
|
dom_inv_eq_ran_self,
|
|
|
|
|
ran_inv_eq_dom_self,
|
|
|
|
|
mem_self_comm_mem_inv,
|
|
|
|
|
eq_iff_iff
|
|
|
|
|
]
|
|
|
|
|
apply Iff.intro <;>
|
|
|
|
|
· intro ⟨hx, hy⟩
|
|
|
|
|
exact ⟨hy, hx⟩
|
|
|
|
|
|
2023-07-06 21:31:09 +00:00
|
|
|
|
/-! ## Surjections -/
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
Indicates `Relation` `F` is a function from `A` to `B`.
|
|
|
|
|
|
|
|
|
|
This is usually denoted as `F : A → B`.
|
|
|
|
|
-/
|
2023-07-10 22:08:48 +00:00
|
|
|
|
structure mapsInto (F : HRelation α β) (A : Set α) (B : Set β) : Prop where
|
|
|
|
|
is_func : isSingleValued F
|
|
|
|
|
dom_eq : dom F = A
|
|
|
|
|
ran_ss : ran F ⊆ B
|
2023-07-06 21:31:09 +00:00
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
Indicates `Relation` `F` is a function from `A` to `ran F = B`.
|
|
|
|
|
-/
|
2023-07-10 22:08:48 +00:00
|
|
|
|
structure mapsOnto (F : HRelation α β) (A : Set α) (B : Set β) : Prop where
|
|
|
|
|
is_func : isSingleValued F
|
|
|
|
|
dom_eq : dom F = A
|
|
|
|
|
ran_eq : ran F = B
|
2023-07-06 21:31:09 +00:00
|
|
|
|
|
2023-06-26 19:11:55 +00:00
|
|
|
|
/-! ## Composition -/
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
The composition of two `Relation`s.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
def comp (F : HRelation β γ) (G : HRelation α β) : HRelation α γ :=
|
|
|
|
|
{ p | ∃ t : β, (p.1, t) ∈ G ∧ (t, p.2) ∈ F}
|
2023-06-26 19:11:55 +00:00
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
If `x ∈ dom (F ∘ G)`, then `x ∈ dom G`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem dom_comp_imp_dom_self {F : HRelation β γ} {G : HRelation α β}
|
|
|
|
|
: x ∈ dom (comp F G) → x ∈ dom G := by
|
2023-06-26 19:11:55 +00:00
|
|
|
|
unfold dom comp
|
|
|
|
|
simp only [
|
|
|
|
|
mem_image,
|
|
|
|
|
mem_setOf_eq,
|
|
|
|
|
Prod.exists,
|
|
|
|
|
exists_and_right,
|
|
|
|
|
exists_eq_right,
|
|
|
|
|
forall_exists_index
|
|
|
|
|
]
|
|
|
|
|
intro y t ht
|
|
|
|
|
exact ⟨t, ht.left⟩
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
If `y ∈ ran (F ∘ G)`, then `y ∈ ran F`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem ran_comp_imp_ran_self {F : HRelation β γ} {G : HRelation α β}
|
|
|
|
|
: y ∈ ran (comp F G) → y ∈ ran F := by
|
2023-06-26 19:11:55 +00:00
|
|
|
|
unfold ran comp
|
|
|
|
|
simp only [
|
|
|
|
|
mem_image,
|
|
|
|
|
mem_setOf_eq,
|
|
|
|
|
Prod.exists,
|
|
|
|
|
exists_eq_right,
|
|
|
|
|
forall_exists_index
|
|
|
|
|
]
|
|
|
|
|
intro x t ht
|
|
|
|
|
exact ⟨t, ht.right⟩
|
|
|
|
|
|
2023-07-06 21:31:09 +00:00
|
|
|
|
/--
|
|
|
|
|
Composition of functions is associative.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem comp_assoc {R : HRelation γ δ} {S : HRelation β γ} {T : HRelation α β}
|
|
|
|
|
: comp (comp R S) T = comp R (comp S T) := by
|
|
|
|
|
calc comp (comp R S) T
|
|
|
|
|
_ = { p | ∃ t, (p.1, t) ∈ T ∧ (t, p.2) ∈ comp R S} := rfl
|
2023-07-06 21:31:09 +00:00
|
|
|
|
_ = { p | ∃ t, (p.1, t) ∈ T ∧ (∃ a, (t, a) ∈ S ∧ (a, p.2) ∈ R) } := rfl
|
|
|
|
|
_ = { p | ∃ t, ∃ a, ((p.1, t) ∈ T ∧ (t, a) ∈ S) ∧ (a, p.2) ∈ R } := by
|
|
|
|
|
ext p
|
|
|
|
|
simp only [mem_setOf_eq]
|
|
|
|
|
apply Iff.intro
|
|
|
|
|
· intro ⟨t, ht, a, ha⟩
|
|
|
|
|
exact ⟨t, a, ⟨ht, ha.left⟩, ha.right⟩
|
|
|
|
|
· intro ⟨t, a, h₁, h₂⟩
|
|
|
|
|
exact ⟨t, h₁.left, a, h₁.right, h₂⟩
|
|
|
|
|
_ = { p | ∃ a, ∃ t, ((p.1, t) ∈ T ∧ (t, a) ∈ S) ∧ (a, p.2) ∈ R } := by
|
|
|
|
|
ext p
|
|
|
|
|
simp only [mem_setOf_eq]
|
|
|
|
|
apply Iff.intro
|
|
|
|
|
· intro ⟨t, a, h⟩
|
|
|
|
|
exact ⟨a, t, h⟩
|
|
|
|
|
· intro ⟨a, t, h⟩
|
|
|
|
|
exact ⟨t, a, h⟩
|
|
|
|
|
_ = { p | ∃ a, (∃ t, (p.1, t) ∈ T ∧ (t, a) ∈ S) ∧ (a, p.2) ∈ R } := by
|
|
|
|
|
ext p
|
|
|
|
|
simp only [mem_setOf_eq]
|
|
|
|
|
apply Iff.intro
|
|
|
|
|
· intro ⟨a, t, h⟩
|
|
|
|
|
exact ⟨a, ⟨t, h.left⟩, h.right⟩
|
|
|
|
|
· intro ⟨a, ⟨t, ht⟩, ha⟩
|
|
|
|
|
exact ⟨a, t, ht, ha⟩
|
2023-07-07 12:15:17 +00:00
|
|
|
|
_ = { p | ∃ a, (p.1, a) ∈ comp S T ∧ (a, p.2) ∈ R } := rfl
|
|
|
|
|
_ = comp R (comp S T) := rfl
|
2023-07-06 21:31:09 +00:00
|
|
|
|
|
2023-06-26 19:11:55 +00:00
|
|
|
|
/--
|
|
|
|
|
The composition of two functions is itself a function.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem single_valued_comp_is_single_valued
|
|
|
|
|
{F : HRelation β γ} {G : HRelation α β}
|
|
|
|
|
(hF : isSingleValued F) (hG : isSingleValued G)
|
|
|
|
|
: isSingleValued (comp F G) := by
|
2023-06-26 19:11:55 +00:00
|
|
|
|
unfold isSingleValued
|
|
|
|
|
intro x hx
|
|
|
|
|
have ⟨y, hxy⟩ := dom_exists hx
|
|
|
|
|
have hy := mem_pair_imp_snd_mem_ran hxy
|
|
|
|
|
refine ⟨y, ⟨hy, hxy⟩, ?_⟩
|
|
|
|
|
simp only [and_imp]
|
|
|
|
|
|
|
|
|
|
intro y₁ _ hxy₁
|
|
|
|
|
unfold comp at hxy hxy₁
|
|
|
|
|
simp only [mem_setOf_eq] at hxy hxy₁
|
|
|
|
|
have ⟨t₁, ht₁⟩ := hxy
|
|
|
|
|
have ⟨t₂, ht₂⟩ := hxy₁
|
|
|
|
|
|
|
|
|
|
-- First show `t₁ = t₂` and then show `y = y₁`.
|
|
|
|
|
have t_eq : t₁ = t₂ := by
|
|
|
|
|
unfold isSingleValued at hG
|
|
|
|
|
have ⟨t', ht'⟩ := hG x (mem_pair_imp_fst_mem_dom ht₁.left)
|
|
|
|
|
simp only [and_imp] at ht'
|
|
|
|
|
have ht₁' := ht'.right t₁ (mem_pair_imp_snd_mem_ran ht₁.left) ht₁.left
|
|
|
|
|
have ht₂' := ht'.right t₂ (mem_pair_imp_snd_mem_ran ht₂.left) ht₂.left
|
|
|
|
|
rw [ht₁', ht₂']
|
|
|
|
|
|
|
|
|
|
unfold isSingleValued at hF
|
|
|
|
|
rw [t_eq] at ht₁
|
|
|
|
|
have ⟨y', hy'⟩ := hF t₂ (mem_pair_imp_fst_mem_dom ht₁.right)
|
|
|
|
|
simp only [and_imp] at hy'
|
|
|
|
|
have hk₁ := hy'.right y (mem_pair_imp_snd_mem_ran ht₁.right) ht₁.right
|
|
|
|
|
have hk₂ := hy'.right y₁ (mem_pair_imp_snd_mem_ran ht₂.right) ht₂.right
|
|
|
|
|
rw [hk₁, hk₂]
|
|
|
|
|
|
2023-08-16 18:46:16 +00:00
|
|
|
|
/--
|
|
|
|
|
The composition of two one-to-one `Relation`s is one-to-one.
|
|
|
|
|
-/
|
|
|
|
|
theorem one_to_one_comp_is_one_to_one
|
|
|
|
|
{F : HRelation β γ} {G : HRelation α β}
|
|
|
|
|
(hF : isOneToOne F) (hG : isOneToOne G)
|
|
|
|
|
: isOneToOne (comp F G) := by
|
|
|
|
|
refine ⟨single_valued_comp_is_single_valued hF.left hG.left, ?_⟩
|
|
|
|
|
intro y hy
|
|
|
|
|
unfold ExistsUnique
|
|
|
|
|
have ⟨x₁, hx₁⟩ := ran_exists hy
|
|
|
|
|
refine ⟨x₁, ⟨mem_pair_imp_fst_mem_dom hx₁, hx₁⟩, ?_⟩
|
|
|
|
|
intro x₂ ⟨_, hx₂⟩
|
|
|
|
|
have ⟨t₁, ht₁⟩ := hx₁
|
|
|
|
|
have ⟨t₂, ht₂⟩ := hx₂
|
|
|
|
|
simp only at ht₁ ht₂
|
|
|
|
|
have ht : t₁ = t₂ := single_rooted_eq_unique hF.right ht₁.right ht₂.right
|
|
|
|
|
rw [ht] at ht₁
|
|
|
|
|
exact single_rooted_eq_unique hG.right ht₂.left ht₁.left
|
|
|
|
|
|
2023-06-26 21:11:19 +00:00
|
|
|
|
/--
|
|
|
|
|
For `Relation`s `F` and `G`, `(F ∘ G)⁻¹ = G⁻¹ ∘ F⁻¹`.
|
|
|
|
|
-/
|
2023-07-07 12:15:17 +00:00
|
|
|
|
theorem comp_inv_eq_inv_comp_inv {F : HRelation β γ} {G : HRelation α β}
|
|
|
|
|
: inv (comp F G) = comp (inv G) (inv F) := by
|
|
|
|
|
calc inv (comp F G)
|
2023-06-26 21:11:19 +00:00
|
|
|
|
_ = {p | ∃ t, (p.2, t) ∈ G ∧ (t, p.1) ∈ F} := by
|
|
|
|
|
rw [Set.Subset.antisymm_iff]
|
|
|
|
|
apply And.intro
|
|
|
|
|
· unfold inv comp
|
|
|
|
|
intro t ht
|
|
|
|
|
simp only [mem_setOf_eq, Prod.exists] at ht
|
|
|
|
|
have ⟨a, b, ⟨⟨p, hp⟩, hab⟩⟩ := ht
|
|
|
|
|
rw [← hab]
|
|
|
|
|
exact ⟨p, hp⟩
|
|
|
|
|
· unfold inv comp
|
|
|
|
|
intro (a, b) ⟨p, hp⟩
|
|
|
|
|
simp only [mem_setOf_eq, Prod.exists, Prod.mk.injEq]
|
|
|
|
|
exact ⟨b, a, ⟨p, hp⟩, rfl, rfl⟩
|
|
|
|
|
_ = {p | ∃ t, (t, p.1) ∈ F ∧ (p.2, t) ∈ G} := by
|
|
|
|
|
rw [Set.Subset.antisymm_iff]
|
|
|
|
|
apply And.intro
|
|
|
|
|
· intro (a, b) ht
|
|
|
|
|
simp only [mem_setOf_eq] at *
|
|
|
|
|
have ⟨t, p, q⟩ := ht
|
|
|
|
|
exact ⟨t, q, p⟩
|
|
|
|
|
· intro (a, b) ht
|
|
|
|
|
simp only [mem_setOf_eq] at *
|
|
|
|
|
have ⟨t, p, q⟩ := ht
|
|
|
|
|
exact ⟨t, q, p⟩
|
2023-07-07 12:15:17 +00:00
|
|
|
|
_ = {p | ∃ t, (p.1, t) ∈ inv F ∧ (t, p.2) ∈ inv G } := by
|
2023-06-26 21:11:19 +00:00
|
|
|
|
rw [Set.Subset.antisymm_iff]
|
|
|
|
|
apply And.intro
|
|
|
|
|
· intro (a, b) ht
|
|
|
|
|
simp only [mem_setOf_eq] at *
|
|
|
|
|
have ⟨t, p, q⟩ := ht
|
|
|
|
|
refine ⟨t, ?_, ?_⟩ <;> rwa [mem_self_comm_mem_inv]
|
|
|
|
|
· intro (a, b) ht
|
|
|
|
|
simp only [mem_setOf_eq] at *
|
|
|
|
|
have ⟨t, p, q⟩ := ht
|
|
|
|
|
refine ⟨t, ?_, ?_⟩ <;> rwa [← mem_self_comm_mem_inv]
|
|
|
|
|
_ = comp (inv G) (inv F) := rfl
|
|
|
|
|
|
2023-06-25 13:27:35 +00:00
|
|
|
|
/-! ## Ordered Pairs -/
|
|
|
|
|
|
2023-06-20 21:02:09 +00:00
|
|
|
|
/--
|
|
|
|
|
Convert a `Relation` into an equivalent representation using `OrderedPair`s.
|
|
|
|
|
-/
|
|
|
|
|
def toOrderedPairs (R : Relation α) : Set (Set (Set α)) :=
|
2023-06-23 21:47:55 +00:00
|
|
|
|
-- Notice here we are using `Set.image` and *not* `Set.Relation.image`.
|
|
|
|
|
Set.image (fun (x, y) => OrderedPair x y) R
|
2023-06-20 21:02:09 +00:00
|
|
|
|
|
2023-07-08 16:01:43 +00:00
|
|
|
|
/-! ## Equivalence Classes -/
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
A binary `Relation` `R` is **reflexive** on `A` **iff** `xRx` for all `x ∈ A`.
|
|
|
|
|
-/
|
2023-07-10 22:08:48 +00:00
|
|
|
|
def isReflexive (R : Relation α) (A : Set α) := ∀ x ∈ A, (x, x) ∈ R
|
2023-07-08 16:01:43 +00:00
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
A binary `Relation` `R` is **symmetric** **iff** whenever `xRy` then `yRx`.
|
|
|
|
|
-/
|
|
|
|
|
def isSymmetric (R : Relation α) := ∀ {x y : α}, (x, y) ∈ R → (y, x) ∈ R
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
A binary `Relation` `R` is **transitive** **iff** whenever `xRy` and `yRz`, then
|
|
|
|
|
`xRz`.
|
|
|
|
|
-/
|
|
|
|
|
def isTransitive (R : Relation α) :=
|
|
|
|
|
∀ {x y z : α}, (x, y) ∈ R → (y, z) ∈ R → (x, z) ∈ R
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
`Relation` `R` is an **equivalence relation** on set `A` **iff** `R` is a binary
|
2023-07-10 22:08:48 +00:00
|
|
|
|
relation on `A` that is relexive on `A`, symmetric, and transitive.
|
2023-07-08 16:01:43 +00:00
|
|
|
|
-/
|
2023-07-10 22:08:48 +00:00
|
|
|
|
structure isEquivalence (R : Relation α) (A : Set α) : Prop where
|
|
|
|
|
b_on : fld R ⊆ A
|
|
|
|
|
refl : isReflexive R A
|
|
|
|
|
symm : isSymmetric R
|
|
|
|
|
trans : isTransitive R
|
2023-07-08 16:01:43 +00:00
|
|
|
|
|
|
|
|
|
/--
|
2023-07-10 22:08:48 +00:00
|
|
|
|
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.
|
2023-07-08 16:01:43 +00:00
|
|
|
|
-/
|
2023-07-10 22:08:48 +00:00
|
|
|
|
def neighborhood (R : Relation α) (x : α) := { t | (x, t) ∈ R }
|
2023-07-08 16:01:43 +00:00
|
|
|
|
|
2023-07-11 22:48:46 +00:00
|
|
|
|
/--
|
|
|
|
|
The neighborhood with some respect to an equivalence relation `R` on set `A`
|
|
|
|
|
and member `x` contains `x`.
|
|
|
|
|
-/
|
2023-07-13 12:40:40 +00:00
|
|
|
|
theorem neighborhood_self_mem {R : Set.Relation α} {A : Set α}
|
2023-07-11 22:48:46 +00:00
|
|
|
|
(hR : isEquivalence R A) (hx : x ∈ A)
|
|
|
|
|
: x ∈ neighborhood R x := hR.refl x hx
|
|
|
|
|
|
2023-07-08 16:01:43 +00:00
|
|
|
|
/--
|
2023-07-10 22:08:48 +00:00
|
|
|
|
Assume that `R` is an equivalence relation on `A` and that `x` and `y` belong
|
|
|
|
|
to `A`. Then `[x]_R = [y]_R ↔ xRy`.
|
2023-07-08 16:01:43 +00:00
|
|
|
|
-/
|
2023-07-13 12:40:40 +00:00
|
|
|
|
theorem neighborhood_eq_iff_mem_relate {R : Set.Relation α} {A : Set α}
|
2023-07-10 22:08:48 +00:00
|
|
|
|
(hR : isEquivalence R A) (_ : x ∈ A) (hy : y ∈ A)
|
|
|
|
|
: neighborhood R x = neighborhood R y ↔ (x, y) ∈ R := by
|
|
|
|
|
apply Iff.intro
|
|
|
|
|
· intro h
|
|
|
|
|
have : y ∈ neighborhood R y := hR.refl y hy
|
|
|
|
|
rwa [← h] at this
|
|
|
|
|
· intro h
|
|
|
|
|
rw [Set.ext_iff]
|
|
|
|
|
intro t
|
|
|
|
|
apply Iff.intro
|
|
|
|
|
· intro ht
|
|
|
|
|
have := hR.symm h
|
|
|
|
|
exact hR.trans this ht
|
|
|
|
|
· intro ht
|
|
|
|
|
exact hR.trans h ht
|
2023-07-08 16:01:43 +00:00
|
|
|
|
|
2023-07-13 12:40:40 +00:00
|
|
|
|
/--
|
|
|
|
|
Assume that `R` is an equivalence relation on `A`. If two sets `x` and `y`
|
2023-11-11 22:15:03 +00:00
|
|
|
|
belong to the same neighborhood, then `xRy`.
|
2023-07-13 12:40:40 +00:00
|
|
|
|
-/
|
|
|
|
|
theorem neighborhood_mem_imp_relate {R : Set.Relation α} {A : Set α}
|
|
|
|
|
(hR : isEquivalence R A)
|
|
|
|
|
(hx : x ∈ neighborhood R z) (hy : y ∈ neighborhood R z)
|
|
|
|
|
: (x, y) ∈ R := by
|
|
|
|
|
unfold neighborhood at hx hy
|
|
|
|
|
simp only [mem_setOf_eq] at hx hy
|
|
|
|
|
have := hR.symm hx
|
|
|
|
|
exact hR.trans this hy
|
|
|
|
|
|
2023-07-08 16:01:43 +00:00
|
|
|
|
/--
|
2023-07-10 22:08:48 +00:00
|
|
|
|
A **partition** `Π` of a set `A` is a set of nonempty subsets of `A` that is
|
|
|
|
|
disjoint and exhaustive.
|
2023-07-08 16:01:43 +00:00
|
|
|
|
-/
|
2023-08-15 02:37:09 +00:00
|
|
|
|
structure Partition (P : Set (Set α)) (A : Set α) : Prop where
|
2023-11-11 22:15:03 +00:00
|
|
|
|
p_subset : ∀ p ∈ P, p ⊆ A
|
2023-07-10 22:08:48 +00:00
|
|
|
|
nonempty : ∀ p ∈ P, Set.Nonempty p
|
|
|
|
|
disjoint : ∀ a ∈ P, ∀ b, b ∈ P → a ≠ b → a ∩ b = ∅
|
|
|
|
|
exhaustive : ∀ a ∈ A, ∃ p, p ∈ P ∧ a ∈ p
|
|
|
|
|
|
2023-07-11 22:48:46 +00:00
|
|
|
|
/--
|
|
|
|
|
Membership of sets within `P` is unique.
|
|
|
|
|
-/
|
|
|
|
|
theorem partition_mem_mem_eq {P : Set (Set α)} {A : Set α}
|
2023-08-15 02:37:09 +00:00
|
|
|
|
(hP : Partition P A) (hx : x ∈ A)
|
2023-07-11 22:48:46 +00:00
|
|
|
|
: ∃! B, B ∈ P ∧ x ∈ B := by
|
|
|
|
|
have ⟨B, hB⟩ := hP.exhaustive x hx
|
|
|
|
|
refine ⟨B, hB, ?_⟩
|
|
|
|
|
intro B₁ hB₁
|
|
|
|
|
by_contra nB
|
|
|
|
|
have hB_disj := hP.disjoint B hB.left B₁ hB₁.left (Ne.symm nB)
|
|
|
|
|
rw [Set.ext_iff] at hB_disj
|
|
|
|
|
have := (hB_disj x).mp ⟨hB.right, hB₁.right⟩
|
|
|
|
|
simp at this
|
|
|
|
|
|
2023-07-10 22:08:48 +00:00
|
|
|
|
/--
|
|
|
|
|
The partition `A / R` induced by an equivalence relation `R`.
|
|
|
|
|
-/
|
|
|
|
|
def modEquiv {A : Set α} {R : Relation α} (_ : isEquivalence R A) :=
|
|
|
|
|
{neighborhood R x | x ∈ A}
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
Show the sets formed by `modEquiv` do indeed form a `partition`.
|
|
|
|
|
-/
|
|
|
|
|
theorem modEquiv_partition {A : Set α} {R : Relation α} (hR : isEquivalence R A)
|
2023-08-15 02:37:09 +00:00
|
|
|
|
: Partition (modEquiv hR) A := by
|
2023-07-10 22:08:48 +00:00
|
|
|
|
refine ⟨?_, ?_, ?_, ?_⟩
|
|
|
|
|
· intro p hp
|
|
|
|
|
have ⟨x, hx⟩ := hp
|
|
|
|
|
rw [← hx.right]
|
|
|
|
|
show ∀ t, t ∈ neighborhood R x → t ∈ A
|
|
|
|
|
intro t ht
|
|
|
|
|
have : t ∈ fld R := Or.inr (mem_pair_imp_snd_mem_ran ht)
|
|
|
|
|
exact hR.b_on this
|
|
|
|
|
· intro p hp
|
|
|
|
|
have ⟨x, hx⟩ := hp
|
|
|
|
|
refine ⟨x, ?_⟩
|
|
|
|
|
rw [← hx.right]
|
|
|
|
|
exact hR.refl x hx.left
|
|
|
|
|
· intro X hX Y hY nXY
|
|
|
|
|
by_contra nh
|
|
|
|
|
have nh' : Set.Nonempty (X ∩ Y) := by
|
|
|
|
|
rw [← Set.nmem_singleton_empty]
|
|
|
|
|
exact nh
|
|
|
|
|
have ⟨x, hx⟩ := hX
|
|
|
|
|
have ⟨y, hy⟩ := hY
|
|
|
|
|
have ⟨z, hz⟩ := nh'
|
|
|
|
|
rw [← hx.right, ← hy.right] at hz
|
|
|
|
|
unfold neighborhood at hz
|
|
|
|
|
simp only [mem_inter_iff, mem_setOf_eq] at hz
|
|
|
|
|
have hz_mem : z ∈ A := by
|
|
|
|
|
have : z ∈ fld R := Or.inr (mem_pair_imp_snd_mem_ran hz.left)
|
|
|
|
|
exact hR.b_on this
|
|
|
|
|
rw [
|
2023-07-13 12:40:40 +00:00
|
|
|
|
← neighborhood_eq_iff_mem_relate hR hx.left hz_mem,
|
|
|
|
|
← neighborhood_eq_iff_mem_relate hR hy.left hz_mem,
|
2023-07-10 22:08:48 +00:00
|
|
|
|
hx.right, hy.right
|
|
|
|
|
] at hz
|
|
|
|
|
rw [hz.left, hz.right] at nXY
|
|
|
|
|
simp only [ne_eq, not_true] at nXY
|
|
|
|
|
· intro x hx
|
|
|
|
|
exact ⟨neighborhood R x, ⟨x, hx, rfl⟩, hR.refl x hx⟩
|
2023-07-08 16:01:43 +00:00
|
|
|
|
|
2023-06-20 21:02:09 +00:00
|
|
|
|
end Relation
|
|
|
|
|
|
2023-11-11 22:15:03 +00:00
|
|
|
|
end Set
|