bookshelf/Bookshelf/Enderton/Set/Relation.lean

670 lines
19 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

import Bookshelf.Enderton.Set.OrderedPair
/-! # Enderton.Set.Relation
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`.
-/
abbrev HRelation (α β : Type ) := Set (α × β)
/--
A homogeneous variant of the `HRelation` type.
-/
abbrev Relation (α : Type _) := HRelation α α
namespace Relation
/-! ## Domain and Range -/
/--
The domain of a `Relation`.
-/
def dom (R : HRelation α β) : Set α := Prod.fst '' R
/--
The first component of any pair in a `Relation` must be a member of the
`Relation`'s domain.
-/
theorem mem_pair_imp_fst_mem_dom {R : HRelation α β} (h : (x, y) ∈ R)
: 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`.
-/
theorem dom_exists {R : HRelation α β} (hx : x ∈ dom R)
: ∃ y : β, (x, y) ∈ R := by
unfold dom at hx
simp only [mem_image, Prod.exists, exists_and_right, exists_eq_right] at hx
exact hx
/--
The range of a `Relation`.
-/
def ran (R : HRelation α β) : Set β := Prod.snd '' R
theorem mem_pair_imp_snd_mem_ran {R : HRelation α β} (h : (x, y) ∈ R)
: 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`.
-/
theorem ran_exists {R : HRelation α β} (hx : x ∈ ran R)
: ∃ t : α, (t, x) ∈ R := by
unfold ran at hx
simp only [mem_image, Prod.exists, exists_eq_right] at hx
exact hx
/--
The field of a `Relation`.
-/
def fld (R : Relation α) : Set α := dom R ran R
/--
The inverse of a `Relation`.
-/
def inv (R : HRelation α β) : HRelation β α := { (p.2, p.1) | p ∈ R }
/--
`(x, y)` is a member of relation `R` **iff** `(y, x)` is a member of `R⁻¹`.
-/
@[simp]
theorem mem_self_comm_mem_inv {R : HRelation α β}
: (y, x) ∈ inv R ↔ (x, y) ∈ R := by
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]
theorem inv_inv_eq_self (R : HRelation α β)
: inv (inv R) = R := by
unfold inv
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]
theorem dom_inv_eq_ran_self {F : HRelation α β}
: dom (inv F) = ran F := by
ext x
unfold dom ran inv
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]
theorem ran_inv_eq_dom_self {F : HRelation α β}
: ran (inv F) = dom F := by
ext x
unfold dom ran inv
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 -/
/--
The restriction of a `Relation` to a `Set`.
-/
def restriction (R : HRelation α β) (A : Set α) : HRelation α β :=
{ p ∈ R | p.1 ∈ A }
/-! ## Image -/
/--
The image of a `Relation` under a `Set`.
-/
def image (R : HRelation α β) (A : Set α) : Set β :=
{ y | ∃ u ∈ A, (u, y) ∈ R }
/-! ## Single-Rooted and Single-Valued -/
/--
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`.
-/
def isSingleRooted (R : HRelation α β) : Prop :=
∀ y ∈ ran R, ∃! x, x ∈ dom R ∧ (x, y) ∈ R
/--
A single-rooted `Relation` should map the same output to the same input.
-/
theorem single_rooted_eq_unique {R : HRelation α β} {x₁ x₂ : α} {y : β}
(hR : isSingleRooted R)
: (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₂]
/--
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.
-/
def isSingleValued (R : HRelation α β) : Prop :=
∀ x ∈ dom R, ∃! y, y ∈ ran R ∧ (x, y) ∈ R
/--
A single-valued `Relation` should map the same input to the same output.
-/
theorem single_valued_eq_unique {R : HRelation α β} {x : α} {y₁ y₂ : β}
(hR : isSingleValued R)
: (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₂]
/--
For a set `F`, `F⁻¹` is a function **iff** `F` is single-rooted.
-/
theorem single_valued_inv_iff_single_rooted_self {F : HRelation α β}
: isSingleValued (inv F) ↔ isSingleRooted F := by
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
suffices ∀ x ∈ ran F, ∃! y, (y, x) ∈ F from hF
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.
-/
theorem single_valued_self_iff_single_rooted_inv {F : HRelation α β}
: isSingleValued F ↔ isSingleRooted (inv F) := by
conv => lhs; rw [← inv_inv_eq_self F]
rw [single_valued_inv_iff_single_rooted_self]
/--
The subset of a function must also be a function.
-/
theorem single_valued_subset {F G : HRelation α β}
(hG : isSingleValued G) (h : F ⊆ G)
: isSingleValued F := by
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)
/-! ## Injections -/
/--
A `Relation` `R` is one-to-one if it is a single-rooted function.
-/
def isOneToOne (R : HRelation α β) : Prop :=
isSingleValued R ∧ isSingleRooted R
/--
A `Relation` is one-to-one **iff** it's inverse is.
-/
theorem one_to_one_self_iff_one_to_one_inv {R : HRelation α β}
: isOneToOne R ↔ isOneToOne (inv R) := by
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⟩
/-! ## Surjections -/
/--
Indicates `Relation` `F` is a function from `A` to `B`.
This is usually denoted as `F : A → B`.
-/
structure mapsInto (F : HRelation α β) (A : Set α) (B : Set β) : Prop where
is_func : isSingleValued F
dom_eq : dom F = A
ran_ss : ran F ⊆ B
/--
Indicates `Relation` `F` is a function from `A` to `ran F = B`.
-/
structure mapsOnto (F : HRelation α β) (A : Set α) (B : Set β) : Prop where
is_func : isSingleValued F
dom_eq : dom F = A
ran_eq : ran F = B
/-! ## Composition -/
/--
The composition of two `Relation`s.
-/
def comp (F : HRelation β γ) (G : HRelation α β) : HRelation α γ :=
{ p | ∃ t : β, (p.1, t) ∈ G ∧ (t, p.2) ∈ F}
/--
If `x ∈ dom (F ∘ G)`, then `x ∈ dom G`.
-/
theorem dom_comp_imp_dom_self {F : HRelation β γ} {G : HRelation α β}
: x ∈ dom (comp F G) → x ∈ dom G := by
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`.
-/
theorem ran_comp_imp_ran_self {F : HRelation β γ} {G : HRelation α β}
: y ∈ ran (comp F G) → y ∈ ran F := by
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⟩
/--
Composition of functions is associative.
-/
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
_ = { 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⟩
_ = { p | ∃ a, (p.1, a) ∈ comp S T ∧ (a, p.2) ∈ R } := rfl
_ = comp R (comp S T) := rfl
/--
The composition of two functions is itself a function.
-/
theorem single_valued_comp_is_single_valued
{F : HRelation β γ} {G : HRelation α β}
(hF : isSingleValued F) (hG : isSingleValued G)
: isSingleValued (comp F G) := by
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₂]
/--
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
/--
For `Relation`s `F` and `G`, `(F ∘ G)⁻¹ = G⁻¹ ∘ F⁻¹`.
-/
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)
_ = {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⟩
_ = {p | ∃ t, (p.1, t) ∈ inv F ∧ (t, p.2) ∈ inv 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
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
/-! ## Ordered Pairs -/
/--
Convert a `Relation` into an equivalent representation using `OrderedPair`s.
-/
def toOrderedPairs (R : Relation α) : Set (Set (Set α)) :=
-- Notice here we are using `Set.image` and *not* `Set.Relation.image`.
Set.image (fun (x, y) => OrderedPair x y) R
/-! ## Equivalence Classes -/
/--
A binary `Relation` `R` is **reflexive** on `A` **iff** `xRx` for all `x ∈ A`.
-/
def isReflexive (R : Relation α) (A : Set α) := ∀ x ∈ A, (x, x) ∈ R
/--
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
relation on `A` that is relexive on `A`, symmetric, and transitive.
-/
structure isEquivalence (R : Relation α) (A : Set α) : Prop where
b_on : fld R ⊆ A
refl : isReflexive R A
symm : isSymmetric R
trans : isTransitive R
/--
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.
-/
def neighborhood (R : Relation α) (x : α) := { t | (x, t) ∈ R }
/--
The neighborhood with some respect to an equivalence relation `R` on set `A`
and member `x` contains `x`.
-/
theorem neighborhood_self_mem {R : Set.Relation α} {A : Set α}
(hR : isEquivalence R A) (hx : x ∈ A)
: x ∈ neighborhood R x := hR.refl x hx
/--
Assume that `R` is an equivalence relation on `A` and that `x` and `y` belong
to `A`. Then `[x]_R = [y]_R ↔ xRy`.
-/
theorem neighborhood_eq_iff_mem_relate {R : Set.Relation α} {A : Set α}
(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
/--
Assume that `R` is an equivalence relation on `A`. If two sets `x` and `y`
belong to the same neighborhood, then `xRy`.
-/
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
/--
A **partition** `Π` of a set `A` is a set of nonempty subsets of `A` that is
disjoint and exhaustive.
-/
structure Partition (P : Set (Set α)) (A : Set α) : Prop where
p_subset : ∀ p ∈ P, p ⊆ A
nonempty : ∀ p ∈ P, Set.Nonempty p
disjoint : ∀ a ∈ P, ∀ b, b ∈ P → a ≠ b → a ∩ b = ∅
exhaustive : ∀ a ∈ A, ∃ p, p ∈ P ∧ a ∈ p
/--
Membership of sets within `P` is unique.
-/
theorem partition_mem_mem_eq {P : Set (Set α)} {A : Set α}
(hP : Partition P A) (hx : x ∈ A)
: ∃! 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
/--
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)
: Partition (modEquiv hR) A := by
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 [
← neighborhood_eq_iff_mem_relate hR hx.left hz_mem,
← neighborhood_eq_iff_mem_relate hR hy.left hz_mem,
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⟩
end Relation
end Set