Mathlib.Data.Rel

Rel definition

(α β : Type*)

Full source

/-- A relation on `α` and `β`, aka a set-valued function, aka a partial multifunction -/
def Rel (α β : Type*) :=
  α → β → Prop

Relation between types $\alpha$ and $\beta$

Informal description

A relation between types $\alpha$ and $\beta$ is a function that takes an element of $\alpha$ and an element of $\beta$ and returns a proposition, representing whether the two elements are related. This can also be viewed as a set-valued function or a partial multifunction.

instCompleteLatticeRel instance

: CompleteLattice (Rel α β)

Full source

instance : CompleteLattice (Rel α β) := show CompleteLattice (α → β → Prop) from inferInstance

Complete Lattice Structure on Relations

Informal description

For any types $\alpha$ and $\beta$, the set of relations between $\alpha$ and $\beta$ forms a complete lattice. Here, a relation is a function $\alpha \to \beta \to \text{Prop}$, and the lattice operations (meet, join, top, bottom) are defined pointwise.

instInhabitedRel instance

: Inhabited (Rel α β)

Full source

instance : Inhabited (Rel α β) := show Inhabited (α → β → Prop) from inferInstance

Inhabited Type of Relations

Informal description

For any types $\alpha$ and $\beta$, the type of relations $\text{Rel}(\alpha, \beta)$ is inhabited.

Rel.ext theorem

{r s : Rel α β} : (∀ a, r a = s a) → r = s

Full source

@[ext] theorem ext {r s : Rel α β} : (∀ a, r a = s a) → r = s := funext

Extensionality of Relations

Informal description

For any two relations $r, s$ between types $\alpha$ and $\beta$, if for every element $a \in \alpha$ the relations $r(a)$ and $s(a)$ are equal (as functions $\beta \to \text{Prop}$), then $r = s$.

Rel.inv definition

: Rel β α

Full source

/-- The inverse relation : `r.inv x y ↔ r y x`. Note that this is *not* a groupoid inverse. -/
def inv : Rel β α :=
  flip r

Inverse relation

Informal description

The inverse relation of a relation $r$ between types $\alpha$ and $\beta$ is the relation $r^{-1}$ between $\beta$ and $\alpha$ defined by $r^{-1}(y, x) \leftrightarrow r(x, y)$ for all $x \in \alpha$ and $y \in \beta$. Note that this is not a groupoid inverse, but simply swaps the arguments of the original relation.

Rel.inv_def theorem

(x : α) (y : β) : r.inv y x ↔ r x y

Full source

theorem inv_def (x : α) (y : β) : r.inv y x ↔ r x y :=
  Iff.rfl

Characterization of Inverse Relation: $r^{-1}(y, x) \leftrightarrow r(x, y)$

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, and for any elements $x \in \alpha$ and $y \in \beta$, the inverse relation $r^{-1}$ satisfies $r^{-1}(y, x) \leftrightarrow r(x, y)$.

Rel.inv_inv theorem

: inv (inv r) = r

Full source

theorem inv_inv : inv (inv r) = r := by
  ext x y
  rfl

Double Inverse of Relation Equals Original Relation

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the inverse of the inverse relation equals the original relation, i.e., $(r^{-1})^{-1} = r$.

Rel.dom definition

Full source

/-- Domain of a relation -/
def dom := { x | ∃ y, r x y }

Domain of a relation

Informal description

The domain of a relation $r$ between types $\alpha$ and $\beta$ is the set of all elements $x \in \alpha$ for which there exists some $y \in \beta$ such that $r(x, y)$ holds. In other words, $\text{dom}(r) = \{x \in \alpha \mid \exists y \in \beta, r(x, y)\}$.

Rel.dom_mono theorem

{r s : Rel α β} (h : r ≤ s) : dom r ⊆ dom s

Full source

theorem dom_mono {r s : Rel α β} (h : r ≤ s) : domdom r ⊆ dom s := fun a ⟨b, hx⟩ => ⟨b, h a b hx⟩

Monotonicity of Relation Domains with Respect to Relation Inclusion

Informal description

For any two relations $r$ and $s$ between types $\alpha$ and $\beta$, if $r$ is pointwise less than or equal to $s$ (i.e., $r(x,y) \to s(x,y)$ for all $x \in \alpha$ and $y \in \beta$), then the domain of $r$ is a subset of the domain of $s$.

Rel.codom definition

Full source

/-- Codomain aka range of a relation -/
def codom := { y | ∃ x, r x y }

Codomain of a relation

Informal description

The codomain (or range) of a relation $r$ between types $\alpha$ and $\beta$ is the set of all elements $y \in \beta$ for which there exists some $x \in \alpha$ such that $r(x, y)$ holds. In other words, $\text{codom}(r) = \{y \in \beta \mid \exists x \in \alpha, r(x, y)\}$.

Rel.codom_inv theorem

: r.inv.codom = r.dom

Full source

theorem codom_inv : r.inv.codom = r.dom := by
  ext x
  rfl

Codomain of Inverse Relation Equals Domain of Original Relation

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the codomain of its inverse relation $r^{-1}$ is equal to the domain of $r$. In other words, $\text{codom}(r^{-1}) = \text{dom}(r)$.

Rel.dom_inv theorem

: r.inv.dom = r.codom

Full source

theorem dom_inv : r.inv.dom = r.codom := by
  ext x
  rfl

Domain of Inverse Relation Equals Codomain of Original Relation

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the domain of its inverse relation $r^{-1}$ is equal to the codomain of $r$. In other words, $\text{dom}(r^{-1}) = \text{codom}(r)$.

Rel.comp definition

(r : Rel α β) (s : Rel β γ) : Rel α γ

Full source

/-- Composition of relation; note that it follows the `CategoryTheory/` order of arguments. -/
def comp (r : Rel α β) (s : Rel β γ) : Rel α γ := fun x z => ∃ y, r x y ∧ s y z

Composition of relations

Informal description

