Enderton. Continue through theorem 3 set.
parent
d215265a91
commit
a6e6251627
|
|
@ -3037,14 +3037,14 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive
|
|||
|
||||
\statementpadding
|
||||
|
||||
\lean*{Bookshelf/Enderton/Set/Chapter\_3}
|
||||
{Enderton.Set.Chapter\_3.theorem\_3e\_i}
|
||||
\lean*{Common/Set/Relation}
|
||||
{Set.Relation.dom\_inv\_eq\_ran\_self}
|
||||
|
||||
\lean*{Bookshelf/Enderton/Set/Chapter\_3}
|
||||
{Enderton.Set.Chapter\_3.theorem\_3e\_ii}
|
||||
\lean*{Common/Set/Relation}
|
||||
{Set.Relation.ran\_inv\_eq\_dom\_self}
|
||||
|
||||
\lean{Bookshelf/Enderton/Set/Chapter\_3}
|
||||
{Enderton.Set.Chapter\_3.theorem\_3e\_iii}
|
||||
\lean{Common/Set/Relation}
|
||||
{Set.Relation.inv\_inv\_eq\_self}
|
||||
|
||||
We prove that (i) $\dom{(F^{-1})} = \ran{F}$, (ii) $\ran{(F^{-1})} = \dom{F}$,
|
||||
and (iii) $(F^{-1})^{-1} = F$.
|
||||
|
|
@ -3081,7 +3081,7 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive
|
|||
|
||||
\end{proof}
|
||||
|
||||
\subsection{\partial{Theorem 3F}}%
|
||||
\subsection{\verified{Theorem 3F}}%
|
||||
\label{sub:theorem-3f}
|
||||
|
||||
\begin{theorem}[3F]
|
||||
|
|
@ -3095,11 +3095,11 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive
|
|||
|
||||
\statementpadding
|
||||
|
||||
\lean*{Bookshelf/Enderton/Set/Chapter\_3}
|
||||
{Enderton.Set.Chapter\_3.theorem\_3f\_i}
|
||||
\lean*{Common/Set/Relation}
|
||||
{Set.Relation.single\_valued\_inv\_iff\_single\_rooted\_self}
|
||||
|
||||
\lean{Bookshelf/Enderton/Set/Chapter\_3}
|
||||
{Enderton.Set.Chapter\_3.theorem\_3f\_ii}
|
||||
\lean{Common/Set/Relation}
|
||||
{Set.Relation.single\_valued\_self\_iff\_single\_rooted\_inv}
|
||||
|
||||
We prove that (i) any set $F$, $F^{-1}$ is a function iff $F$ is
|
||||
single-rooted and (ii) any relation $F$ is a function iff $F^{-1}$ is
|
||||
|
|
@ -3151,14 +3151,16 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive
|
|||
|
||||
\end{proof}
|
||||
|
||||
\subsection{\partial{Lemma 1}}%
|
||||
\subsection{\verified{Lemma 1}}%
|
||||
\label{sub:lemma-1}
|
||||
|
||||
Assume that $F$ is a one-to-one function.
|
||||
Then $F^{-1}$ is a one-to-one function.
|
||||
For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
|
||||
|
||||
\begin{proof}
|
||||
|
||||
\lean{Common/Set/Relation}
|
||||
{Set.Relation.one\_to\_one\_self\_iff\_one\_to\_one\_inv}
|
||||
|
||||
We prove that (i) $F^{-1}$ is a function and (ii) $F^{-1}$ is single-rooted.
|
||||
|
||||
\paragraph{(i)}%
|
||||
|
|
@ -3211,11 +3213,11 @@ Then $F^{-1}$ is a one-to-one function.
|
|||
|
||||
For all $x \in \dom{F}$, $\left< x, F(x) \right> \in F$.
|
||||
Then $\left< F(x), x \right> \in F^{-1}$.
|
||||
Since $F^{-1}$ is single-valued, $F^{-1}(F(x)) = x$ is well-defined.
|
||||
Since $F^{-1}$ is single-valued, $F^{-1}(F(x)) = x$.
|
||||
|
||||
For all $y \in \ran{F}$, $\left< y, F^{-1}(y) \right> \in F^{-1}$.
|
||||
Then $\left< F^{-1}(y), y \right> \in F$.
|
||||
Since $F$ is single-valued, $F(F^{-1}(y)) = y$ is also well-defined.
|
||||
Since $F$ is single-valued, $F(F^{-1}(y)) = y$.
|
||||
|
||||
\end{proof}
|
||||
|
||||
|
|
|
|||
|
|
@ -432,86 +432,22 @@ theorem exercise_6_9_ii {A : Set (Set.Relation α)}
|
|||
intro _ y hy R hR
|
||||
exact ⟨y, hy R hR⟩
|
||||
|
||||
/-- ### Theorem 3E (i)
|
||||
/-- ### Theorem 3G (i)
|
||||
|
||||
For a set `F`, `dom F⁻¹ = ran F`.
|
||||
Assume that `F` is a one-to-one function. If `x ∈ dom F`, then `F⁻¹(F(x)) = x`.
|
||||
-/
|
||||
theorem theorem_3e_i {F : Set.Relation α}
|
||||
: Set.Relation.dom (F.inv) = Set.Relation.ran F := by
|
||||
ext x
|
||||
unfold Set.Relation.dom Set.Relation.ran Set.Relation.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⟩
|
||||
|
||||
/-- ### Theorem 3E (ii)
|
||||
|
||||
For a set `F`, `ran F⁻¹ = dom F`.
|
||||
-/
|
||||
theorem theorem_3e_ii {F : Set.Relation α}
|
||||
: Set.Relation.ran (F.inv) = Set.Relation.dom F := by
|
||||
ext x
|
||||
unfold Set.Relation.dom Set.Relation.ran Set.Relation.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⟩
|
||||
|
||||
/-- ### Theorem 3E (iii)
|
||||
|
||||
For a set `F`, `(F⁻¹)⁻¹ = F`.
|
||||
-/
|
||||
theorem theorem_3e_iii {F : Set.Relation α}
|
||||
: F.inv.inv = F := by
|
||||
unfold Set.Relation.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
|
||||
|
||||
/-- ### Theorem 3F (i)
|
||||
|
||||
For a set `F`, `F⁻¹` is a function **iff** `F` is single-rooted.
|
||||
-/
|
||||
theorem theorem_3f_i {F : Set.Relation α}
|
||||
: Set.Relation.isSingleValued F.inv ↔ Set.Relation.isSingleRooted F := by
|
||||
theorem theorem_3g_i {F : Set.Relation α}
|
||||
(hF : Set.Relation.isOneToOne F) (hx : x ∈ F.dom)
|
||||
: ∃! y, (x, y) ∈ F ∧ (y, x) ∈ F.inv := by
|
||||
sorry
|
||||
|
||||
/-- ### Theorem 3F (ii)
|
||||
/-- ### Theorem 3G (ii)
|
||||
|
||||
For a relation `F`, `F` is a function **iff** `F⁻¹` is single-rooted.
|
||||
Assume that `F` is a one-to-one function. If `y ∈ ran F`, then `F(F⁻¹(y)) = y`.
|
||||
-/
|
||||
theorem theorem_3f_ii {F : Set.Relation α}
|
||||
: Set.Relation.isSingleValued F ↔ Set.Relation.isSingleRooted F.inv := by
|
||||
theorem theorem_3g_ii {F : Set.Relation α}
|
||||
(hF : Set.Relation.isOneToOne F) (hy : x ∈ F.ran)
|
||||
: ∃! x, (x, y) ∈ F ∧ (y, x) ∈ F.inv := by
|
||||
sorry
|
||||
|
||||
end Enderton.Set.Chapter_3
|
||||
|
|
@ -22,16 +22,52 @@ abbrev Relation (α : Type _) := Set (α × α)
|
|||
|
||||
namespace Relation
|
||||
|
||||
/-! ## Domain and Range -/
|
||||
|
||||
/--
|
||||
The domain of a `Relation`.
|
||||
-/
|
||||
def dom (R : Relation α) : 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 : Relation α} (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 : Relation α} (hx : x ∈ R.dom)
|
||||
: ∃ 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 : Relation α) : Set α := Prod.snd '' R
|
||||
|
||||
theorem mem_pair_imp_snd_mem_ran {R : Relation α} (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 : Relation α} (hx : x ∈ R.ran)
|
||||
: ∃ 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`.
|
||||
-/
|
||||
|
|
@ -42,24 +78,113 @@ The inverse of a `Relation`.
|
|||
-/
|
||||
def inv (R : Relation α) : Relation α := { (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 : Relation α}
|
||||
: (y, x) ∈ R.inv ↔ (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 : Relation α)
|
||||
: R.inv.inv = R := by
|
||||
unfold Set.Relation.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 : Set.Relation α}
|
||||
: Set.Relation.dom (F.inv) = Set.Relation.ran F := by
|
||||
ext x
|
||||
unfold Set.Relation.dom Set.Relation.ran Set.Relation.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 : Set.Relation α}
|
||||
: Set.Relation.ran (F.inv) = Set.Relation.dom F := by
|
||||
ext x
|
||||
unfold Set.Relation.dom Set.Relation.ran Set.Relation.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⟩
|
||||
|
||||
/-! ## Composition -/
|
||||
|
||||
/--
|
||||
The composition of two `Relation`s.
|
||||
-/
|
||||
def comp (F G : Relation α) : Relation α :=
|
||||
{ p | ∃ t, (p.1, t) ∈ G ∧ (t, p.2) ∈ F}
|
||||
|
||||
/-! ## Restriction -/
|
||||
|
||||
/--
|
||||
The restriction of a `Relation` to a `Set`.
|
||||
-/
|
||||
def restriction (R : Relation α) (A : Set α) : Relation α :=
|
||||
{ p ∈ R | p.1 ∈ A }
|
||||
|
||||
/-! ## Image -/
|
||||
|
||||
/--
|
||||
The image of a `Relation` under a `Set`.
|
||||
-/
|
||||
def image (R : Relation α) (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`.
|
||||
|
|
@ -76,6 +201,72 @@ Notice, a `Relation` that is single-valued is a function.
|
|||
def isSingleValued (R : Relation α) : Prop :=
|
||||
∀ x ∈ R.dom, ∃! y, y ∈ R.ran ∧ (x, y) ∈ R
|
||||
|
||||
/--
|
||||
For a set `F`, `F⁻¹` is a function **iff** `F` is single-rooted.
|
||||
-/
|
||||
theorem single_valued_inv_iff_single_rooted_self {F : Set.Relation α}
|
||||
: isSingleValued F.inv ↔ 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 ∈ F.ran, ∃! 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 : Set.Relation α}
|
||||
: Set.Relation.isSingleValued F ↔ Set.Relation.isSingleRooted F.inv := by
|
||||
conv => lhs; rw [← inv_inv_eq_self F]
|
||||
rw [single_valued_inv_iff_single_rooted_self]
|
||||
|
||||
/--
|
||||
A `Relation` `R` is one-to-one if it is a single-rooted function.
|
||||
-/
|
||||
def isOneToOne (R : Relation α) : 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 : Relation α}
|
||||
: isOneToOne R ↔ isOneToOne R.inv := 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⟩
|
||||
|
||||
/-! ## Ordered Pairs -/
|
||||
|
||||
/--
|
||||
Convert a `Relation` into an equivalent representation using `OrderedPair`s.
|
||||
-/
|
||||
|
|
|
|||
Loading…
Reference in New Issue