The composition of relations $r : \alpha \to \beta \to \text{Prop}$ and $s : \beta \to \gamma \to \text{Prop}$ is the relation $r \circ s : \alpha \to \gamma \to \text{Prop}$ defined by $(r \circ s)(x, z) \coloneqq \exists y \in \beta, r(x, y) \land s(y, z)$. This follows the category-theoretic order of composition.

Rel.comp_assoc theorem

{δ : Type*} (r : Rel α β) (s : Rel β γ) (t : Rel γ δ) : (r • s) • t = r • (s • t)

Full source

theorem comp_assoc {δ : Type*} (r : Rel α β) (s : Rel β γ) (t : Rel γ δ) :
    (r • s) • t = r • (s • t) := by
  unfold comp; ext (x w); constructor
  · rintro ⟨z, ⟨y, rxy, syz⟩, tzw⟩; exact ⟨y, rxy, z, syz, tzw⟩
  · rintro ⟨y, rxy, z, syz, tzw⟩; exact ⟨z, ⟨y, rxy, syz⟩, tzw⟩

Associativity of Relation Composition

Informal description

For any relations $r : \alpha \to \beta \to \text{Prop}$, $s : \beta \to \gamma \to \text{Prop}$, and $t : \gamma \to \delta \to \text{Prop}$, the composition of relations is associative, i.e., $(r \circ s) \circ t = r \circ (s \circ t)$.

Rel.comp_right_id theorem

(r : Rel α β) : r • @Eq β = r

Full source

@[simp]
theorem comp_right_id (r : Rel α β) : r • @Eq β = r := by
  unfold comp
  ext y
  simp

Right Identity Property of Relation Composition with Equality

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the composition of $r$ with the equality relation on $\beta$ is equal to $r$ itself. In other words, $r \circ \text{Eq}_\beta = r$.

Rel.comp_left_id theorem

(r : Rel α β) : @Eq α • r = r

Full source

@[simp]
theorem comp_left_id (r : Rel α β) : @Eq α • r = r := by
  unfold comp
  ext x
  simp

Left Identity Property of Relation Composition with Equality

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the composition of the equality relation on $\alpha$ with $r$ is equal to $r$ itself. In other words, $\text{Eq}_\alpha \circ r = r$.

Rel.comp_right_bot theorem

(r : Rel α β) : r • (⊥ : Rel β γ) = ⊥

Full source

@[simp]
theorem comp_right_bot (r : Rel α β) : r • (⊥ : Rel β γ) = ⊥ := by
  ext x y
  simp [comp, Bot.bot]

Composition with Bottom Relation Yields Bottom Relation

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the composition of $r$ with the bottom relation $\bot$ (the empty relation) from $\beta$ to $\gamma$ results in the bottom relation $\bot$ from $\alpha$ to $\gamma$. In other words, $r \circ \bot = \bot$.

Rel.comp_left_bot theorem

(r : Rel α β) : (⊥ : Rel γ α) • r = ⊥

Full source

@[simp]
theorem comp_left_bot (r : Rel α β) : (⊥ : Rel γ α) • r = ⊥ := by
  ext x y
  simp [comp, Bot.bot]

Left Composition with Bottom Relation Yields Bottom Relation

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the composition of the bottom relation $\bot$ (the empty relation) from $\gamma$ to $\alpha$ with $r$ results in the bottom relation $\bot$ from $\gamma$ to $\beta$. In other words, $\bot \circ r = \bot$.

Rel.comp_right_top theorem

(r : Rel α β) : r • (⊤ : Rel β γ) = fun x _ ↦ x ∈ r.dom

Full source

@[simp]
theorem comp_right_top (r : Rel α β) : r • (⊤ : Rel β γ) = fun x _ ↦ x ∈ r.dom := by
  ext x z
  simp [comp, Top.top, dom]

Composition with Top Relation Yields Domain Condition

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the composition of $r$ with the top relation $\top$ (the total relation) from $\beta$ to $\gamma$ yields the relation that holds between $x \in \alpha$ and any $z \in \gamma$ if and only if $x$ belongs to the domain of $r$. In other words, $r \circ \top = \{(x,z) \mid x \in \text{dom}(r)\}$.

Rel.comp_left_top theorem

(r : Rel α β) : (⊤ : Rel γ α) • r = fun _ y ↦ y ∈ r.codom

Full source

@[simp]
theorem comp_left_top (r : Rel α β) : (⊤ : Rel γ α) • r = fun _ y ↦ y ∈ r.codom := by
  ext x z
  simp [comp, Top.top, codom]

Composition with Total Relation Yields Codomain Condition

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the composition of the total relation $\top$ from $\gamma$ to $\alpha$ with $r$ yields the relation that holds between any $x \in \gamma$ and $y \in \beta$ if and only if $y$ belongs to the codomain of $r$. In other words, $\top \circ r = \{(x,y) \mid y \in \text{codom}(r)\}$.

Rel.inv_id theorem

: inv (@Eq α) = @Eq α

Full source

theorem inv_id : inv (@Eq α) = @Eq α := by
  ext x y
  constructor <;> apply Eq.symm

Inverse of Equality Relation is Equality Relation

Informal description

The inverse of the equality relation on a type $\alpha$ is the equality relation itself, i.e., $(\text{Eq}_{\alpha})^{-1} = \text{Eq}_{\alpha}$.

Rel.inv_comp theorem

(r : Rel α β) (s : Rel β γ) : inv (r • s) = inv s • inv r

Full source

theorem inv_comp (r : Rel α β) (s : Rel β γ) : inv (r • s) = invinv s • inv r := by
  ext x z
  simp [comp, inv, flip, and_comm]

Inverse of Relation Composition: $(r \circ s)^{-1} = s^{-1} \circ r^{-1}$

Informal description

For any relations $r : \alpha \to \beta \to \text{Prop}$ and $s : \beta \to \gamma \to \text{Prop}$, the inverse of the composition $r \circ s$ is equal to the composition of the inverses in reverse order, i.e., $(r \circ s)^{-1} = s^{-1} \circ r^{-1}$.

Rel.inv_bot theorem

: (⊥ : Rel α β).inv = (⊥ : Rel β α)

Full source

@[simp]
theorem inv_bot : (⊥ : Rel α β).inv = (⊥ : Rel β α) := by
  simp [Bot.bot, inv, Function.flip_def]

Inverse of Bottom Relation is Bottom Relation

Informal description

The inverse of the bottom relation (the relation that relates no elements of $\alpha$ to any elements of $\beta$) is equal to the bottom relation between $\beta$ and $\alpha$.

Rel.inv_top theorem

: (⊤ : Rel α β).inv = (⊤ : Rel β α)

Full source

@[simp]
theorem inv_top : (⊤ : Rel α β).inv = (⊤ : Rel β α) := by
  simp [Top.top, inv, Function.flip_def]

Inverse of Top Relation is Top Relation

Informal description

The inverse of the top relation (the relation that relates every element of $\alpha$ to every element of $\beta$) is equal to the top relation between $\beta$ and $\alpha$.

Rel.image definition

(s : Set α) : Set β

Full source

/-- Image of a set under a relation -/
def image (s : Set α) : Set β := { y | ∃ x ∈ s, r x y }

Image of a set under a relation

Informal description

Given a relation $r$ between types $\alpha$ and $\beta$ and a subset $s$ of $\alpha$, the image of $s$ under $r$ is the set of all elements $y \in \beta$ such that there exists an $x \in s$ with $r(x, y)$.

Rel.mem_image theorem

(y : β) (s : Set α) : y ∈ image r s ↔ ∃ x ∈ s, r x y

Full source

theorem mem_image (y : β) (s : Set α) : y ∈ image r sy ∈ image r s ↔ ∃ x ∈ s, r x y :=
  Iff.rfl

Characterization of Membership in Relation Image

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, an element $y \in \beta$ belongs to the image of a subset $s \subseteq \alpha$ under $r$ if and only if there exists an element $x \in s$ such that $r(x, y)$ holds.

Rel.image_subset theorem

: ((· ⊆ ·) ⇒ (· ⊆ ·)) r.image r.image

Full source

theorem image_subset : ((· ⊆ ·) ⇒ (· ⊆ ·)) r.image r.image := fun _ _ h _ ⟨x, xs, rxy⟩ =>
  ⟨x, h xs, rxy⟩

Monotonicity of Relation Image under Subset Inclusion

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the image operation $r.\text{image}$ is covariant with respect to the subset relation $\subseteq$. That is, if $s \subseteq t$ are subsets of $\alpha$, then $r.\text{image}(s) \subseteq r.\text{image}(t)$.

Rel.image_mono theorem

: Monotone r.image

Full source

theorem image_mono : Monotone r.image :=
  r.image_subset

Monotonicity of Relation Image

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the image operation $r.\text{image}$ is monotone. That is, if $s \subseteq t$ are subsets of $\alpha$, then $r.\text{image}(s) \subseteq r.\text{image}(t)$.

Rel.image_inter theorem

(s t : Set α) : r.image (s ∩ t) ⊆ r.image s ∩ r.image t

Full source

theorem image_inter (s t : Set α) : r.image (s ∩ t) ⊆ r.image s ∩ r.image t :=
  r.image_mono.map_inf_le s t

Image of Intersection under Relation is Contained in Intersection of Images

Informal description

For any relation $r$ between types $\alpha$ and $\beta$ and any subsets $s, t \subseteq \alpha$, the image of the intersection $s \cap t$ under $r$ is contained in the intersection of the images of $s$ and $t$ under $r$, i.e., \[ r(s \cap t) \subseteq r(s) \cap r(t). \]

Rel.image_union theorem

(s t : Set α) : r.image (s ∪ t) = r.image s ∪ r.image t

Full source

theorem image_union (s t : Set α) : r.image (s ∪ t) = r.image s ∪ r.image t :=
  le_antisymm
    (fun _y ⟨x, xst, rxy⟩ =>
      xst.elim (fun xs => Or.inl ⟨x, ⟨xs, rxy⟩⟩) fun xt => Or.inr ⟨x, ⟨xt, rxy⟩⟩)
    (r.image_mono.le_map_sup s t)

Image of Union under Relation Equals Union of Images

Informal description

For any relation $r$ between types $\alpha$ and $\beta$ and any subsets $s, t$ of $\alpha$, the image of the union $s \cup t$ under $r$ is equal to the union of the images of $s$ and $t$ under $r$, i.e., $$ r(s \cup t) = r(s) \cup r(t). $$

Rel.image_id theorem

(s : Set α) : image (@Eq α) s = s

Full source

@[simp]
theorem image_id (s : Set α) : image (@Eq α) s = s := by
  ext x
  simp [mem_image]

Image of Set Under Equality Relation is the Set Itself

Informal description

For any set $s$ of elements of type $\alpha$, the image of $s$ under the equality relation (i.e., the relation $\{(x, y) \mid x = y\}$) is equal to $s$ itself. In other words, $\{y \mid \exists x \in s, x = y\} = s$.

Rel.image_comp theorem

(s : Rel β γ) (t : Set α) : image (r • s) t = image s (image r t)

Full source

theorem image_comp (s : Rel β γ) (t : Set α) : image (r • s) t = image s (image r t) := by
  ext z; simp only [mem_image]; constructor
  · rintro ⟨x, xt, y, rxy, syz⟩; exact ⟨y, ⟨x, xt, rxy⟩, syz⟩
  · rintro ⟨y, ⟨x, xt, rxy⟩, syz⟩; exact ⟨x, xt, y, rxy, syz⟩

Image of Composition of Relations Equals Composition of Images

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, any relation $s$ between $\beta$ and $\gamma$, and any subset $t$ of $\alpha$, the image of $t$ under the composition $r \circ s$ is equal to the image under $s$ of the image of $t$ under $r$. In symbols: $$ (r \circ s)(t) = s(r(t)) $$

Rel.image_univ theorem

: r.image Set.univ = r.codom

Full source

theorem image_univ : r.image Set.univ = r.codom := by
  ext y
  simp [mem_image, codom]

Image of Universal Set Equals Codomain of Relation

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the image of the universal set $\text{univ} : \text{Set } \alpha$ under $r$ is equal to the codomain of $r$, i.e., $r(\text{univ}) = \text{codom}(r)$.

Rel.image_empty theorem

: r.image ∅ = ∅

Full source

@[simp]
theorem image_empty : r.image ∅ = ∅ := by
  ext x
  simp [mem_image]

Image of Empty Set is Empty

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the image of the empty set under $r$ is the empty set, i.e., $r(\emptyset) = \emptyset$.

Rel.image_bot theorem

(s : Set α) : (⊥ : Rel α β).image s = ∅

Full source

@[simp]
theorem image_bot (s : Set α) : (⊥ : Rel α β).image s = ∅ := by
  rw [Set.eq_empty_iff_forall_not_mem]
  intro x h
  simp [mem_image, Bot.bot] at h

Image of Any Set Under Bottom Relation is Empty

Informal description

For any set $s$ of type $\alpha$, the image of $s$ under the bottom relation $\bot$ (which relates no elements) is the empty set, i.e., $\bot(s) = \emptyset$.

Rel.image_top theorem

{s : Set α} (h : Set.Nonempty s) : (⊤ : Rel α β).image s = Set.univ

Full source

@[simp]
theorem image_top {s : Set α} (h : Set.Nonempty s) :
    (⊤ : Rel α β).image s = Set.univ :=
  Set.eq_univ_of_forall fun _ ↦ ⟨h.some, by simp [h.some_mem, Top.top]⟩

Image of Nonempty Set under Universal Relation is Entire Codomain

Informal description

For any nonempty set $s \subseteq \alpha$, the image of $s$ under the universal relation $\top$ (which relates every element of $\alpha$ to every element of $\beta$) is the entire set $\beta$, i.e., $\top(s) = \beta$.

Rel.preimage definition

(s : Set β) : Set α

Full source

/-- Preimage of a set under a relation `r`. Same as the image of `s` under `r.inv` -/
def preimage (s : Set β) : Set α :=
  r.inv.image s

Preimage of a set under a relation

Informal description

Given a relation $r$ between types $\alpha$ and $\beta$ and a subset $s$ of $\beta$, the preimage of $s$ under $r$ is the set of all elements $x \in \alpha$ such that there exists a $y \in s$ with $r(x, y)$. This is equivalent to the image of $s$ under the inverse relation $r^{-1}$.

Rel.mem_preimage theorem

(x : α) (s : Set β) : x ∈ r.preimage s ↔ ∃ y ∈ s, r x y

Full source

theorem mem_preimage (x : α) (s : Set β) : x ∈ r.preimage sx ∈ r.preimage s ↔ ∃ y ∈ s, r x y :=
  Iff.rfl

Characterization of Preimage Membership in Relations

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, an element $x \in \alpha$ belongs to the preimage of a set $s \subseteq \beta$ under $r$ if and only if there exists an element $y \in s$ such that $r(x, y)$ holds. In symbols: \[ x \in r^{-1}(s) \iff \exists y \in s, r(x, y). \]

Rel.preimage_def theorem

(s : Set β) : preimage r s = {x | ∃ y ∈ s, r x y}

Full source

theorem preimage_def (s : Set β) : preimage r s = { x | ∃ y ∈ s, r x y } :=
  Set.ext fun _ => mem_preimage _ _ _

Definition of Relation Preimage as Set Comprehension

Informal description

For a relation $r$ between types $\alpha$ and $\beta$ and a subset $s \subseteq \beta$, the preimage of $s$ under $r$ is equal to the set of all elements $x \in \alpha$ for which there exists $y \in s$ such that $r(x, y)$ holds. In symbols: \[ r^{-1}(s) = \{x \mid \exists y \in s, r(x, y)\}. \]

Rel.preimage_mono theorem

{s t : Set β} (h : s ⊆ t) : r.preimage s ⊆ r.preimage t

Full source

theorem preimage_mono {s t : Set β} (h : s ⊆ t) : r.preimage s ⊆ r.preimage t :=
  image_mono _ h

Monotonicity of Relation Preimage

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, and any subsets $s, t \subseteq \beta$ such that $s \subseteq t$, the preimage of $s$ under $r$ is a subset of the preimage of $t$ under $r$. In symbols: \[ s \subseteq t \implies r^{-1}(s) \subseteq r^{-1}(t). \]

Rel.preimage_inter theorem

(s t : Set β) : r.preimage (s ∩ t) ⊆ r.preimage s ∩ r.preimage t

Full source

theorem preimage_inter (s t : Set β) : r.preimage (s ∩ t) ⊆ r.preimage s ∩ r.preimage t :=
  image_inter _ s t

Preimage of Intersection under Relation is Contained in Intersection of Preimages

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, and any subsets $s, t \subseteq \beta$, the preimage of the intersection $s \cap t$ under $r$ is contained in the intersection of the preimages of $s$ and $t$ under $r$, i.e., \[ r^{-1}(s \cap t) \subseteq r^{-1}(s) \cap r^{-1}(t). \]

Rel.preimage_union theorem

(s t : Set β) : r.preimage (s ∪ t) = r.preimage s ∪ r.preimage t

Full source

theorem preimage_union (s t : Set β) : r.preimage (s ∪ t) = r.preimage s ∪ r.preimage t :=
  image_union _ s t

Preimage of Union under Relation Equals Union of Preimages

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, and any subsets $s, t \subseteq \beta$, the preimage of the union $s \cup t$ under $r$ is equal to the union of the preimages of $s$ and $t$ under $r$, i.e., $$ r^{-1}(s \cup t) = r^{-1}(s) \cup r^{-1}(t). $$

Rel.preimage_id theorem

(s : Set α) : preimage (@Eq α) s = s

Full source

theorem preimage_id (s : Set α) : preimage (@Eq α) s = s := by
  simp only [preimage, inv_id, image_id]

Preimage of Set Under Equality Relation is the Set Itself

Informal description

For any set $s$ of elements of type $\alpha$, the preimage of $s$ under the equality relation (i.e., the relation $\{(x, y) \mid x = y\}$) is equal to $s$ itself. In other words, $\{x \mid \exists y \in s, x = y\} = s$.

Rel.preimage_comp theorem

(s : Rel β γ) (t : Set γ) : preimage (r • s) t = preimage r (preimage s t)

Full source

theorem preimage_comp (s : Rel β γ) (t : Set γ) :
    preimage (r • s) t = preimage r (preimage s t) := by simp only [preimage, inv_comp, image_comp]

Preimage of Composition of Relations: $(r \circ s)^{-1}(t) = r^{-1}(s^{-1}(t))$

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, any relation $s$ between $\beta$ and $\gamma$, and any subset $t$ of $\gamma$, the preimage of $t$ under the composition $r \circ s$ is equal to the preimage under $r$ of the preimage of $t$ under $s$. In symbols: $$ (r \circ s)^{-1}(t) = r^{-1}(s^{-1}(t)) $$

Rel.preimage_univ theorem

: r.preimage Set.univ = r.dom

Full source

theorem preimage_univ : r.preimage Set.univ = r.dom := by rw [preimage, image_univ, codom_inv]

Preimage of Universal Set Equals Domain of Relation

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the preimage of the universal set $\text{univ} \subseteq \beta$ under $r$ is equal to the domain of $r$, i.e., $r^{-1}(\text{univ}) = \text{dom}(r)$.

Rel.preimage_empty theorem

: r.preimage ∅ = ∅

Full source

@[simp]
theorem preimage_empty : r.preimage ∅ = ∅ := by rw [preimage, image_empty]

Preimage of Empty Set is Empty

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the preimage of the empty set under $r$ is the empty set, i.e., $r^{-1}(\emptyset) = \emptyset$.

Rel.preimage_inv theorem

(s : Set α) : r.inv.preimage s = r.image s

Full source

@[simp]
theorem preimage_inv (s : Set α) : r.inv.preimage s = r.image s := by rw [preimage, inv_inv]

Preimage Under Inverse Relation Equals Image Under Original Relation

Informal description

For any relation $r$ between types $\alpha$ and $\beta$ and any subset $s$ of $\alpha$, the preimage of $s$ under the inverse relation $r^{-1}$ equals the image of $s$ under $r$. In other words, $r^{-1}.preimage(s) = r.image(s)$.

Rel.preimage_bot theorem

(s : Set β) : (⊥ : Rel α β).preimage s = ∅

Full source

@[simp]
theorem preimage_bot (s : Set β) : (⊥ : Rel α β).preimage s = ∅ := by
  rw [preimage, inv_bot, image_bot]

Preimage Under Bottom Relation is Empty

Informal description

For any set $s$ of type $\beta$, the preimage of $s$ under the bottom relation $\bot$ (which relates no elements of $\alpha$ to any elements of $\beta$) is the empty set, i.e., $\bot^{-1}(s) = \emptyset$.

Rel.preimage_top theorem

{s : Set β} (h : Set.Nonempty s) : (⊤ : Rel α β).preimage s = Set.univ

Full source

@[simp]
theorem preimage_top {s : Set β} (h : Set.Nonempty s) :
    (⊤ : Rel α β).preimage s = Set.univ := by rwa [← inv_top, preimage, inv_inv, image_top]

Preimage of Nonempty Set under Universal Relation is Entire Domain

Informal description

For any nonempty set $s \subseteq \beta$, the preimage of $s$ under the universal relation $\top$ (which relates every element of $\alpha$ to every element of $\beta$) is the entire set $\alpha$, i.e., $\top^{-1}(s) = \alpha$.

Rel.image_eq_dom_of_codomain_subset theorem

{s : Set β} (h : r.codom ⊆ s) : r.preimage s = r.dom

Full source

theorem image_eq_dom_of_codomain_subset {s : Set β} (h : r.codom ⊆ s) : r.preimage s = r.dom := by
  rw [← preimage_univ]
  apply Set.eq_of_subset_of_subset
  · exact image_subset _ (Set.subset_univ _)
  · intro x hx
    simp only [mem_preimage, Set.mem_univ, true_and] at hx
    rcases hx with ⟨y, ryx⟩
    have hy : y ∈ s := h ⟨x, ryx⟩
    exact ⟨y, ⟨hy, ryx⟩⟩

Preimage Equals Domain When Codomain is Subset

Informal description

For any relation $r$ between types $\alpha$ and $\beta$ and any subset $s$ of $\beta$, if the codomain of $r$ is a subset of $s$, then the preimage of $s$ under $r$ equals the domain of $r$, i.e., $r^{-1}(s) = \text{dom}(r)$.

Rel.preimage_eq_codom_of_domain_subset theorem

{s : Set α} (h : r.dom ⊆ s) : r.image s = r.codom

Full source

theorem preimage_eq_codom_of_domain_subset {s : Set α} (h : r.dom ⊆ s) : r.image s = r.codom := by
  apply r.inv.image_eq_dom_of_codomain_subset (by rwa [← codom_inv] at h)

Image Equals Codomain When Domain is Subset

Informal description

For any relation $r$ between types $\alpha$ and $\beta$ and any subset $s$ of $\alpha$, if the domain of $r$ is contained in $s$, then the image of $s$ under $r$ equals the codomain of $r$, i.e., $r(s) = \text{codom}(r)$.

Rel.image_inter_dom_eq theorem

(s : Set α) : r.image (s ∩ r.dom) = r.image s

Full source

theorem image_inter_dom_eq (s : Set α) : r.image (s ∩ r.dom) = r.image s := by
  apply Set.eq_of_subset_of_subset
  · apply r.image_mono (by simp)
  · intro x h
    rw [mem_image] at *
    rcases h with ⟨y, hy, ryx⟩
    use y
    suffices h : y ∈ r.dom by simp_all only [Set.mem_inter_iff, and_self]
    rw [dom, Set.mem_setOf_eq]
    use x

Image of Intersection with Domain Equals Image

Informal description

For any relation $r$ between types $\alpha$ and $\beta$ and any subset $s$ of $\alpha$, the image of $s \cap \text{dom}(r)$ under $r$ is equal to the image of $s$ under $r$. That is, $r(s \cap \text{dom}(r)) = r(s)$.

Rel.preimage_inter_codom_eq theorem

(s : Set β) : r.preimage (s ∩ r.codom) = r.preimage s

Full source

@[simp]
theorem preimage_inter_codom_eq (s : Set β) : r.preimage (s ∩ r.codom) = r.preimage s := by
  rw [← dom_inv, preimage, preimage, image_inter_dom_eq]

Preimage of Intersection with Codomain Equals Preimage

Informal description

For any relation $r$ between types $\alpha$ and $\beta$ and any subset $s$ of $\beta$, the preimage of $s \cap \text{codom}(r)$ under $r$ is equal to the preimage of $s$ under $r$. In other words, $r^{-1}(s \cap \text{codom}(r)) = r^{-1}(s)$.

Rel.inter_dom_subset_preimage_image theorem

(s : Set α) : s ∩ r.dom ⊆ r.preimage (r.image s)

Full source

theorem inter_dom_subset_preimage_image (s : Set α) : s ∩ r.doms ∩ r.dom ⊆ r.preimage (r.image s) := by
  intro x hx
  simp only [Set.mem_inter_iff, dom] at hx
  rcases hx with ⟨hx, ⟨y, rxy⟩⟩
  use y
  simp only [image, Set.mem_setOf_eq]
  exact ⟨⟨x, hx, rxy⟩, rxy⟩

Domain-Restricted Subset is Contained in Preimage of Image

Informal description

For any relation $r$ between types $\alpha$ and $\beta$ and any subset $s$ of $\alpha$, the intersection of $s$ with the domain of $r$ is contained in the preimage of the image of $s$ under $r$. In other words, $s \cap \text{dom}(r) \subseteq r^{-1}(r(s))$.

Rel.image_preimage_subset_inter_codom theorem

(s : Set β) : s ∩ r.codom ⊆ r.image (r.preimage s)

Full source

theorem image_preimage_subset_inter_codom (s : Set β) : s ∩ r.codoms ∩ r.codom ⊆ r.image (r.preimage s) := by
  rw [← dom_inv, ← preimage_inv]
  apply inter_dom_subset_preimage_image

Image-Preimage Inclusion for Relations: $s \cap \text{codom}(r) \subseteq r(r^{-1}(s))$

Informal description

For any relation $r$ between types $\alpha$ and $\beta$ and any subset $s$ of $\beta$, the intersection of $s$ with the codomain of $r$ is contained in the image of the preimage of $s$ under $r$. In other words, $s \cap \text{codom}(r) \subseteq r(r^{-1}(s))$.

Rel.core definition

(s : Set β)

Full source

/-- Core of a set `s : Set β` w.r.t `r : Rel α β` is the set of `x : α` that are related *only*
to elements of `s`. Other generalization of `Function.preimage`. -/
def core (s : Set β) := { x | ∀ y, r x y → y ∈ s }

Core of a set under a relation

Informal description

The core of a set $s \subseteq \beta$ with respect to a relation $r : \alpha \to \beta \to \text{Prop}$ is the set of all elements $x \in \alpha$ such that for every $y \in \beta$, if $x$ is related to $y$ by $r$, then $y$ must belong to $s$. In other words, $x$ is in the core of $s$ if all elements related to $x$ under $r$ are contained in $s$.

Rel.mem_core theorem

(x : α) (s : Set β) : x ∈ r.core s ↔ ∀ y, r x y → y ∈ s

Full source

theorem mem_core (x : α) (s : Set β) : x ∈ r.core sx ∈ r.core s ↔ ∀ y, r x y → y ∈ s :=
  Iff.rfl

Characterization of Core Membership in Relations

Informal description

For a relation $r$ between types $\alpha$ and $\beta$, an element $x \in \alpha$, and a set $s \subseteq \beta$, we have $x$ belongs to the core of $s$ under $r$ if and only if for every $y \in \beta$, if $x$ is related to $y$ by $r$, then $y$ must belong to $s$. In symbols: $$x \in r.core(s) \leftrightarrow (\forall y \in \beta, r(x,y) \rightarrow y \in s)$$

Rel.core_subset theorem

: ((· ⊆ ·) ⇒ (· ⊆ ·)) r.core r.core

Full source

theorem core_subset : ((· ⊆ ·) ⇒ (· ⊆ ·)) r.core r.core := fun _s _t h _x h' y rxy => h (h' y rxy)

Monotonicity of Relation Core with Respect to Subset Inclusion

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the core operation $r^{\text{core}}$ is subset-preserving. That is, for any sets $s, t \subseteq \beta$, if $s \subseteq t$, then $r^{\text{core}}(s) \subseteq r^{\text{core}}(t)$.

Rel.core_mono theorem

: Monotone r.core

Full source

theorem core_mono : Monotone r.core :=
  r.core_subset

Monotonicity of Relation Core

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the core operation $r^{\text{core}}$ is monotone. That is, for any sets $s, t \subseteq \beta$, if $s \subseteq t$, then $r^{\text{core}}(s) \subseteq r^{\text{core}}(t)$.

Rel.core_inter theorem

(s t : Set β) : r.core (s ∩ t) = r.core s ∩ r.core t

Full source

theorem core_inter (s t : Set β) : r.core (s ∩ t) = r.core s ∩ r.core t :=
  Set.ext (by simp [mem_core, imp_and, forall_and])

Core of Intersection Equals Intersection of Cores

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, and any sets $s, t \subseteq \beta$, the core of the intersection $s \cap t$ under $r$ is equal to the intersection of the cores of $s$ and $t$ under $r$. In other words: $$ r^{\text{core}}(s \cap t) = r^{\text{core}}(s) \cap r^{\text{core}}(t) $$ where $r^{\text{core}}(u) = \{x \in \alpha \mid \forall y \in \beta, r(x,y) \to y \in u\}$.

Rel.core_union theorem

(s t : Set β) : r.core s ∪ r.core t ⊆ r.core (s ∪ t)

Full source

theorem core_union (s t : Set β) : r.core s ∪ r.core tr.core s ∪ r.core t ⊆ r.core (s ∪ t) :=
  r.core_mono.le_map_sup s t

Union of Cores is Subset of Core of Union

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, and any sets $s, t \subseteq \beta$, the union of the cores of $s$ and $t$ under $r$ is a subset of the core of the union $s \cup t$ under $r$. In other words: $$ r^{\text{core}}(s) \cup r^{\text{core}}(t) \subseteq r^{\text{core}}(s \cup t) $$ where $r^{\text{core}}(u) = \{x \in \alpha \mid \forall y \in \beta, r(x,y) \to y \in u\}$.

Rel.core_univ theorem

: r.core Set.univ = Set.univ

Full source

@[simp]
theorem core_univ : r.core Set.univ = Set.univ :=
  Set.ext (by simp [mem_core])

Core of Universal Set is Universal Set

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the core of the universal set $\text{univ} \subseteq \beta$ under $r$ is equal to the universal set $\text{univ} \subseteq \alpha$. In other words, $\{x \in \alpha \mid \forall y \in \beta, r(x,y) \to y \in \text{univ}\} = \text{univ}$.

Rel.core_id theorem

(s : Set α) : core (@Eq α) s = s

Full source

theorem core_id (s : Set α) : core (@Eq α) s = s := by simp [core]

Core of Set under Equality Relation Equals Itself

Informal description

For any set $s \subseteq \alpha$, the core of $s$ with respect to the equality relation on $\alpha$ is equal to $s$ itself. In other words, $\{x \in \alpha \mid \forall y \in \alpha, x = y \to y \in s\} = s$.

Rel.core_comp theorem

(s : Rel β γ) (t : Set γ) : core (r • s) t = core r (core s t)

Full source

theorem core_comp (s : Rel β γ) (t : Set γ) : core (r • s) t = core r (core s t) := by
  ext x; simp only [core, comp, forall_exists_index, and_imp, Set.mem_setOf_eq]; constructor
  · exact fun h y rxy z => h z y rxy
  · exact fun h z y rzy => h y rzy z

Core of Composition Equals Composition of Cores

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, relation $s$ between $\beta$ and $\gamma$, and subset $t \subseteq \gamma$, the core of the composed relation $r \circ s$ with respect to $t$ is equal to the core of $r$ with respect to the core of $s$ with respect to $t$. In other words: $$\text{core}(r \circ s, t) = \text{core}(r, \text{core}(s, t))$$

Rel.restrictDomain definition

(s : Set α) : Rel { x // x ∈ s } β

Full source

/-- Restrict the domain of a relation to a subtype. -/
def restrictDomain (s : Set α) : Rel { x // x ∈ s } β := fun x y => r x.val y

Domain restriction of a relation

Informal description

Given a relation $r$ between types $\alpha$ and $\beta$ and a subset $s$ of $\alpha$, the restricted relation $\text{restrictDomain}\ r\ s$ is defined on the subtype $\{x \in \alpha \mid x \in s\}$ such that for any $x$ in this subtype and $y \in \beta$, $(\text{restrictDomain}\ r\ s)\ x\ y$ holds if and only if $r\ x\ y$ holds.

Rel.image_subset_iff theorem

(s : Set α) (t : Set β) : image r s ⊆ t ↔ s ⊆ core r t

Full source

theorem image_subset_iff (s : Set α) (t : Set β) : imageimage r s ⊆ timage r s ⊆ t ↔ s ⊆ core r t :=
  Iff.intro (fun h x xs _y rxy => h ⟨x, xs, rxy⟩) fun h y ⟨_x, xs, rxy⟩ => h xs y rxy

Image-Core Subset Equivalence for Relations

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, subset $s \subseteq \alpha$, and subset $t \subseteq \beta$, the image of $s$ under $r$ is contained in $t$ if and only if $s$ is contained in the core of $t$ under $r$. In other words: $$ r(s) \subseteq t \Leftrightarrow s \subseteq r^{-1}(t) $$ where $r(s)$ denotes the image of $s$ under $r$ and $r^{-1}(t)$ denotes the core of $t$ under $r$.

Rel.image_core_gc theorem

: GaloisConnection r.image r.core

Full source

theorem image_core_gc : GaloisConnection r.image r.core :=
  image_subset_iff _

Galois Connection Between Image and Core of a Relation

Informal description

For any relation $r$ between types $\alpha$ and $\beta$, the pair of functions $(r.\text{image}, r.\text{core})$ forms a Galois connection between the complete lattices of subsets of $\alpha$ and $\beta$. This means that for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, we have: $$ r(s) \subseteq t \Leftrightarrow s \subseteq r^{-1}(t) $$ where $r(s)$ denotes the image of $s$ under $r$ and $r^{-1}(t)$ denotes the core of $t$ under $r$.

Function.graph definition

(f : α → β) : Rel α β

Full source

/-- The graph of a function as a relation. -/
def graph (f : α → β) : Rel α β := fun x y => f x = y

Graph of a function

Informal description

The graph of a function $ f : \alpha \to \beta $ is the relation $ \text{graph}(f) $ between $ \alpha $ and $ \beta $ defined by $ \text{graph}(f)(x, y) $ if and only if $ f(x) = y $.

Function.graph_def theorem

(f : α → β) (x y) : f.graph x y ↔ (f x = y)

Full source

@[simp] lemma graph_def (f : α → β) (x y) : f.graph x y ↔ (f x = y) := Iff.rfl

Graph Relation Characterization: $\text{graph}(f)(x, y) \leftrightarrow f(x) = y$

Informal description

For any function $f : \alpha \to \beta$ and elements $x \in \alpha$, $y \in \beta$, the graph relation $\text{graph}(f)(x, y)$ holds if and only if $f(x) = y$.

Function.graph_injective theorem

: Injective (graph : (α → β) → Rel α β)

Full source

theorem graph_injective : Injective (graph : (α → β) → Rel α β) := by
  intro _ g h
  ext x
  have h2 := congr_fun₂ h x (g x)
  simp only [graph_def, eq_iff_iff, iff_true] at h2
  exact h2

Injectivity of the Graph Construction

Informal description

The function `graph` that maps a function $f : \alpha \to \beta$ to its graph relation is injective. That is, for any two functions $f, g : \alpha \to \beta$, if $\text{graph}(f) = \text{graph}(g)$, then $f = g$.

Function.graph_inj theorem

{f g : α → β} : f.graph = g.graph ↔ f = g

Full source

@[simp] lemma graph_inj {f g : α → β} : f.graph = g.graph ↔ f = g := graph_injective.eq_iff

Graph Equality Characterizes Function Equality

Informal description

For any two functions $f, g \colon \alpha \to \beta$, the graph of $f$ equals the graph of $g$ if and only if $f = g$.

Function.graph_id theorem

: graph id = @Eq α

Full source

theorem graph_id : graph id = @Eq α := by simp +unfoldPartialApp [graph]

Graph of Identity Function Equals Equality Relation

Informal description

The graph of the identity function $\text{id} : \alpha \to \alpha$ is equal to the equality relation on $\alpha$, i.e., $\text{graph}(\text{id}) = \{(x, x) \mid x \in \alpha\}$.

Function.graph_comp theorem

{f : β → γ} {g : α → β} : graph (f ∘ g) = Rel.comp (graph g) (graph f)

Full source

theorem graph_comp {f : β → γ} {g : α → β} : graph (f ∘ g) = Rel.comp (graph g) (graph f) := by
  ext x y
  simp [Rel.comp]

Graph of Function Composition Equals Composition of Graphs

Informal description

For any functions $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the graph of the composition $f \circ g$ is equal to the composition of the graphs of $g$ and $f$ as relations. That is, $\text{graph}(f \circ g) = \text{graph}(g) \circ \text{graph}(f)$.

Equiv.graph_inv theorem

(f : α ≃ β) : (f.symm : β → α).graph = Rel.inv (f : α → β).graph

Full source

theorem Equiv.graph_inv (f : α ≃ β) : (f.symm : β → α).graph = Rel.inv (f : α → β).graph := by
  ext x y
  aesop (add norm Rel.inv_def)

Graph of Inverse Equivalence Equals Inverse Graph Relation

Informal description

For any equivalence $f \colon \alpha \simeq \beta$, the graph of the inverse function $f^{-1} \colon \beta \to \alpha$ is equal to the inverse relation of the graph of $f \colon \alpha \to \beta$. That is, $\text{graph}(f^{-1}) = \text{graph}(f)^{-1}$.

Relation.is_graph_iff theorem

(r : Rel α β) : (∃! f, Function.graph f = r) ↔ ∀ x, ∃! y, r x y

Full source

theorem Relation.is_graph_iff (r : Rel α β) : (∃! f, Function.graph f = r) ↔ ∀ x, ∃! y, r x y := by
  unfold Function.graph
  constructor
  · rintro ⟨f, rfl, _⟩ x
    use f x
    simp only [forall_eq', and_self]
  · intro h
    choose f hf using fun x ↦ (h x).exists
    use f
    constructor
    · ext x _
      constructor
      · rintro rfl
        exact hf x
      · exact (h x).unique (hf x)
    · rintro _ rfl
      exact funext hf

Characterization of Functional Relations: $r$ is a Function Graph if and only if $r$ is Uniquely Determined at Every Point

Informal description

A relation $r$ between types $\alpha$ and $\beta$ is the graph of a unique function $f \colon \alpha \to \beta$ if and only if for every $x \in \alpha$, there exists a unique $y \in \beta$ such that $r(x, y)$ holds.

Set.image_eq theorem

(f : α → β) (s : Set α) : f '' s = (Function.graph f).image s

Full source

theorem image_eq (f : α → β) (s : Set α) : f '' s = (Function.graph f).image s := by
  rfl

Image of Set under Function Equals Image under Graph Relation

Informal description

For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image of $s$ under $f$ is equal to the image of $s$ under the graph relation of $f$. That is, $f(s) = \{y \in \beta \mid \exists x \in s, f(x) = y\}$.

Set.preimage_eq theorem

(f : α → β) (s : Set β) : f ⁻¹' s = (Function.graph f).preimage s

Full source

theorem preimage_eq (f : α → β) (s : Set β) : f ⁻¹' s = (Function.graph f).preimage s := by
  simp [Set.preimage, Rel.preimage, Rel.inv, flip, Rel.image]

Preimage Equals Graph Relation Preimage

Informal description

For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \beta$, the preimage $f^{-1}(s)$ is equal to the preimage of $s$ under the graph relation of $f$. That is, $$ f^{-1}(s) = \{x \in \alpha \mid \exists y \in s, (x, y) \in \text{graph}(f)\}. $$

Set.preimage_eq_core theorem

(f : α → β) (s : Set β) : f ⁻¹' s = (Function.graph f).core s

Full source

theorem preimage_eq_core (f : α → β) (s : Set β) : f ⁻¹' s = (Function.graph f).core s := by
  simp [Set.preimage, Rel.core]

Preimage as Core of Graph Relation

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \beta$, the preimage $f^{-1}(s)$ is equal to the core of $s$ under the graph relation of $f$. In other words, $f^{-1}(s) = \{x \in \alpha \mid \forall y, f(x) = y \implies y \in s\}$.

Mathlib.Data.Rel

Main declarations

TODO