Mathlib.Order.RelIso.Basic

RelHom structure

{α β : Type*} (r : α → α → Prop) (s : β → β → Prop)

Full source

/-- A relation homomorphism with respect to a given pair of relations `r` and `s`
is a function `f : α → β` such that `r a b → s (f a) (f b)`. -/
structure RelHom {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) where
  /-- The underlying function of a `RelHom` -/
  toFun : α → β
  /-- A `RelHom` sends related elements to related elements -/
  map_rel' : ∀ {a b}, r a b → s (toFun a) (toFun b)

Relation Homomorphism

Informal description

A relation homomorphism between two relations `r : α → α → Prop` and `s : β → β → Prop` is a function `f : α → β` such that for any `a, b : α`, if `r a b` holds, then `s (f a) (f b)` also holds. In other words, the function `f` preserves the relation `r` in the codomain relation `s`.

term_→r_ definition

: Lean.TrailingParserDescr✝

Full source

/-- A relation homomorphism with respect to a given pair of relations `r` and `s`
is a function `f : α → β` such that `r a b → s (f a) (f b)`. -/
infixl:25 " →r " => RelHom

Relation homomorphism

Informal description

Given two types $\alpha$ and $\beta$ with relations $r : \alpha \to \alpha \to \text{Prop}$ and $s : \beta \to \beta \to \text{Prop}$, a relation homomorphism $f : \alpha \to \beta$ is a function that preserves the relations, i.e., for any $a, b \in \alpha$, if $r(a, b)$ holds, then $s(f(a), f(b))$ must also hold.

RelHomClass structure

 (F : Type*) {α β : outParam Type*} (r : outParam <| α → α → Prop) (s : outParam <| β → β → Prop) [FunLike F α β]

Full source

/-- `RelHomClass F r s` asserts that `F` is a type of functions such that all `f : F`
satisfy `r a b → s (f a) (f b)`.

The relations `r` and `s` are `outParam`s since figuring them out from a goal is a higher-order
matching problem that Lean usually can't do unaided.
-/
class RelHomClass (F : Type*) {α β : outParam Type*} (r : outParam <| α → α → Prop)
  (s : outParam <| β → β → Prop) [FunLike F α β] : Prop where
  /-- A `RelHomClass` sends related elements to related elements -/
  map_rel : ∀ (f : F) {a b}, r a b → s (f a) (f b)

Relation Homomorphism Class

Informal description

The class `RelHomClass F r s` asserts that `F` is a type of functions where every `f : F` preserves the relation `r` to `s`, meaning that for any `a b : α`, if `r a b` holds, then `s (f a) (f b)` must also hold. Here, `r` and `s` are relations on types `α` and `β` respectively, and `F` is a type of functions from `α` to `β` that respects these relations.

RelHomClass.isIrrefl theorem

[RelHomClass F r s] (f : F) : ∀ [IsIrrefl β s], IsIrrefl α r

Full source

protected theorem isIrrefl [RelHomClass F r s] (f : F) : ∀ [IsIrrefl β s], IsIrrefl α r
  | ⟨H⟩ => ⟨fun _ h => H _ (map_rel f h)⟩

Irreflexivity Preservation under Relation Homomorphisms

Informal description

Let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves relations $r$ and $s$ (i.e., for any $f \in F$ and $a, b \in \alpha$, $r(a, b)$ implies $s(f(a), f(b))$). Given $f \in F$, if the relation $s$ on $\beta$ is irreflexive (i.e., for all $b \in \beta$, $\neg s(b, b)$), then the relation $r$ on $\alpha$ is also irreflexive (i.e., for all $a \in \alpha$, $\neg r(a, a)$).

RelHomClass.isAsymm theorem

[RelHomClass F r s] (f : F) : ∀ [IsAsymm β s], IsAsymm α r

Full source

protected theorem isAsymm [RelHomClass F r s] (f : F) : ∀ [IsAsymm β s], IsAsymm α r
  | ⟨H⟩ => ⟨fun _ _ h₁ h₂ => H _ _ (map_rel f h₁) (map_rel f h₂)⟩

Asymmetry Preservation under Relation Homomorphisms

Informal description

Let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves relations $r$ and $s$ (i.e., for any $f \in F$ and $a, b \in \alpha$, $r(a, b)$ implies $s(f(a), f(b))$). Given $f \in F$, if the relation $s$ on $\beta$ is asymmetric (i.e., for all $b_1, b_2 \in \beta$, $s(b_1, b_2)$ implies $\neg s(b_2, b_1)$), then the relation $r$ on $\alpha$ is also asymmetric (i.e., for all $a_1, a_2 \in \alpha$, $r(a_1, a_2)$ implies $\neg r(a_2, a_1)$).

RelHomClass.acc theorem

[RelHomClass F r s] (f : F) (a : α) : Acc s (f a) → Acc r a

Full source

protected theorem acc [RelHomClass F r s] (f : F) (a : α) : Acc s (f a) → Acc r a := by
  generalize h : f a = b
  intro ac
  induction ac generalizing a with | intro _ H IH => ?_
  subst h
  exact ⟨_, fun a' h => IH (f a') (map_rel f h) _ rfl⟩

Accessibility Preservation under Relation Homomorphisms

Informal description

Let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves relations $r$ and $s$ (i.e., for any $f \in F$ and $a, b \in \alpha$, $r(a, b)$ implies $s(f(a), f(b))$). Given $f \in F$ and $a \in \alpha$, if $f(a)$ is accessible with respect to the relation $s$, then $a$ is accessible with respect to the relation $r$.

RelHomClass.wellFounded theorem

[RelHomClass F r s] (f : F) : WellFounded s → WellFounded r

Full source

protected theorem wellFounded [RelHomClass F r s] (f : F) : WellFounded s → WellFounded r
  | ⟨H⟩ => ⟨fun _ => RelHomClass.acc f _ (H _)⟩

Well-foundedness Preservation under Relation Homomorphisms

Informal description

Let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves relations $r$ and $s$ (i.e., for any $f \in F$ and $a, b \in \alpha$, $r(a, b)$ implies $s(f(a), f(b))$). Given $f \in F$, if the relation $s$ on $\beta$ is well-founded, then the relation $r$ on $\alpha$ is also well-founded.

RelHomClass.isWellFounded theorem

[RelHomClass F r s] (f : F) [IsWellFounded β s] : IsWellFounded α r

Full source

protected theorem isWellFounded [RelHomClass F r s] (f : F) [IsWellFounded β s] :
    IsWellFounded α r :=
  ⟨RelHomClass.wellFounded f IsWellFounded.wf⟩

Well-foundedness Preservation under Relation Homomorphisms

Informal description

Let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves relations $r$ and $s$ (i.e., for any $f \in F$ and $a, b \in \alpha$, $r(a, b)$ implies $s(f(a), f(b))$). Given $f \in F$ and assuming the relation $s$ on $\beta$ is well-founded, the relation $r$ on $\alpha$ is also well-founded.

RelHom.instFunLike instance

: FunLike (r →r s) α β

Full source

instance : FunLike (r →r s) α β where
  coe o := o.toFun
  coe_injective' f g h := by
    cases f
    cases g
    congr

Relation Homomorphisms as Function-Like Types

Informal description

For any two relations $r$ on $\alpha$ and $s$ on $\beta$, the type of relation homomorphisms $r \to_r s$ is a function-like type, meaning its elements can be coerced to functions from $\alpha$ to $\beta$.

RelHom.instRelHomClass instance

: RelHomClass (r →r s) r s

Full source

instance : RelHomClass (r →r s) r s where
  map_rel := map_rel'

Relation Homomorphism Class for Relation Homomorphisms

Informal description

For any two relations $r$ on $\alpha$ and $s$ on $\beta$, the type of relation homomorphisms $r \to_r s$ forms a class of relation-preserving functions from $\alpha$ to $\beta$. This means every $f \in r \to_r s$ satisfies the property that if $r(a, b)$ holds for $a, b \in \alpha$, then $s(f(a), f(b))$ must also hold.

RelHom.map_rel theorem

(f : r →r s) {a b} : r a b → s (f a) (f b)

Full source

protected theorem map_rel (f : r →r s) {a b} : r a b → s (f a) (f b) :=
  f.map_rel'

Relation Homomorphism Preserves Relations

Informal description

For any relation homomorphism $f \colon r \to_r s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $a, b \in \alpha$, if $r(a, b)$ holds, then $s(f(a), f(b))$ also holds.

RelHom.coe_fn_toFun theorem

(f : r →r s) : f.toFun = (f : α → β)

Full source

@[simp]
theorem coe_fn_toFun (f : r →r s) : f.toFun = (f : α → β) :=
  rfl

Underlying Function of Relation Homomorphism Equals Coerced Function

Informal description

For any relation homomorphism $f \colon r \to_r s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the underlying function $f \colon \alpha \to \beta$ is equal to the function obtained by coercing $f$ to a function via the `FunLike` instance.

RelHom.coe_fn_injective theorem

: Injective fun (f : r →r s) => (f : α → β)

Full source

/-- The map `coe_fn : (r →r s) → (α → β)` is injective. -/
theorem coe_fn_injective : Injective fun (f : r →r s) => (f : α → β) :=
  DFunLike.coe_injective

Injectivity of the Relation Homomorphism to Function Map

Informal description

The canonical map from relation homomorphisms $f \colon r \to_r s$ to functions $\alpha \to \beta$ is injective. That is, if two relation homomorphisms $f, g \colon r \to_r s$ satisfy $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.

RelHom.ext theorem

⦃f g : r →r s⦄ (h : ∀ x, f x = g x) : f = g

Full source

@[ext]
theorem ext ⦃f g : r →r s⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

Extensionality of Relation Homomorphisms

Informal description

For any two relation homomorphisms $f, g \colon r \to_r s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.

RelHom.id definition

(r : α → α → Prop) : r →r r

Full source

/-- Identity map is a relation homomorphism. -/
@[refl, simps]
protected def id (r : α → α → Prop) : r →r r :=
  ⟨fun x => x, fun x => x⟩

Identity relation homomorphism

Informal description

The identity function serves as a relation homomorphism from a relation $r$ to itself, where $r$ is a binary relation on a type $\alpha$. Specifically, for any $x \in \alpha$, the identity function maps $x$ to itself, and preserves the relation $r$ in the sense that if $r a b$ holds for some $a, b \in \alpha$, then $r (\text{id } a) (\text{id } b)$ also holds.

RelHom.comp definition

(g : s →r t) (f : r →r s) : r →r t

Full source

/-- Composition of two relation homomorphisms is a relation homomorphism. -/
@[simps]
protected def comp (g : s →r t) (f : r →r s) : r →r t :=
  ⟨fun x => g (f x), fun h => g.2 (f.2 h)⟩

Composition of relation homomorphisms

Informal description

Given relation homomorphisms $g : s \to_r t$ and $f : r \to_r s$, their composition $g \circ f$ is a relation homomorphism from $r$ to $t$. Specifically, for any $a, b$ in the domain of $r$, if $r a b$ holds, then $t (g(f a)) (g(f b))$ holds.

RelHom.swap definition

(f : r →r s) : swap r →r swap s

Full source

/-- A relation homomorphism is also a relation homomorphism between dual relations. -/
protected def swap (f : r →r s) : swapswap r →r swap s :=
  ⟨f, f.map_rel⟩

Relation homomorphism between swapped relations

Informal description

Given a relation homomorphism $f \colon r \to_r s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the same function $f$ also serves as a relation homomorphism between the swapped relations $\text{swap}\, r$ on $\alpha$ and $\text{swap}\, s$ on $\beta$, where $\text{swap}\, r\, a\, b = r\, b\, a$ and similarly for $s$.

RelHom.preimage definition

(f : α → β) (s : β → β → Prop) : f ⁻¹'o s →r s

Full source

/-- A function is a relation homomorphism from the preimage relation of `s` to `s`. -/
def preimage (f : α → β) (s : β → β → Prop) : f ⁻¹'o sf ⁻¹'o s →r s :=
  ⟨f, id⟩

Preimage relation homomorphism

Informal description

Given a function $f : \alpha \to \beta$ and a relation $s : \beta \to \beta \to \text{Prop}$, the preimage relation $f^{-1}o\, s$ (defined by $f^{-1}o\, s\, a\, b \leftrightarrow s\, (f\, a)\, (f\, b)$) forms a relation homomorphism from $f^{-1}o\, s$ to $s$.

injective_of_increasing theorem

 (r : α → α → Prop) (s : β → β → Prop) [IsTrichotomous α r] [IsIrrefl β s] (f : α → β)
  (hf : ∀ {x y}, r x y → s (f x) (f y)) : Injective f

Full source

/-- An increasing function is injective -/
theorem injective_of_increasing (r : α → α → Prop) (s : β → β → Prop) [IsTrichotomous α r]
    [IsIrrefl β s] (f : α → β) (hf : ∀ {x y}, r x y → s (f x) (f y)) : Injective f := by
  intro x y hxy
  rcases trichotomous_of r x y with (h | h | h)
  · have := hf h
    rw [hxy] at this
    exfalso
    exact irrefl_of s (f y) this
  · exact h
  · have := hf h
    rw [hxy] at this
    exfalso
    exact irrefl_of s (f y) this

Injectivity of Increasing Functions on Trichotomous Domains

Informal description

Let $r$ be a trichotomous relation on a type $\alpha$ and $s$ an irreflexive relation on a type $\beta$. If $f : \alpha \to \beta$ is a function such that for all $x, y \in \alpha$, $r(x, y)$ implies $s(f(x), f(y))$, then $f$ is injective.

RelHom.injective_of_increasing theorem

[IsTrichotomous α r] [IsIrrefl β s] (f : r →r s) : Injective f

Full source

/-- An increasing function is injective -/
theorem RelHom.injective_of_increasing [IsTrichotomous α r] [IsIrrefl β s] (f : r →r s) :
    Injective f :=
  _root_.injective_of_increasing r s f f.map_rel

Injectivity of Relation Homomorphisms on Trichotomous Domains

Informal description

Let $r$ be a trichotomous relation on a type $\alpha$ and $s$ an irreflexive relation on a type $\beta$. If $f \colon r \to_r s$ is a relation homomorphism (i.e., $f$ preserves the relation $r$ in $s$), then $f$ is injective.

Function.Surjective.wellFounded_iff theorem

{f : α → β} (hf : Surjective f) (o : ∀ {a b}, r a b ↔ s (f a) (f b)) : WellFounded r ↔ WellFounded s

Full source

theorem Function.Surjective.wellFounded_iff {f : α → β} (hf : Surjective f)
    (o : ∀ {a b}, r a b ↔ s (f a) (f b)) :
    WellFoundedWellFounded r ↔ WellFounded s :=
  Iff.intro
    (RelHomClass.wellFounded (⟨surjInv hf,
      fun h => by simpa only [o, surjInv_eq hf] using h⟩ : s →r r))
    (RelHomClass.wellFounded (⟨f, o.1⟩ : r →r s))

Well-foundedness Equivalence under Surjective Relation-Preserving Maps

Informal description

Let $f \colon \alpha \to \beta$ be a surjective function between two types $\alpha$ and $\beta$ equipped with relations $r$ and $s$ respectively. Suppose that for all $a, b \in \alpha$, the relation $r(a, b)$ holds if and only if $s(f(a), f(b))$ holds. Then the relation $r$ is well-founded if and only if the relation $s$ is well-founded.

RelEmbedding structure

{α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends α ↪ β

Full source

/-- A relation embedding with respect to a given pair of relations `r` and `s`
is an embedding `f : α ↪ β` such that `r a b ↔ s (f a) (f b)`. -/
structure RelEmbedding {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends α ↪ β where
  /-- Elements are related iff they are related after apply a `RelEmbedding` -/
  map_rel_iff' : ∀ {a b}, s (toEmbedding a) (toEmbedding b) ↔ r a b

Relation embedding

Informal description

A relation embedding between two types $\alpha$ and $\beta$ with respect to relations $r$ on $\alpha$ and $s$ on $\beta$ is an embedding $f : \alpha \hookrightarrow \beta$ such that for any $a, b \in \alpha$, $r(a, b)$ holds if and only if $s(f(a), f(b))$ holds. In other words, $f$ preserves and reflects the relations $r$ and $s$.

term_↪r_ definition

: Lean.TrailingParserDescr✝

Full source

/-- A relation embedding with respect to a given pair of relations `r` and `s`
is an embedding `f : α ↪ β` such that `r a b ↔ s (f a) (f b)`. -/
infixl:25 " ↪r " => RelEmbedding

Relation embedding

Informal description

Given two types $\alpha$ and $\beta$ with relations $r$ and $s$ respectively, a relation embedding $f : \alpha \hookrightarrow \beta$ is an injective function that preserves the relations in both directions, i.e., $r(a, b)$ holds if and only if $s(f(a), f(b))$ holds for all $a, b \in \alpha$.

Subtype.relEmbedding definition

{X : Type*} (r : X → X → Prop) (p : X → Prop) : (Subtype.val : Subtype p → X) ⁻¹'o r ↪r r

Full source

/-- The induced relation on a subtype is an embedding under the natural inclusion. -/
def Subtype.relEmbedding {X : Type*} (r : X → X → Prop) (p : X → Prop) :
    (Subtype.val : Subtype p → X) ⁻¹'o r(Subtype.val : Subtype p → X) ⁻¹'o r ↪r r :=
  ⟨Embedding.subtype p, Iff.rfl⟩

Subtype relation embedding via natural inclusion

Informal description

For a type $X$ with a relation $r$ and a predicate $p$ on $X$, the natural inclusion map from the subtype $\{x \in X \mid p(x)\}$ to $X$ is a relation embedding between the induced relation $(\text{Subtype.val})^{-1}o r$ on the subtype and the original relation $r$ on $X$. Here, $(\text{Subtype.val})^{-1}o r$ is defined by $(\text{Subtype.val})^{-1}o r(a, b) \leftrightarrow r(a, b)$ for $a, b$ in the subtype.

preimage_equivalence theorem

{α β} (f : α → β) {s : β → β → Prop} (hs : Equivalence s) : Equivalence (f ⁻¹'o s)

Full source

theorem preimage_equivalence {α β} (f : α → β) {s : β → β → Prop} (hs : Equivalence s) :
    Equivalence (f ⁻¹'o s) :=
  ⟨fun _ => hs.1 _, fun h => hs.2 h, fun h₁ h₂ => hs.3 h₁ h₂⟩

Pullback of an Equivalence Relation is an Equivalence Relation

Informal description

Let $f : \alpha \to \beta$ be a function between types $\alpha$ and $\beta$, and let $s$ be an equivalence relation on $\beta$. Then the pullback relation $f^{-1}o s$ defined by $(f^{-1}o s)(x, y) \Leftrightarrow s(f(x), f(y))$ is an equivalence relation on $\alpha$.

RelEmbedding.toRelHom definition

(f : r ↪r s) : r →r s

Full source

/-- A relation embedding is also a relation homomorphism -/
def toRelHom (f : r ↪r s) : r →r s where
  toFun := f.toEmbedding.toFun
  map_rel' := (map_rel_iff' f).mpr

Relation embedding as relation homomorphism

Informal description

Given a relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the function $f$ can be viewed as a relation homomorphism from $r$ to $s$. This means that for any $a, b \in \alpha$, if $r(a, b)$ holds, then $s(f(a), f(b))$ also holds.

RelEmbedding.instCoeRelHom instance

: Coe (r ↪r s) (r →r s)

Full source

instance : Coe (r ↪r s) (r →r s) :=
  ⟨toRelHom⟩

Relation Embeddings as Relation Homomorphisms

Informal description

Every relation embedding $f : r \hookrightarrow s$ can be coerced to a relation homomorphism $f : r \to s$.

RelEmbedding.instFunLike instance

: FunLike (r ↪r s) α β

Full source

instance : FunLike (r ↪r s) α β where
  coe x := x.toFun
  coe_injective' f g h := by
    rcases f with ⟨⟨⟩⟩
    rcases g with ⟨⟨⟩⟩
    congr

Function-Like Structure for Relation Embeddings

Informal description

For any relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the type of such embeddings $(r \hookrightarrow s)$ is equipped with a function-like structure, meaning it can be coerced to a function from $\alpha$ to $\beta$ in an injective way.

RelEmbedding.instRelHomClass instance

: RelHomClass (r ↪r s) r s

Full source

instance : RelHomClass (r ↪r s) r s where
  map_rel f _ _ := Iff.mpr (map_rel_iff' f)

Relation Embeddings as Relation Homomorphism Class

Informal description

For any relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the type of such embeddings $(r \hookrightarrow s)$ forms a class of relation homomorphisms that preserve the relations $r$ and $s$. This means that for any $a, b \in \alpha$, if $r(a, b)$ holds, then $s(f(a), f(b))$ must also hold.

RelEmbedding.instEmbeddingLike instance

: EmbeddingLike (r ↪r s) α β

Full source

instance : EmbeddingLike (r ↪r s) α β where
  injective' f := f.inj'

Embedding-like Structure for Relation Embeddings

Informal description

For any relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the type of such embeddings $(r \hookrightarrow s)$ is equipped with an embedding-like structure, meaning it can be coerced to an injective function from $\alpha$ to $\beta$.

RelEmbedding.coe_toEmbedding theorem

{f : r ↪r s} : ((f : r ↪r s).toEmbedding : α → β) = f

Full source

@[simp]
theorem coe_toEmbedding {f : r ↪r s} : ((f : r ↪r s).toEmbedding : α → β) = f :=
  rfl

Embedding Component of Relation Embedding Coerces to Original Function

Informal description

For any relation embedding $f : r \hookrightarrow s$, the underlying function of the embedding (obtained by coercing $f$ to its embedding component) is equal to $f$ itself when viewed as a function from $\alpha$ to $\beta$.

RelEmbedding.coe_toRelHom theorem

{f : r ↪r s} : ((f : r ↪r s).toRelHom : α → β) = f

Full source

@[simp]
theorem coe_toRelHom {f : r ↪r s} : ((f : r ↪r s).toRelHom : α → β) = f :=
  rfl

Relation Homomorphism Component of Relation Embedding Coerces to Original Function

Informal description

For any relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the underlying function of the relation homomorphism obtained from $f$ is equal to $f$ itself when viewed as a function from $\alpha$ to $\beta$.

RelEmbedding.toEmbedding_injective theorem

: Injective (toEmbedding : r ↪r s → (α ↪ β))

Full source

theorem toEmbedding_injective : Injective (toEmbedding : r ↪r s → (α ↪ β)) := by
  rintro ⟨f, -⟩ ⟨g, -⟩; simp

Injectivity of the Underlying Embedding Map for Relation Embeddings

Informal description

The function that maps a relation embedding $f : r \hookrightarrow s$ to its underlying embedding $f : \alpha \hookrightarrow \beta$ is injective. In other words, if two relation embeddings have the same underlying embedding, then they must be equal.

RelEmbedding.toEmbedding_inj theorem

{f g : r ↪r s} : f.toEmbedding = g.toEmbedding ↔ f = g

Full source

@[simp]
theorem toEmbedding_inj {f g : r ↪r s} : f.toEmbedding = g.toEmbedding ↔ f = g :=
  toEmbedding_injective.eq_iff

Equality of Relation Embeddings via Underlying Embeddings

Informal description

For any two relation embeddings $f, g : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the underlying embeddings $f$ and $g$ are equal if and only if $f$ and $g$ are equal as relation embeddings.

RelEmbedding.injective theorem

(f : r ↪r s) : Injective f

Full source

theorem injective (f : r ↪r s) : Injective f :=
  f.inj'

Injectivity of Relation Embeddings

Informal description

For any relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the function $f$ is injective.

RelEmbedding.inj theorem

(f : r ↪r s) {a b} : f a = f b ↔ a = b

Full source

theorem inj (f : r ↪r s) {a b} : f a = f b ↔ a = b := f.injective.eq_iff

Relation Embedding Preserves Equality

Informal description

For any relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $a, b \in \alpha$, we have $f(a) = f(b)$ if and only if $a = b$.

RelEmbedding.map_rel_iff theorem

(f : r ↪r s) {a b} : s (f a) (f b) ↔ r a b

Full source

theorem map_rel_iff (f : r ↪r s) {a b} : s (f a) (f b) ↔ r a b :=
  f.map_rel_iff'

Relation Embedding Preserves and Reflects Relations

Informal description

For any relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $a, b \in \alpha$, we have $s(f(a), f(b))$ if and only if $r(a, b)$.

RelEmbedding.coe_mk theorem

{f} {h} : ⇑(⟨f, h⟩ : r ↪r s) = f

Full source

@[simp]
theorem coe_mk {f} {h} : ⇑(⟨f, h⟩ : r ↪r s) = f :=
  rfl

Coefficient Function of Relation Embedding Constructor Equals Input Function

Informal description

For any function $f : \alpha \to \beta$ and proof $h$ that $f$ is a relation embedding between relations $r$ on $\alpha$ and $s$ on $\beta$, the underlying function of the constructed relation embedding $\langle f, h \rangle$ is equal to $f$.

RelEmbedding.coe_fn_injective theorem

: Injective fun f : r ↪r s => (f : α → β)

Full source

/-- The map `coe_fn : (r ↪r s) → (α → β)` is injective. -/
theorem coe_fn_injective : Injective fun f : r ↪r s => (f : α → β) :=
  DFunLike.coe_injective

Injectivity of the Underlying Function Map for Relation Embeddings

Informal description

The function that maps a relation embedding $f : r \hookrightarrow s$ to its underlying function $f : \alpha \to \beta$ is injective. That is, if two relation embeddings $f, g : r \hookrightarrow s$ satisfy $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.

RelEmbedding.ext theorem

⦃f g : r ↪r s⦄ (h : ∀ x, f x = g x) : f = g

Full source

@[ext]
theorem ext ⦃f g : r ↪r s⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

Extensionality of Relation Embeddings

Informal description

For any two relation embeddings $f, g : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.

RelEmbedding.refl definition

(r : α → α → Prop) : r ↪r r

Full source

/-- Identity map is a relation embedding. -/
@[refl, simps!]
protected def refl (r : α → α → Prop) : r ↪r r :=
  ⟨Embedding.refl _, Iff.rfl⟩

Identity relation embedding

Informal description

The identity function is a relation embedding from a relation $r$ on a type $\alpha$ to itself, meaning that for any $a, b \in \alpha$, $r(a, b)$ holds if and only if $r(\text{id}(a), \text{id}(b))$ holds.

RelEmbedding.trans definition

(f : r ↪r s) (g : s ↪r t) : r ↪r t

Full source

/-- Composition of two relation embeddings is a relation embedding. -/
protected def trans (f : r ↪r s) (g : s ↪r t) : r ↪r t :=
  ⟨f.1.trans g.1, by simp [f.map_rel_iff, g.map_rel_iff]⟩

Composition of relation embeddings

Informal description

Given relation embeddings $f : r \hookrightarrow s$ and $g : s \hookrightarrow t$, their composition $g \circ f$ is a relation embedding from $r$ to $t$. This means that for any $a, b \in \alpha$, $r(a, b)$ holds if and only if $t(g(f(a)), g(f(b)))$ holds.

RelEmbedding.instInhabited instance

(r : α → α → Prop) : Inhabited (r ↪r r)

Full source

instance (r : α → α → Prop) : Inhabited (r ↪r r) :=
  ⟨RelEmbedding.refl _⟩

Existence of Identity Relation Embedding

Informal description

For any relation $r$ on a type $\alpha$, there exists a relation embedding from $r$ to itself, namely the identity embedding.

RelEmbedding.trans_apply theorem

(f : r ↪r s) (g : s ↪r t) (a : α) : (f.trans g) a = g (f a)

Full source

theorem trans_apply (f : r ↪r s) (g : s ↪r t) (a : α) : (f.trans g) a = g (f a) :=
  rfl

Function Application of Composed Relation Embeddings

Informal description

For any relation embeddings $f \colon r \hookrightarrow s$ and $g \colon s \hookrightarrow t$, and for any element $a \in \alpha$, the application of the composed embedding $f \circ g$ to $a$ is equal to $g(f(a))$.

RelEmbedding.coe_trans theorem

(f : r ↪r s) (g : s ↪r t) : (f.trans g) = g ∘ f

Full source

@[simp]
theorem coe_trans (f : r ↪r s) (g : s ↪r t) : (f.trans g) = g ∘ f :=
  rfl

Composition of Relation Embeddings Preserves Function Application

Informal description

For any relation embeddings $f : r \hookrightarrow s$ and $g : s \hookrightarrow t$, the underlying function of their composition $f \circ g$ is equal to the composition of their underlying functions, i.e., $(f \circ g)(x) = g(f(x))$ for all $x \in \alpha$.

RelEmbedding.swap definition

(f : r ↪r s) : swap r ↪r swap s

Full source

/-- A relation embedding is also a relation embedding between dual relations. -/
protected def swap (f : r ↪r s) : swapswap r ↪r swap s :=
  ⟨f.toEmbedding, f.map_rel_iff⟩

Relation embedding between swapped relations

Informal description

Given a relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the same function $f$ also serves as a relation embedding between the swapped relations $\text{swap } r$ on $\alpha$ and $\text{swap } s$ on $\beta$, where $\text{swap } r(a,b) = r(b,a)$ and similarly for $s$.

RelEmbedding.preimage definition

(f : α ↪ β) (s : β → β → Prop) : f ⁻¹'o s ↪r s

Full source

/-- If `f` is injective, then it is a relation embedding from the
  preimage relation of `s` to `s`. -/
def preimage (f : α ↪ β) (s : β → β → Prop) : f ⁻¹'o sf ⁻¹'o s ↪r s :=
  ⟨f, Iff.rfl⟩

Preimage relation embedding

Informal description

Given an injective function $f : \alpha \hookrightarrow \beta$ and a relation $s$ on $\beta$, the function $f$ induces a relation embedding from the preimage relation $f^{-1}o s$ (defined by $a \mapsto b$ if and only if $s(f(a), f(b))$ holds) to the relation $s$ itself.

RelEmbedding.isIrrefl theorem

(f : r ↪r s) [IsIrrefl β s] : IsIrrefl α r

Full source

protected theorem isIrrefl (f : r ↪r s) [IsIrrefl β s] : IsIrrefl α r :=
  ⟨fun a => mt f.map_rel_iff.2 (irrefl (f a))⟩

Irreflexivity Preservation under Relation Embedding

Informal description

Given a relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, if the relation $s$ is irreflexive (i.e., for all $b \in \beta$, $\neg s(b, b)$), then the relation $r$ is also irreflexive (i.e., for all $a \in \alpha$, $\neg r(a, a)$).

RelEmbedding.isRefl theorem

(f : r ↪r s) [IsRefl β s] : IsRefl α r

Full source

protected theorem isRefl (f : r ↪r s) [IsRefl β s] : IsRefl α r :=
  ⟨fun _ => f.map_rel_iff.1 <| refl _⟩

Reflexivity Preservation under Relation Embedding

Informal description

Let $r$ be a relation on a type $\alpha$ and $s$ a relation on a type $\beta$. If there exists a relation embedding $f : r \hookrightarrow s$ (i.e., $f$ preserves and reflects the relations), and if $s$ is reflexive, then $r$ is also reflexive.

RelEmbedding.isSymm theorem

(f : r ↪r s) [IsSymm β s] : IsSymm α r

Full source

protected theorem isSymm (f : r ↪r s) [IsSymm β s] : IsSymm α r :=
  ⟨fun _ _ => imp_imp_imp f.map_rel_iff.2 f.map_rel_iff.1 symm⟩

Symmetry Preservation under Relation Embedding

Informal description

Let $r$ be a relation on a type $\alpha$ and $s$ a relation on a type $\beta$. If there exists a relation embedding $f : r \hookrightarrow s$ (i.e., $f$ preserves and reflects the relations), and if $s$ is symmetric, then $r$ is also symmetric.

RelEmbedding.isAsymm theorem

(f : r ↪r s) [IsAsymm β s] : IsAsymm α r

Full source

protected theorem isAsymm (f : r ↪r s) [IsAsymm β s] : IsAsymm α r :=
  ⟨fun _ _ h₁ h₂ => asymm (f.map_rel_iff.2 h₁) (f.map_rel_iff.2 h₂)⟩

Asymmetry Preservation under Relation Embedding

Informal description

Let $r$ be a relation on a type $\alpha$ and $s$ a relation on a type $\beta$. If there exists a relation embedding $f : r \hookrightarrow s$ (i.e., $f$ preserves and reflects the relations), and if $s$ is asymmetric, then $r$ is also asymmetric.

RelEmbedding.isAntisymm theorem

: ∀ (_ : r ↪r s) [IsAntisymm β s], IsAntisymm α r

Full source

protected theorem isAntisymm : ∀ (_ : r ↪r s) [IsAntisymm β s], IsAntisymm α r
  | ⟨f, o⟩, ⟨H⟩ => ⟨fun _ _ h₁ h₂ => f.inj' (H _ _ (o.2 h₁) (o.2 h₂))⟩

Relation Embedding Preserves Antisymmetry

Informal description

Let $r$ be a relation on a type $\alpha$ and $s$ a relation on a type $\beta$. If there exists a relation embedding $f : r \hookrightarrow s$ (i.e., $f$ preserves and reflects the relations), and if $s$ is antisymmetric, then $r$ is also antisymmetric.

RelEmbedding.isTrans theorem

: ∀ (_ : r ↪r s) [IsTrans β s], IsTrans α r

Full source

protected theorem isTrans : ∀ (_ : r ↪r s) [IsTrans β s], IsTrans α r
  | ⟨_, o⟩, ⟨H⟩ => ⟨fun _ _ _ h₁ h₂ => o.1 (H _ _ _ (o.2 h₁) (o.2 h₂))⟩

Transitivity Preservation under Relation Embedding

Informal description

Let $r$ be a relation on a type $\alpha$ and $s$ a relation on a type $\beta$. If there exists a relation embedding $f : r \hookrightarrow s$ (i.e., $f$ preserves and reflects the relations), and if $s$ is transitive, then $r$ is also transitive.

RelEmbedding.isTotal theorem

: ∀ (_ : r ↪r s) [IsTotal β s], IsTotal α r

Full source

protected theorem isTotal : ∀ (_ : r ↪r s) [IsTotal β s], IsTotal α r
  | ⟨_, o⟩, ⟨H⟩ => ⟨fun _ _ => (or_congr o o).1 (H _ _)⟩

Relation Embedding Preserves Totality

Informal description

For any relation embedding $f : (\alpha, r) \hookrightarrow (\beta, s)$, if the relation $s$ on $\beta$ is total, then the relation $r$ on $\alpha$ is also total. Here, a relation is called total if for any two elements, either $r(a,b)$ or $r(b,a)$ holds.

RelEmbedding.isPreorder theorem

: ∀ (_ : r ↪r s) [IsPreorder β s], IsPreorder α r

Full source

protected theorem isPreorder : ∀ (_ : r ↪r s) [IsPreorder β s], IsPreorder α r
  | f, _ => { f.isRefl, f.isTrans with }

Preorder Preservation under Relation Embedding

Informal description

Let $r$ be a relation on a type $\alpha$ and $s$ a relation on a type $\beta$. If there exists a relation embedding $f : r \hookrightarrow s$ (i.e., $f$ preserves and reflects the relations), and if $s$ is a preorder (i.e., reflexive and transitive), then $r$ is also a preorder.

RelEmbedding.isPartialOrder theorem

: ∀ (_ : r ↪r s) [IsPartialOrder β s], IsPartialOrder α r

Full source

protected theorem isPartialOrder : ∀ (_ : r ↪r s) [IsPartialOrder β s], IsPartialOrder α r
  | f, _ => { f.isPreorder, f.isAntisymm with }

Relation Embedding Preserves Partial Order

Informal description

Let $r$ be a relation on a type $\alpha$ and $s$ a relation on a type $\beta$. If there exists a relation embedding $f : r \hookrightarrow s$ (i.e., $f$ preserves and reflects the relations), and if $s$ is a partial order (i.e., reflexive, antisymmetric, and transitive), then $r$ is also a partial order.

RelEmbedding.isLinearOrder theorem

: ∀ (_ : r ↪r s) [IsLinearOrder β s], IsLinearOrder α r

Full source

protected theorem isLinearOrder : ∀ (_ : r ↪r s) [IsLinearOrder β s], IsLinearOrder α r
  | f, _ => { f.isPartialOrder, f.isTotal with }

Relation Embedding Preserves Linear Order

Informal description

For any relation embedding $f : (\alpha, r) \hookrightarrow (\beta, s)$, if the relation $s$ on $\beta$ is a linear order (i.e., it is reflexive, transitive, antisymmetric, and total), then the relation $r$ on $\alpha$ is also a linear order.

RelEmbedding.isStrictOrder theorem

: ∀ (_ : r ↪r s) [IsStrictOrder β s], IsStrictOrder α r

Full source

protected theorem isStrictOrder : ∀ (_ : r ↪r s) [IsStrictOrder β s], IsStrictOrder α r
  | f, _ => { f.isIrrefl, f.isTrans with }

Relation Embedding Preserves Strict Order

Informal description

For any relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, if $s$ is a strict order on $\beta$, then $r$ is a strict order on $\alpha$.

RelEmbedding.isTrichotomous theorem

: ∀ (_ : r ↪r s) [IsTrichotomous β s], IsTrichotomous α r

Full source

protected theorem isTrichotomous : ∀ (_ : r ↪r s) [IsTrichotomous β s], IsTrichotomous α r
  | ⟨f, o⟩, ⟨H⟩ => ⟨fun _ _ => (or_congr o (or_congr f.inj'.eq_iff o)).1 (H _ _)⟩

Relation Embedding Preserves Trichotomy

Informal description

For any relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, if $s$ is a trichotomous relation on $\beta$, then $r$ is a trichotomous relation on $\alpha$. That is, for any $a, b \in \alpha$, exactly one of $r(a, b)$, $a = b$, or $r(b, a)$ holds.

RelEmbedding.isStrictTotalOrder theorem

: ∀ (_ : r ↪r s) [IsStrictTotalOrder β s], IsStrictTotalOrder α r

Full source

protected theorem isStrictTotalOrder : ∀ (_ : r ↪r s) [IsStrictTotalOrder β s],
    IsStrictTotalOrder α r
  | f, _ => { f.isTrichotomous, f.isStrictOrder with }

Relation Embedding Preserves Strict Total Order

Informal description

For any relation embedding $f \colon r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, if $s$ is a strict total order on $\beta$, then $r$ is a strict total order on $\alpha$.

RelEmbedding.acc theorem

(f : r ↪r s) (a : α) : Acc s (f a) → Acc r a

Full source

protected theorem acc (f : r ↪r s) (a : α) : Acc s (f a) → Acc r a := by
  generalize h : f a = b
  intro ac
  induction ac generalizing a with | intro _ H IH => ?_
  subst h
  exact ⟨_, fun a' h => IH (f a') (f.map_rel_iff.2 h) _ rfl⟩

Relation Embedding Preserves Accessibility

Informal description

For any relation embedding $f \colon r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any element $a \in \alpha$, if the image $f(a)$ is accessible with respect to the relation $s$, then $a$ is accessible with respect to the relation $r$. Here, an element $x$ is called *accessible* with respect to a relation $R$ if every descending $R$-chain starting from $x$ is finite.

RelEmbedding.wellFounded theorem

: ∀ (_ : r ↪r s) (_ : WellFounded s), WellFounded r

Full source

protected theorem wellFounded : ∀ (_ : r ↪r s) (_ : WellFounded s), WellFounded r
  | f, ⟨H⟩ => ⟨fun _ => f.acc _ (H _)⟩

Well-Foundedness Preservation under Relation Embeddings

Informal description

For any relation embedding $f \colon r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, if the relation $s$ is well-founded, then the relation $r$ is also well-founded. Here, a relation $R$ on a type is called *well-founded* if every non-empty subset of the type has a minimal element with respect to $R$.

RelEmbedding.isWellFounded theorem

(f : r ↪r s) [IsWellFounded β s] : IsWellFounded α r

Full source

protected theorem isWellFounded (f : r ↪r s) [IsWellFounded β s] : IsWellFounded α r :=
  ⟨f.wellFounded IsWellFounded.wf⟩

Well-Foundedness Preservation under Relation Embeddings

Informal description

Given a relation embedding $f \colon r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, if $\beta$ is well-founded with respect to $s$, then $\alpha$ is well-founded with respect to $r$. Here, a type is called *well-founded* with respect to a relation if every non-empty subset has a minimal element with respect to that relation.

RelEmbedding.isWellOrder theorem

: ∀ (_ : r ↪r s) [IsWellOrder β s], IsWellOrder α r

Full source

protected theorem isWellOrder : ∀ (_ : r ↪r s) [IsWellOrder β s], IsWellOrder α r
  | f, H => { f.isStrictTotalOrder with wf := f.wellFounded H.wf }

Well-Order Preservation under Relation Embeddings

Informal description

For any relation embedding $f \colon r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, if $s$ is a well-order on $\beta$, then $r$ is a well-order on $\alpha$. Here, a relation $R$ on a type is called a *well-order* if it is a strict total order and every non-empty subset has a minimal element with respect to $R$.

Subtype.wellFoundedLT instance

[LT α] [WellFoundedLT α] (p : α → Prop) : WellFoundedLT (Subtype p)

Full source

instance Subtype.wellFoundedLT [LT α] [WellFoundedLT α] (p : α → Prop) :
    WellFoundedLT (Subtype p) :=
  (Subtype.relEmbedding (· < ·) p).isWellFounded

Well-Founded Order on Subtypes

Informal description

For any type $\alpha$ with a strict order relation $<$ that is well-founded, and any predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ also has a well-founded strict order relation inherited from $\alpha$.

Subtype.wellFoundedGT instance

[LT α] [WellFoundedGT α] (p : α → Prop) : WellFoundedGT (Subtype p)

Full source

instance Subtype.wellFoundedGT [LT α] [WellFoundedGT α] (p : α → Prop) :
    WellFoundedGT (Subtype p) :=
  (Subtype.relEmbedding (· > ·) p).isWellFounded

Well-Foundedness of Greater-Than Relation on Subtypes

Informal description

For any type $\alpha$ with a strict order relation `<$, if $\alpha$ is well-founded with respect to the greater-than relation (i.e., the reverse of $<$), then for any predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ is also well-founded with respect to the greater-than relation.

Quotient.mkRelHom definition

 {_ : Setoid α} {r : α → α → Prop} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) :
  r →r Quotient.lift₂ r H

Full source

/-- `Quotient.mk` as a relation homomorphism between the relation and the lift of a relation. -/
@[simps]
def Quotient.mkRelHom {_ : Setoid α} {r : α → α → Prop}
    (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) : r →r Quotient.lift₂ r H :=
  ⟨Quotient.mk _, id⟩

Quotient map as a relation homomorphism

Informal description

Given a setoid $\alpha$ (a type equipped with an equivalence relation $\approx$) and a relation $r : \alpha \to \alpha \to \text{Prop}$, the function $\text{Quotient.mk}$ (which maps an element of $\alpha$ to its equivalence class) is a relation homomorphism from $r$ to the lifted relation $\text{Quotient.lift₂ } r H$ on the quotient type, provided that $H$ ensures $r$ respects the equivalence relation $\approx$. Here, $H$ is the proof that for any $a_1, b_1, a_2, b_2 \in \alpha$, if $a_1 \approx a_2$ and $b_1 \approx b_2$, then $r a_1 b_1 = r a_2 b_2$.

Quotient.outRelEmbedding definition

 {_ : Setoid α} {r : α → α → Prop} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) :
  Quotient.lift₂ r H ↪r r

Full source

/-- `Quotient.out` as a relation embedding between the lift of a relation and the relation. -/
@[simps!]
noncomputable def Quotient.outRelEmbedding {_ : Setoid α} {r : α → α → Prop}
    (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) : Quotient.lift₂Quotient.lift₂ r H ↪r r :=
  ⟨Embedding.quotientOut α, by
    refine @fun x y => Quotient.inductionOn₂ x y fun a b => ?_
    apply iff_iff_eq.2 (H _ _ _ _ _ _) <;> apply Quotient.mk_out⟩

Relation embedding from quotient relation to original relation via representatives

Informal description

Given a setoid $\alpha$ (a type equipped with an equivalence relation $\approx$) and a relation $r : \alpha \to \alpha \to \text{Prop}$, the function $\text{Quotient.out}$ (which maps an equivalence class back to a representative element) forms a relation embedding from the lifted relation $\text{Quotient.lift₂ } r H$ on the quotient type back to the original relation $r$ on $\alpha$. Here, $H$ is the proof that $r$ respects the equivalence relation $\approx$, meaning for any $a_1, b_1, a_2, b_2 \in \alpha$, if $a_1 \approx a_2$ and $b_1 \approx b_2$, then $r a_1 b_1 = r a_2 b_2$.

acc_lift₂_iff theorem

 {_ : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} {a} :
  Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a

Full source

@[simp]
theorem acc_lift₂_iff {_ : Setoid α} {r : α → α → Prop}
    {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} {a} :
    AccAcc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a := by
  constructor
  · exact RelHomClass.acc (Quotient.mkRelHom H) a
  · intro ac
    induction ac with | intro _ _ IH => ?_
    refine ⟨_, fun q h => ?_⟩
    obtain ⟨a', rfl⟩ := q.exists_rep
    exact IH a' h

Accessibility Equivalence for Quotient Relation and Original Relation

Informal description

Let $\alpha$ be a type equipped with an equivalence relation $\approx$ and $r : \alpha \to \alpha \to \text{Prop}$ be a relation such that for any $a_1, b_1, a_2, b_2 \in \alpha$, if $a_1 \approx a_2$ and $b_1 \approx b_2$, then $r a_1 b_1 = r a_2 b_2$. For any $a \in \alpha$, the equivalence class $\llbracket a \rrbracket$ is accessible with respect to the lifted relation $\text{Quotient.lift₂ } r H$ if and only if $a$ is accessible with respect to the original relation $r$.

acc_liftOn₂'_iff theorem

 {s : Setoid α} {r : α → α → Prop} {H} {a} :
  Acc (fun x y => Quotient.liftOn₂' x y r H) (Quotient.mk'' a : Quotient s) ↔ Acc r a

Full source

@[simp]
theorem acc_liftOn₂'_iff {s : Setoid α} {r : α → α → Prop} {H} {a} :
    AccAcc (fun x y => Quotient.liftOn₂' x y r H) (Quotient.mk'' a : Quotient s) ↔ Acc r a :=
  acc_lift₂_iff (H := H)

Accessibility Equivalence for Quotient Relation via $\text{liftOn₂}'$ and Original Relation

Informal description

Let $\alpha$ be a type equipped with a setoid (an equivalence relation $\approx$) and let $r : \alpha \to \alpha \to \text{Prop}$ be a relation. For any $a \in \alpha$, the equivalence class $\llbracket a \rrbracket$ is accessible with respect to the relation $\text{liftOn₂}'$ (defined by lifting $r$ to the quotient via $H$) if and only if $a$ is accessible with respect to the original relation $r$.

wellFounded_lift₂_iff theorem

 {_ : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} :
  WellFounded (Quotient.lift₂ r H) ↔ WellFounded r

Full source

/-- A relation is well founded iff its lift to a quotient is. -/
@[simp]
theorem wellFounded_lift₂_iff {_ : Setoid α} {r : α → α → Prop}
    {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} :
    WellFoundedWellFounded (Quotient.lift₂ r H) ↔ WellFounded r := by
  constructor
  · exact RelHomClass.wellFounded (Quotient.mkRelHom H)
  · refine fun wf => ⟨fun q => ?_⟩
    obtain ⟨a, rfl⟩ := q.exists_rep
    exact acc_lift₂_iff.2 (wf.apply a)

Well-foundedness Equivalence for Quotient Relation and Original Relation

Informal description

Let $\alpha$ be a type equipped with an equivalence relation $\approx$ and $r : \alpha \to \alpha \to \text{Prop}$ be a relation such that for any $a_1, b_1, a_2, b_2 \in \alpha$, if $a_1 \approx a_2$ and $b_1 \approx b_2$, then $r a_1 b_1 = r a_2 b_2$. Then the lifted relation $\text{Quotient.lift₂ } r H$ on the quotient type is well-founded if and only if the original relation $r$ on $\alpha$ is well-founded.

wellFounded_liftOn₂'_iff theorem

 {s : Setoid α} {r : α → α → Prop} {H} : (WellFounded fun x y : Quotient s => Quotient.liftOn₂' x y r H) ↔ WellFounded r

Full source

@[simp]
theorem wellFounded_liftOn₂'_iff {s : Setoid α} {r : α → α → Prop} {H} :
    (WellFounded fun x y : Quotient s => Quotient.liftOn₂' x y r H) ↔ WellFounded r :=
  wellFounded_lift₂_iff (H := H)

Well-foundedness Equivalence for Quotient Relation via $\text{liftOn₂}'$ and Original Relation

Informal description

Let $\alpha$ be a type equipped with a setoid (an equivalence relation $\approx$) and let $r : \alpha \to \alpha \to \text{Prop}$ be a relation. The relation defined by $\text{liftOn₂}'$ on the quotient type $\text{Quotient } s$ (where $\text{liftOn₂}'$ lifts $r$ to the quotient via $H$) is well-founded if and only if the original relation $r$ on $\alpha$ is well-founded.

RelEmbedding.ofMapRelIff definition

(f : α → β) [IsAntisymm α r] [IsRefl β s] (hf : ∀ a b, s (f a) (f b) ↔ r a b) : r ↪r s

Full source

/-- To define a relation embedding from an antisymmetric relation `r` to a reflexive relation `s`
it suffices to give a function together with a proof that it satisfies `s (f a) (f b) ↔ r a b`.
-/
def ofMapRelIff (f : α → β) [IsAntisymm α r] [IsRefl β s] (hf : ∀ a b, s (f a) (f b) ↔ r a b) :
    r ↪r s where
  toFun := f
  inj' _ _ h := antisymm ((hf _ _).1 (h ▸ refl _)) ((hf _ _).1 (h ▸ refl _))
  map_rel_iff' := hf _ _

Relation embedding from a function preserving relation iff condition

Informal description

Given a function $f : \alpha \to \beta$ between types $\alpha$ and $\beta$ with relations $r$ and $s$ respectively, if $r$ is antisymmetric on $\alpha$ and $s$ is reflexive on $\beta$, and $f$ satisfies the condition that $s(f(a), f(b)) \leftrightarrow r(a, b)$ for all $a, b \in \alpha$, then $f$ can be promoted to a relation embedding from $r$ to $s$.

RelEmbedding.ofMapRelIff_coe theorem

 (f : α → β) [IsAntisymm α r] [IsRefl β s] (hf : ∀ a b, s (f a) (f b) ↔ r a b) : (ofMapRelIff f hf : r ↪r s) = f

Full source

@[simp]
theorem ofMapRelIff_coe (f : α → β) [IsAntisymm α r] [IsRefl β s]
    (hf : ∀ a b, s (f a) (f b) ↔ r a b) :
    (ofMapRelIff f hf : r ↪r s) = f :=
  rfl

Relation Embedding Construction from Function Preserving Relation IFF Condition Yields Original Function

Informal description

Given a function $f : \alpha \to \beta$ between types $\alpha$ and $\beta$ with relations $r$ and $s$ respectively, where $r$ is antisymmetric on $\alpha$ and $s$ is reflexive on $\beta$, and $f$ satisfies the condition that $s(f(a), f(b)) \leftrightarrow r(a, b)$ for all $a, b \in \alpha$, then the relation embedding constructed from $f$ via `ofMapRelIff` is equal to $f$ itself when viewed as a function.

RelEmbedding.ofMonotone definition

[IsTrichotomous α r] [IsAsymm β s] (f : α → β) (H : ∀ a b, r a b → s (f a) (f b)) : r ↪r s

Full source

/-- It suffices to prove `f` is monotone between strict relations
  to show it is a relation embedding. -/
def ofMonotone [IsTrichotomous α r] [IsAsymm β s] (f : α → β) (H : ∀ a b, r a b → s (f a) (f b)) :
    r ↪r s := by
  haveI := @IsAsymm.isIrrefl β s _
  refine ⟨⟨f, fun a b e => ?_⟩, @fun a b => ⟨fun h => ?_, H _ _⟩⟩
  · refine ((@trichotomous _ r _ a b).resolve_left ?_).resolve_right ?_
    · exact fun h => irrefl (r := s) (f a) (by simpa [e] using H _ _ h)
    · exact fun h => irrefl (r := s) (f b) (by simpa [e] using H _ _ h)
  · refine (@trichotomous _ r _ a b).resolve_right (Or.rec (fun e => ?_) fun h' => ?_)
    · subst e
      exact irrefl _ h
    · exact asymm (H _ _ h') h

Relation embedding from a monotone function under trichotomy and asymmetry conditions

Informal description

Given a function $f : \alpha \to \beta$ between types $\alpha$ and $\beta$ with relations $r$ and $s$ respectively, if $r$ is trichotomous on $\alpha$ and $s$ is asymmetric on $\beta$, and $f$ is monotone (i.e., $r(a, b) \implies s(f(a), f(b))$ for all $a, b \in \alpha$), then $f$ can be promoted to a relation embedding from $r$ to $s$.

RelEmbedding.ofMonotone_coe theorem

[IsTrichotomous α r] [IsAsymm β s] (f : α → β) (H) : (@ofMonotone _ _ r s _ _ f H : α → β) = f

Full source

@[simp]
theorem ofMonotone_coe [IsTrichotomous α r] [IsAsymm β s] (f : α → β) (H) :
    (@ofMonotone _ _ r s _ _ f H : α → β) = f :=
  rfl

Relation embedding from monotone function coincides with original function

Informal description

Given a function $f : \alpha \to \beta$ between types $\alpha$ and $\beta$ with relations $r$ and $s$ respectively, where $r$ is trichotomous on $\alpha$ and $s$ is asymmetric on $\beta$, and $f$ is monotone (i.e., $r(a, b) \implies s(f(a), f(b))$ for all $a, b \in \alpha$), the relation embedding constructed from $f$ via `ofMonotone` is equal to $f$ itself when viewed as a function.

RelEmbedding.ofIsEmpty definition

(r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] : r ↪r s

Full source

/-- A relation embedding from an empty type. -/
def ofIsEmpty (r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] : r ↪r s :=
  ⟨Embedding.ofIsEmpty, @fun a => isEmptyElim a⟩

Relation embedding from an empty type

Informal description

Given relations $r$ on an empty type $\alpha$ and $s$ on any type $\beta$, there exists a relation embedding from $r$ to $s$. This is constructed using the unique embedding from an empty type and the fact that all statements about elements of $\alpha$ are vacuously true.

RelEmbedding.sumLiftRelInl definition

(r : α → α → Prop) (s : β → β → Prop) : r ↪r Sum.LiftRel r s

Full source

/-- `Sum.inl` as a relation embedding into `Sum.LiftRel r s`. -/
@[simps]
def sumLiftRelInl (r : α → α → Prop) (s : β → β → Prop) : r ↪r Sum.LiftRel r s where
  toFun := Sum.inl
  inj' := Sum.inl_injective
  map_rel_iff' := Sum.liftRel_inl_inl

Left inclusion as a relation embedding into lifted sum relation

Informal description

The left inclusion function $\text{Sum.inl} : \alpha \to \alpha \oplus \beta$ is a relation embedding from the relation $r$ on $\alpha$ to the lifted relation $\text{Sum.LiftRel}\ r\ s$ on $\alpha \oplus \beta$, where $s$ is a relation on $\beta$. This means that for any $a_1, a_2 \in \alpha$, $r(a_1, a_2)$ holds if and only if $\text{Sum.LiftRel}\ r\ s\ (\text{Sum.inl}\ a_1)\ (\text{Sum.inl}\ a_2)$ holds.

RelEmbedding.sumLiftRelInr definition

(r : α → α → Prop) (s : β → β → Prop) : s ↪r Sum.LiftRel r s

Full source

/-- `Sum.inr` as a relation embedding into `Sum.LiftRel r s`. -/
@[simps]
def sumLiftRelInr (r : α → α → Prop) (s : β → β → Prop) : s ↪r Sum.LiftRel r s where
  toFun := Sum.inr
  inj' := Sum.inr_injective
  map_rel_iff' := Sum.liftRel_inr_inr

Right inclusion as a relation embedding into lexicographic sum

Informal description

The right inclusion function $\text{Sum.inr} : \beta \to \alpha \oplus \beta$ is a relation embedding from the relation $s$ on $\beta$ to the lexicographic sum relation $\text{Sum.LiftRel}\ r\ s$ on $\alpha \oplus \beta$, where $r$ is a relation on $\alpha$. This means that for any $b_1, b_2 \in \beta$, $s(b_1, b_2)$ holds if and only if $\text{Sum.LiftRel}\ r\ s\ (\text{Sum.inr}\ b_1)\ (\text{Sum.inr}\ b_2)$ holds.

RelEmbedding.sumLiftRelMap definition

(f : r ↪r s) (g : t ↪r u) : Sum.LiftRel r t ↪r Sum.LiftRel s u

Full source

/-- `Sum.map` as a relation embedding between `Sum.LiftRel` relations. -/
@[simps]
def sumLiftRelMap (f : r ↪r s) (g : t ↪r u) : Sum.LiftRelSum.LiftRel r t ↪r Sum.LiftRel s u where
  toFun := Sum.map f g
  inj' := f.injective.sumMap g.injective
  map_rel_iff' := by rintro (a | b) (c | d) <;> simp [f.map_rel_iff, g.map_rel_iff]

Relation embedding of sum maps under lifted relations

Informal description

Given relation embeddings $f : r \hookrightarrow s$ and $g : t \hookrightarrow u$, the function $\text{Sum.map}\ f\ g$ is a relation embedding from $\text{Sum.LiftRel}\ r\ t$ to $\text{Sum.LiftRel}\ s\ u$. This means that for any $x, y$ in the sum type, the relation $\text{Sum.LiftRel}\ r\ t\ x\ y$ holds if and only if $\text{Sum.LiftRel}\ s\ u\ (\text{Sum.map}\ f\ g\ x)\ (\text{Sum.map}\ f\ g\ y)$ holds.

RelEmbedding.sumLexInl definition

(r : α → α → Prop) (s : β → β → Prop) : r ↪r Sum.Lex r s

Full source

/-- `Sum.inl` as a relation embedding into `Sum.Lex r s`. -/
@[simps]
def sumLexInl (r : α → α → Prop) (s : β → β → Prop) : r ↪r Sum.Lex r s where
  toFun := Sum.inl
  inj' := Sum.inl_injective
  map_rel_iff' := Sum.lex_inl_inl

Left inclusion as a relation embedding into lexicographic sum

Informal description

The left inclusion function $\text{Sum.inl} : \alpha \to \alpha \oplus \beta$ is a relation embedding from the relation $r$ on $\alpha$ to the lexicographic sum relation $\text{Sum.Lex}\ r\ s$ on $\alpha \oplus \beta$, where $s$ is a relation on $\beta$. This means that for any $a_1, a_2 \in \alpha$, $r(a_1, a_2)$ holds if and only if $\text{Sum.Lex}\ r\ s\ (\text{Sum.inl}\ a_1)\ (\text{Sum.inl}\ a_2)$ holds.

RelEmbedding.sumLexInr definition

(r : α → α → Prop) (s : β → β → Prop) : s ↪r Sum.Lex r s

Full source

/-- `Sum.inr` as a relation embedding into `Sum.Lex r s`. -/
@[simps]
def sumLexInr (r : α → α → Prop) (s : β → β → Prop) : s ↪r Sum.Lex r s where
  toFun := Sum.inr
  inj' := Sum.inr_injective
  map_rel_iff' := Sum.lex_inr_inr

Right inclusion as a relation embedding into lexicographic sum

Informal description

The right inclusion function $\text{Sum.inr} : \beta \to \alpha \oplus \beta$ is a relation embedding from the relation $s$ on $\beta$ to the lexicographic sum relation $\text{Sum.Lex}\ r\ s$ on $\alpha \oplus \beta$, where $r$ is a relation on $\alpha$. This means that for any $b_1, b_2 \in \beta$, $s(b_1, b_2)$ holds if and only if $\text{Sum.Lex}\ r\ s\ (\text{Sum.inr}\ b_1)\ (\text{Sum.inr}\ b_2)$ holds.

RelEmbedding.sumLexMap definition

(f : r ↪r s) (g : t ↪r u) : Sum.Lex r t ↪r Sum.Lex s u

Full source

/-- `Sum.map` as a relation embedding between `Sum.Lex` relations. -/
@[simps]
def sumLexMap (f : r ↪r s) (g : t ↪r u) : Sum.LexSum.Lex r t ↪r Sum.Lex s u where
  toFun := Sum.map f g
  inj' := f.injective.sumMap g.injective
  map_rel_iff' := by rintro (a | b) (c | d) <;> simp [f.map_rel_iff, g.map_rel_iff]

Relation embedding of lexicographic sums under component-wise maps

Informal description

Given relation embeddings $f : r \hookrightarrow s$ and $g : t \hookrightarrow u$, the function $\text{Sum.map} f g$ is a relation embedding from the lexicographic sum of $r$ and $t$ to the lexicographic sum of $s$ and $u$. That is, for any $a, c \in \alpha$ or $b, d \in \beta$, the relation $\text{Sum.Lex} r t (a | b) (c | d)$ holds if and only if $\text{Sum.Lex} s u (f a | g b) (f c | g d)$ holds.

RelEmbedding.prodLexMkLeft definition

(s : β → β → Prop) {a : α} (h : ¬r a a) : s ↪r Prod.Lex r s

Full source

/-- `fun b ↦ Prod.mk a b` as a relation embedding. -/
@[simps]
def prodLexMkLeft (s : β → β → Prop) {a : α} (h : ¬r a a) : s ↪r Prod.Lex r s where
  toFun := Prod.mk a
  inj' := Prod.mk_right_injective a
  map_rel_iff' := by simp [Prod.lex_def, h]

Relation embedding into lexicographic product (left component fixed)

Informal description

Given a relation $s$ on a type $\beta$ and an element $a \in \alpha$ such that $r(a, a)$ does not hold, the function mapping each $b \in \beta$ to $(a, b)$ is a relation embedding from $s$ to the lexicographic order on $\alpha \times \beta$ induced by $r$ and $s$. This means that for any $b_1, b_2 \in \beta$, $s(b_1, b_2)$ holds if and only if the lexicographic order relation holds between $(a, b_1)$ and $(a, b_2)$.

RelEmbedding.prodLexMkRight definition

(r : α → α → Prop) {b : β} (h : ¬s b b) : r ↪r Prod.Lex r s

Full source

/-- `fun a ↦ Prod.mk a b` as a relation embedding. -/
@[simps]
def prodLexMkRight (r : α → α → Prop) {b : β} (h : ¬s b b) : r ↪r Prod.Lex r s where
  toFun a := (a, b)
  inj' := Prod.mk_left_injective b
  map_rel_iff' := by simp [Prod.lex_def, h]

Relation embedding into lexicographic product (right component fixed)

Informal description

Given a relation $r$ on a type $\alpha$ and a relation $s$ on a type $\beta$, and an element $b \in \beta$ such that $s(b, b)$ does not hold, the function mapping each $a \in \alpha$ to $(a, b)$ is a relation embedding from $r$ to the lexicographic order on $\alpha \times \beta$ induced by $r$ and $s$.

RelEmbedding.prodLexMap definition

(f : r ↪r s) (g : t ↪r u) : Prod.Lex r t ↪r Prod.Lex s u

Full source

/-- `Prod.map` as a relation embedding. -/
@[simps]
def prodLexMap (f : r ↪r s) (g : t ↪r u) : Prod.LexProd.Lex r t ↪r Prod.Lex s u where
  toFun := Prod.map f g
  inj' := f.injective.prodMap g.injective
  map_rel_iff' := by simp [Prod.lex_def, f.map_rel_iff, g.map_rel_iff, f.inj]

Relation embedding of lexicographic product maps

Informal description

Given relation embeddings $f : r \hookrightarrow s$ and $g : t \hookrightarrow u$, the product map $\text{Prod.map}\ f\ g$ is a relation embedding from the lexicographic order on $\alpha \times \gamma$ (with relations $r$ and $t$) to the lexicographic order on $\beta \times \delta$ (with relations $s$ and $u$). This means that for any $(a, c)$ and $(b, d)$ in $\alpha \times \gamma$, the lexicographic order relation holds between them if and only if it holds between their images under the product map.

RelIso structure

{α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends α ≃ β

Full source

/-- A relation isomorphism is an equivalence that is also a relation embedding. -/
structure RelIso {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends α ≃ β where
  /-- Elements are related iff they are related after apply a `RelIso` -/
  map_rel_iff' : ∀ {a b}, s (toEquiv a) (toEquiv b) ↔ r a b

Relation Isomorphism

Informal description

A relation isomorphism between two types $\alpha$ and $\beta$ with relations $r$ and $s$ respectively is an equivalence (bijective function) $f : \alpha \to \beta$ that preserves the relations, meaning $r(a, b) \leftrightarrow s(f(a), f(b))$ for all $a, b \in \alpha$.

term_≃r_ definition

: Lean.TrailingParserDescr✝

Full source

/-- A relation isomorphism is an equivalence that is also a relation embedding. -/
infixl:25 " ≃r " => RelIso

Relation isomorphism notation (`≃r`)

Informal description

The notation `≃r` denotes a relation isomorphism, which is an equivalence between types that also preserves the given relations. Specifically, for relations `r : α → α → Prop` and `s : β → β → Prop`, a relation isomorphism `f : r ≃r s` is a bijection `f : α ≃ β` such that for any `a b : α`, `r a b` holds if and only if `s (f a) (f b)` holds.

RelIso.toRelEmbedding definition

(f : r ≃r s) : r ↪r s

Full source

/-- Convert a `RelIso` to a `RelEmbedding`. This function is also available as a coercion
but often it is easier to write `f.toRelEmbedding` than to write explicitly `r` and `s`
in the target type. -/
def toRelEmbedding (f : r ≃r s) : r ↪r s :=
  ⟨f.toEquiv.toEmbedding, f.map_rel_iff'⟩

Relation isomorphism to relation embedding conversion

Informal description

Given a relation isomorphism $f : r \simeqr s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the function converts $f$ into a relation embedding $f : r \hookrightarrow s$ by extracting the underlying embedding from the equivalence and preserving the relation mapping property.

RelIso.toEquiv_injective theorem

: Injective (toEquiv : r ≃r s → α ≃ β)

Full source

theorem toEquiv_injective : Injective (toEquiv : r ≃r s → α ≃ β)
  | ⟨e₁, o₁⟩, ⟨e₂, _⟩, h => by congr

Injectivity of the Equivalence Underlying a Relation Isomorphism

Informal description

The function mapping a relation isomorphism $f : r \simeqr s$ to its underlying equivalence $f : \alpha \simeq \beta$ is injective. In other words, if two relation isomorphisms induce the same equivalence on the underlying types, then they must be the same relation isomorphism.

RelIso.instCoeOutRelEmbedding instance

: CoeOut (r ≃r s) (r ↪r s)

Full source

instance : CoeOut (r ≃r s) (r ↪r s) :=
  ⟨toRelEmbedding⟩

Relation Isomorphism as Relation Embedding

Informal description

Every relation isomorphism $f : r \simeqr s$ can be viewed as a relation embedding $f : r \hookrightarrow s$ by considering the underlying embedding of the equivalence.

RelIso.instFunLike instance

: FunLike (r ≃r s) α β

Full source

instance : FunLike (r ≃r s) α β where
  coe x := x
  coe_injective' := Equiv.coe_fn_injective.comp toEquiv_injective

Function-Like Structure for Relation Isomorphisms

Informal description

For any relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the type of such isomorphisms $(r \simeq s)$ is equipped with a function-like structure, meaning it can be coerced to a function from $\alpha$ to $\beta$ in an injective way.

RelIso.instRelHomClass instance

: RelHomClass (r ≃r s) r s

Full source

instance : RelHomClass (r ≃r s) r s where
  map_rel f _ _ := Iff.mpr (map_rel_iff' f)

Relation Isomorphisms are Relation Homomorphisms

Informal description

Every relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$ is a relation homomorphism, meaning that for any $a, b \in \alpha$, if $r(a, b)$ holds, then $s(f(a), f(b))$ must also hold.

RelIso.instEquivLike instance

: EquivLike (r ≃r s) α β

Full source

instance : EquivLike (r ≃r s) α β where
  coe f := f
  inv f := f.toEquiv.symm
  left_inv f := f.left_inv
  right_inv f := f.right_inv
  coe_injective' _ _ hf _ := DFunLike.ext' hf

Equivalence-like Structure for Relation Isomorphisms

Informal description

For any relations $r$ on $\alpha$ and $s$ on $\beta$, the type of relation isomorphisms $r \simeq s$ (denoted as $r \simeqr s$) is equipped with an equivalence-like structure, meaning it can be injectively coerced to bijections between $\alpha$ and $\beta$.

RelIso.coe_toRelEmbedding theorem

(f : r ≃r s) : (f.toRelEmbedding : α → β) = f

Full source

@[simp]
theorem coe_toRelEmbedding (f : r ≃r s) : (f.toRelEmbedding : α → β) = f :=
  rfl

Relation isomorphism to embedding conversion preserves function

Informal description

For any relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the underlying function of the relation embedding obtained from $f$ is equal to $f$ itself. In other words, if we convert $f$ to a relation embedding and then consider it as a function, we get back the original function $f$.

RelIso.coe_toEmbedding theorem

(f : r ≃r s) : (f.toEmbedding : α → β) = f

Full source

@[simp]
theorem coe_toEmbedding (f : r ≃r s) : (f.toEmbedding : α → β) = f :=
  rfl

Embedding Component of Relation Isomorphism Coincides with Original Function

Informal description

For any relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the underlying function of the embedding obtained from $f$ is equal to $f$ itself. That is, if we extract the embedding component of $f$ and view it as a function, it coincides with $f$.

RelIso.map_rel_iff theorem

(f : r ≃r s) {a b} : s (f a) (f b) ↔ r a b

Full source

theorem map_rel_iff (f : r ≃r s) {a b} : s (f a) (f b) ↔ r a b :=
  f.map_rel_iff'

Relation Preservation under Isomorphism: $s(f(a), f(b)) \leftrightarrow r(a, b)$

Informal description

For any relation isomorphism $f$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $a, b \in \alpha$, we have $s(f(a), f(b))$ if and only if $r(a, b)$.

RelIso.coe_fn_mk theorem

(f : α ≃ β) (o : ∀ ⦃a b⦄, s (f a) (f b) ↔ r a b) : (RelIso.mk f @o : α → β) = f

Full source

@[simp]
theorem coe_fn_mk (f : α ≃ β) (o : ∀ ⦃a b⦄, s (f a) (f b) ↔ r a b) :
    (RelIso.mk f @o : α → β) = f :=
  rfl

Relation Isomorphism Construction Preserves Underlying Function

Informal description

For any equivalence $f : \alpha \simeq \beta$ and proof $o$ that $f$ preserves the relations $r$ and $s$ (i.e., $s(f(a), f(b)) \leftrightarrow r(a, b)$ for all $a, b \in \alpha$), the underlying function of the relation isomorphism constructed from $f$ and $o$ is equal to $f$ itself.

RelIso.coe_fn_toEquiv theorem

(f : r ≃r s) : (f.toEquiv : α → β) = f

Full source

@[simp]
theorem coe_fn_toEquiv (f : r ≃r s) : (f.toEquiv : α → β) = f :=
  rfl

Equivalence Function of Relation Isomorphism Coincides with Itself

Informal description

For any relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the underlying function of the equivalence $f.\text{toEquiv}$ is equal to $f$ itself when viewed as a function from $\alpha$ to $\beta$.

RelIso.coe_fn_injective theorem

: Injective fun f : r ≃r s => (f : α → β)

Full source

/-- The map `DFunLike.coe : (r ≃r s) → (α → β)` is injective. -/
theorem coe_fn_injective : Injective fun f : r ≃r s => (f : α → β) :=
  DFunLike.coe_injective

Injectivity of the Function Representation of Relation Isomorphisms

Informal description

The canonical map from relation isomorphisms $f : r \simeq s$ to functions $\alpha \to \beta$ is injective. That is, if two relation isomorphisms $f, g : r \simeq s$ satisfy $f = g$ as functions, then $f = g$ as relation isomorphisms.

RelIso.ext theorem

⦃f g : r ≃r s⦄ (h : ∀ x, f x = g x) : f = g

Full source

@[ext]
theorem ext ⦃f g : r ≃r s⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

Extensionality for Relation Isomorphisms

Informal description

For any two relation isomorphisms $f, g : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.

RelIso.symm definition

(f : r ≃r s) : s ≃r r

Full source

/-- Inverse map of a relation isomorphism is a relation isomorphism. -/
protected def symm (f : r ≃r s) : s ≃r r :=
  ⟨f.toEquiv.symm, @fun a b => by erw [← f.map_rel_iff, f.1.apply_symm_apply, f.1.apply_symm_apply]⟩

Inverse of a relation isomorphism

Informal description

Given a relation isomorphism $f : r \simeqr s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the inverse map $f^{-1} : \beta \to \alpha$ is also a relation isomorphism from $s$ to $r$.

RelIso.Simps.apply definition

(h : r ≃r s) : α → β

Full source

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
  because `RelIso` defines custom coercions other than the ones given by `DFunLike`. -/
def Simps.apply (h : r ≃r s) : α → β :=
  h

Application of a relation isomorphism

Informal description

The function that applies a relation isomorphism $h : r \simeq s$ to an element of $\alpha$ to obtain an element of $\beta$.

RelIso.Simps.symm_apply definition

(h : r ≃r s) : β → α

Full source

/-- See Note [custom simps projection]. -/
def Simps.symm_apply (h : r ≃r s) : β → α :=
  h.symm

Preimage under relation isomorphism

Informal description

Given a relation isomorphism $h : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the function maps an element $y \in \beta$ to its preimage $x \in \alpha$ under $h$.

RelIso.refl definition

(r : α → α → Prop) : r ≃r r

Full source

/-- Identity map is a relation isomorphism. -/
@[refl, simps! apply]
protected def refl (r : α → α → Prop) : r ≃r r :=
  ⟨Equiv.refl _, Iff.rfl⟩

Identity relation isomorphism

Informal description

The identity map on a type $\alpha$ with a relation $r$ is a relation isomorphism from $r$ to itself. That is, the identity function preserves the relation $r$ in both directions: $r(a, b) \leftrightarrow r(\text{id}(a), \text{id}(b))$ for all $a, b \in \alpha$.

RelIso.trans definition

(f₁ : r ≃r s) (f₂ : s ≃r t) : r ≃r t

Full source

/-- Composition of two relation isomorphisms is a relation isomorphism. -/
@[simps! apply]
protected def trans (f₁ : r ≃r s) (f₂ : s ≃r t) : r ≃r t :=
  ⟨f₁.toEquiv.trans f₂.toEquiv, f₂.map_rel_iff.trans f₁.map_rel_iff⟩

Composition of relation isomorphisms

Informal description

Given two relation isomorphisms $f_1 : r \simeqr s$ and $f_2 : s \simeqr t$, their composition $f_2 \circ f_1$ forms a relation isomorphism between $r$ and $t$. This means that for any $a, b \in \alpha$, the relation $r(a, b)$ holds if and only if $t((f_2 \circ f_1)(a), (f_2 \circ f_1)(b))$ holds.

RelIso.instInhabited instance

(r : α → α → Prop) : Inhabited (r ≃r r)

Full source

instance (r : α → α → Prop) : Inhabited (r ≃r r) :=
  ⟨RelIso.refl _⟩

Existence of Identity Relation Isomorphism

Informal description

For any relation $r$ on a type $\alpha$, there exists a relation isomorphism from $r$ to itself (namely, the identity map).

RelIso.default_def theorem

(r : α → α → Prop) : default = RelIso.refl r

Full source

@[simp]
theorem default_def (r : α → α → Prop) : default = RelIso.refl r :=
  rfl

Default Relation Isomorphism is Identity

Informal description

For any relation $r$ on a type $\alpha$, the default relation isomorphism from $r$ to itself is the identity relation isomorphism.

RelIso.apply_symm_apply theorem

(e : r ≃r s) (x : β) : e (e.symm x) = x

Full source

@[simp] lemma apply_symm_apply (e : r ≃r s) (x : β) : e (e.symm x) = x := e.right_inv x

Relation Isomorphism Preserves Inverse Application: $e(e^{-1}(x)) = x$

Informal description

For any relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any element $x \in \beta$, applying $e$ to the inverse image $e^{-1}(x)$ yields $x$ again, i.e., $e(e^{-1}(x)) = x$.

RelIso.symm_apply_apply theorem

(e : r ≃r s) (x : α) : e.symm (e x) = x

Full source

@[simp] lemma symm_apply_apply (e : r ≃r s) (x : α) : e.symm (e x) = x := e.left_inv x

Inverse Relation Isomorphism Property: $e^{-1}(e(x)) = x$

Informal description

For any relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any element $x \in \alpha$, the inverse map $e^{-1}$ satisfies $e^{-1}(e(x)) = x$.

RelIso.symm_comp_self theorem

(e : r ≃r s) : e.symm ∘ e = id

Full source

@[simp] lemma symm_comp_self (e : r ≃r s) : e.symm ∘ e = id := funext e.symm_apply_apply

Inverse Composition Property of Relation Isomorphism: $e^{-1} \circ e = \text{id}$

Informal description

For any relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the composition of the inverse map $e^{-1}$ with $e$ is equal to the identity function on $\alpha$, i.e., $e^{-1} \circ e = \text{id}$.

RelIso.self_comp_symm theorem

(e : r ≃r s) : e ∘ e.symm = id

Full source

@[simp] lemma self_comp_symm (e : r ≃r s) : e ∘ e.symm = id := funext e.apply_symm_apply

Composition of Relation Isomorphism with Its Inverse Yields Identity: $e \circ e^{-1} = \text{id}$

Informal description

For any relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity function on $\beta$, i.e., $e \circ e^{-1} = \text{id}$.

RelIso.symm_trans_apply theorem

(f : r ≃r s) (g : s ≃r t) (a : γ) : (f.trans g).symm a = f.symm (g.symm a)

Full source

@[simp] lemma symm_trans_apply (f : r ≃r s) (g : s ≃r t) (a : γ) :
    (f.trans g).symm a = f.symm (g.symm a) := rfl

Inverse of Composition of Relation Isomorphisms

Informal description

Let $f : r \simeq s$ and $g : s \simeq t$ be relation isomorphisms between relations $r$ on $\alpha$, $s$ on $\beta$, and $t$ on $\gamma$. Then for any element $a \in \gamma$, the inverse of the composition $f \circ g$ evaluated at $a$ equals the composition of the inverses $f^{-1} \circ g^{-1}$ evaluated at $a$, i.e., $(f \circ g)^{-1}(a) = f^{-1}(g^{-1}(a))$.

RelIso.symm_symm_apply theorem

(f : r ≃r s) (b : α) : f.symm.symm b = f b

Full source

lemma symm_symm_apply (f : r ≃r s) (b : α) : f.symm.symm b = f b := rfl

Double Inverse of Relation Isomorphism Preserves Application: $f^{-1^{-1}}(b) = f(b)$

Informal description

For any relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any element $b \in \alpha$, applying the inverse of the inverse of $f$ to $b$ yields the same result as applying $f$ to $b$, i.e., $f^{-1^{-1}}(b) = f(b)$.

RelIso.apply_eq_iff_eq theorem

(f : r ≃r s) {x y : α} : f x = f y ↔ x = y

Full source

lemma apply_eq_iff_eq (f : r ≃r s) {x y : α} : f x = f y ↔ x = y := EquivLike.apply_eq_iff_eq f

Relation Isomorphism Preserves Equality: $f(x) = f(y) \leftrightarrow x = y$

Informal description

For any relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $x, y \in \alpha$, we have $f(x) = f(y)$ if and only if $x = y$.

RelIso.apply_eq_iff_eq_symm_apply theorem

{x : α} {y : β} (f : r ≃r s) : f x = y ↔ x = f.symm y

Full source

lemma apply_eq_iff_eq_symm_apply {x : α} {y : β} (f : r ≃r s) : f x = y ↔ x = f.symm y := by
  conv_lhs => rw [← apply_symm_apply f y]
  rw [apply_eq_iff_eq]

Relation Isomorphism Characterizes Equality via Inverse: $f(x) = y \leftrightarrow x = f^{-1}(y)$

Informal description

For any relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $x \in \alpha$ and $y \in \beta$, we have $f(x) = y$ if and only if $x = f^{-1}(y)$.

RelIso.symm_apply_eq theorem

(e : r ≃r s) {x y} : e.symm x = y ↔ x = e y

Full source

lemma symm_apply_eq (e : r ≃r s) {x y} : e.symm x = y ↔ x = e y := e.toEquiv.symm_apply_eq

Inverse Relation Isomorphism Characterizes Equality via Symmetric Application

Informal description

For any relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $x \in \beta$ and $y \in \alpha$, the inverse map $e^{-1}$ satisfies $e^{-1}(x) = y$ if and only if $x = e(y)$.

RelIso.symm_symm theorem

(e : r ≃r s) : e.symm.symm = e

Full source

@[simp] lemma symm_symm (e : r ≃r s) : e.symm.symm = e := rfl

Double Inverse of Relation Isomorphism is Identity

Informal description

For any relation isomorphism $e$ between relations $r$ and $s$, the double inverse $e^{-1^{-1}}$ is equal to $e$ itself.

RelIso.symm_bijective theorem

: Bijective (.symm : (r ≃r s) → s ≃r r)

Full source

lemma symm_bijective : Bijective (.symm : (r ≃r s) → s ≃r r) :=
  bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of Relation Isomorphism Inversion

Informal description

The inverse operation on relation isomorphisms is bijective. That is, the map sending a relation isomorphism $f : r \simeqr s$ to its inverse $f^{-1} : s \simeqr r$ is both injective and surjective.

RelIso.refl_symm theorem

: (RelIso.refl r).symm = .refl _

Full source

@[simp] lemma refl_symm : (RelIso.refl r).symm = .refl _ := rfl

Inverse of Identity Relation Isomorphism is Identity

Informal description

The inverse of the identity relation isomorphism on a relation $r$ is equal to the identity relation isomorphism on $r$.

RelIso.trans_refl theorem

(e : r ≃r s) : e.trans (.refl _) = e

Full source

@[simp] lemma trans_refl (e : r ≃r s) : e.trans (.refl _) = e := rfl

Identity Relation Isomorphism is Right Identity for Composition

Informal description

For any relation isomorphism $e$ from $r$ to $s$, the composition of $e$ with the identity relation isomorphism on $s$ equals $e$ itself, i.e., $e \circ \text{id}_s = e$.

RelIso.refl_trans theorem

(e : r ≃r s) : .trans (.refl _) e = e

Full source

@[simp] lemma refl_trans (e : r ≃r s) : .trans (.refl _) e = e := rfl

Identity Relation Isomorphism is Left Identity for Composition

Informal description

For any relation isomorphism $e$ from $r$ to $s$, the composition of the identity relation isomorphism on $r$ with $e$ is equal to $e$ itself. That is, $\text{id}_r \circ e = e$.

RelIso.symm_trans_self theorem

(e : r ≃r s) : e.symm.trans e = .refl _

Full source

@[simp] lemma symm_trans_self (e : r ≃r s) : e.symm.trans e = .refl _ := ext <| by simp

Inverse Composition Yields Identity Relation Isomorphism: $e^{-1} \circ e = \text{id}_s$

Informal description

For any relation isomorphism $e$ from $r$ to $s$, the composition of its inverse $e^{-1}$ with $e$ is equal to the identity relation isomorphism on $s$, i.e., $e^{-1} \circ e = \text{id}_s$.

RelIso.self_trans_symm theorem

(e : r ≃r s) : e.trans e.symm = .refl _

Full source

@[simp] lemma self_trans_symm (e : r ≃r s) : e.trans e.symm = .refl _ := ext <| by simp

Composition of Relation Isomorphism with Its Inverse Yields Identity

Informal description

For any relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity relation isomorphism on $r$. That is, $e \circ e^{-1} = \text{id}_r$.

RelIso.trans_assoc theorem

 {δ : Type*} {u : δ → δ → Prop} (ab : r ≃r s) (bc : s ≃r t) (cd : t ≃r u) :
  (ab.trans bc).trans cd = ab.trans (bc.trans cd)

Full source

lemma trans_assoc {δ : Type*} {u : δ → δ → Prop} (ab : r ≃r s) (bc : s ≃r t) (cd : t ≃r u) :
    (ab.trans bc).trans cd = ab.trans (bc.trans cd) := rfl

Associativity of Relation Isomorphism Composition

Informal description

For any relation isomorphisms $ab : r \simeq s$, $bc : s \simeq t$, and $cd : t \simeq u$, the composition of these isomorphisms is associative, i.e., $(ab \circ bc) \circ cd = ab \circ (bc \circ cd)$.

RelIso.cast definition

{α β : Type u} {r : α → α → Prop} {s : β → β → Prop} (h₁ : α = β) (h₂ : HEq r s) : r ≃r s

Full source

/-- A relation isomorphism between equal relations on equal types. -/
@[simps! toEquiv apply]
protected def cast {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} (h₁ : α = β)
    (h₂ : HEq r s) : r ≃r s :=
  ⟨Equiv.cast h₁, @fun a b => by
    subst h₁
    rw [eq_of_heq h₂]
    rfl⟩

Relation isomorphism via type casting

Informal description

Given two types $\alpha$ and $\beta$ with relations $r$ and $s$ respectively, and given proofs that $\alpha$ is equal to $\beta$ and that $r$ is hereditarily equal to $s$, the function constructs a relation isomorphism between $r$ and $s$ by casting the equivalence between $\alpha$ and $\beta$ and using the equality of relations.

RelIso.cast_symm theorem

 {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} (h₁ : α = β) (h₂ : HEq r s) :
  (RelIso.cast h₁ h₂).symm = RelIso.cast h₁.symm h₂.symm

Full source

@[simp]
protected theorem cast_symm {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} (h₁ : α = β)
    (h₂ : HEq r s) : (RelIso.cast h₁ h₂).symm = RelIso.cast h₁.symm h₂.symm :=
  rfl

Inverse of Cast Relation Isomorphism Equals Cast of Symmetric Equalities

Informal description

Given two types $\alpha$ and $\beta$ with relations $r$ and $s$ respectively, and given proofs that $\alpha$ is equal to $\beta$ and that $r$ is hereditarily equal to $s$, the inverse of the relation isomorphism constructed by casting is equal to the relation isomorphism constructed by casting the symmetric equalities $h_1^{-1}$ and $h_2^{-1}$.

RelIso.cast_trans theorem

 {α β γ : Type u} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (h₁ : α = β) (h₁' : β = γ) (h₂ : HEq r s)
  (h₂' : HEq s t) : (RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂') = RelIso.cast (h₁.trans h₁') (h₂.trans h₂')

Full source

@[simp]
protected theorem cast_trans {α β γ : Type u} {r : α → α → Prop} {s : β → β → Prop}
    {t : γ → γ → Prop} (h₁ : α = β) (h₁' : β = γ) (h₂ : HEq r s) (h₂' : HEq s t) :
    (RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂') = RelIso.cast (h₁.trans h₁') (h₂.trans h₂') :=
  ext fun x => by subst h₁; rfl

Transitivity of Cast Relation Isomorphisms via Type and Relation Equalities

Informal description

Given types $\alpha$, $\beta$, $\gamma$ with relations $r$, $s$, $t$ respectively, and equalities $h_1 : \alpha = \beta$, $h_1' : \beta = \gamma$, and hereditary equalities $h_2 : r \equiv s$, $h_2' : s \equiv t$, the composition of the relation isomorphisms constructed by casting via $h_1$, $h_2$ and $h_1'$, $h_2'$ is equal to the relation isomorphism constructed by casting via the transitivity of $h_1$ and $h_1'$ and the transitivity of $h_2$ and $h_2'$.

RelIso.swap definition

(f : r ≃r s) : swap r ≃r swap s

Full source

/-- A relation isomorphism is also a relation isomorphism between dual relations. -/
protected def swap (f : r ≃r s) : swapswap r ≃r swap s :=
  ⟨f, f.map_rel_iff⟩

Relation isomorphism between swapped relations

Informal description

Given a relation isomorphism $f$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the function $f$ also defines a relation isomorphism between the swapped relations $\text{swap } r$ on $\alpha$ and $\text{swap } s$ on $\beta$, where $\text{swap } r(a, b) = r(b, a)$ and similarly for $s$.

RelIso.compl definition

(f : r ≃r s) : rᶜ ≃r sᶜ

Full source

/-- A relation isomorphism is also a relation isomorphism between complemented relations. -/
@[simps!]
protected def compl (f : r ≃r s) : rᶜrᶜ ≃r sᶜ :=
  ⟨f, f.map_rel_iff.not⟩

Relation isomorphism between complemented relations

Informal description

Given a relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the function $f$ also defines a relation isomorphism between the complemented relations $r^c$ on $\alpha$ and $s^c$ on $\beta$. Specifically, for any $x, y \in \alpha$, $\neg r(x, y) \leftrightarrow \neg s(f(x), f(y))$.

RelIso.coe_fn_symm_mk theorem

(f o) : ((@RelIso.mk _ _ r s f @o).symm : β → α) = f.symm

Full source

@[simp]
theorem coe_fn_symm_mk (f o) : ((@RelIso.mk _ _ r s f @o).symm : β → α) = f.symm :=
  rfl

Inverse of Relation Isomorphism Construction Preserves Inverse Function

Informal description

For any relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and any proof $o$ that $f$ preserves these relations, the underlying function of the inverse isomorphism $(f^{-1} : \beta \to \alpha)$ equals the inverse function $f^{-1}$ of $f$.

RelIso.rel_symm_apply theorem

(e : r ≃r s) {x y} : r x (e.symm y) ↔ s (e x) y

Full source

theorem rel_symm_apply (e : r ≃r s) {x y} : r x (e.symm y) ↔ s (e x) y := by
  rw [← e.map_rel_iff, e.apply_symm_apply]

Relation Symmetry under Isomorphism: $r(x, e^{-1}(y)) \leftrightarrow s(e(x), y)$

Informal description

For any relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $x \in \alpha$ and $y \in \beta$, the relation $r(x, e^{-1}(y))$ holds if and only if $s(e(x), y)$ holds.

RelIso.symm_apply_rel theorem

(e : r ≃r s) {x y} : r (e.symm x) y ↔ s x (e y)

Full source

theorem symm_apply_rel (e : r ≃r s) {x y} : r (e.symm x) y ↔ s x (e y) := by
  rw [← e.map_rel_iff, e.apply_symm_apply]

Relation Preservation under Inverse Isomorphism: $r(e^{-1}(x), y) \leftrightarrow s(x, e(y))$

Informal description

For any relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $x \in \beta$ and $y \in \alpha$, we have $r(e^{-1}(x), y)$ if and only if $s(x, e(y))$.

RelIso.bijective theorem

(e : r ≃r s) : Bijective e

Full source

protected theorem bijective (e : r ≃r s) : Bijective e :=
  e.toEquiv.bijective

Bijectivity of Relation Isomorphisms

Informal description

For any relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the function $e$ is bijective (both injective and surjective).

RelIso.injective theorem

(e : r ≃r s) : Injective e

Full source

protected theorem injective (e : r ≃r s) : Injective e :=
  e.toEquiv.injective

Injectivity of Relation Isomorphisms

Informal description

For any relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the function $e$ is injective.

RelIso.surjective theorem

(e : r ≃r s) : Surjective e

Full source

protected theorem surjective (e : r ≃r s) : Surjective e :=
  e.toEquiv.surjective

Surjectivity of Relation Isomorphisms

Informal description

For any relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the function $e$ is surjective, meaning for every $y \in \beta$, there exists an $x \in \alpha$ such that $e(x) = y$.

RelIso.copy definition

(e : r ≃r s) (f : α → β) (g : β → α) (hf : f = e) (hg : g = e.symm) : r ≃r s

Full source

/-- Copy of a `RelIso` with a new `toFun` and `invFun` equal to the old ones.
Useful to fix definitional equalities. -/
def copy (e : r ≃r s) (f : α → β) (g : β → α) (hf : f = e) (hg : g = e.symm) : r ≃r s where
  toFun := f
  invFun := g
  left_inv _ := by simp [hf, hg]
  right_inv _ := by simp [hf, hg]
  map_rel_iff' := by simp [hf, e.map_rel_iff]

Copy of a relation isomorphism with specified forward and inverse maps

Informal description

Given a relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and functions $f : \alpha \to \beta$ and $g : \beta \to \alpha$ such that $f = e$ and $g = e^{-1}$, the structure `RelIso.copy` constructs a new relation isomorphism with $f$ as its forward map and $g$ as its inverse, while preserving all relation-preserving properties of the original isomorphism $e$.

RelIso.coe_copy theorem

(e : r ≃r s) (f : α → β) (g : β → α) (hf hg) : e.copy f g hf hg = f

Full source

@[simp, norm_cast]
lemma coe_copy (e : r ≃r s) (f : α → β) (g : β → α) (hf hg) : e.copy f g hf hg = f := rfl

Coercion of Copied Relation Isomorphism Equals Forward Map

Informal description

Given a relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and functions $f : \alpha \to \beta$ and $g : \beta \to \alpha$ such that $f = e$ and $g = e^{-1}$, the coercion of the copied relation isomorphism $e.copy\,f\,g\,hf\,hg$ equals $f$.

RelIso.copy_eq theorem

(e : r ≃r s) (f : α → β) (g : β → α) (hf hg) : e.copy f g hf hg = e

Full source

lemma copy_eq (e : r ≃r s) (f : α → β) (g : β → α) (hf hg) : e.copy f g hf hg = e :=
  DFunLike.coe_injective hf

Equality of Copied Relation Isomorphism with Original

Informal description

Given a relation isomorphism $e : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and functions $f : \alpha \to \beta$ and $g : \beta \to \alpha$ such that $f = e$ and $g = e^{-1}$, the copied relation isomorphism $e.copy\,f\,g\,hf\,hg$ is equal to the original isomorphism $e$.

RelIso.preimage definition

(f : α ≃ β) (s : β → β → Prop) : f ⁻¹'o s ≃r s

Full source

/-- Any equivalence lifts to a relation isomorphism between `s` and its preimage. -/
protected def preimage (f : α ≃ β) (s : β → β → Prop) : f ⁻¹'o sf ⁻¹'o s ≃r s :=
  ⟨f, Iff.rfl⟩

Relation isomorphism induced by preimage of an equivalence

Informal description

Given an equivalence $f : \alpha \simeq \beta$ and a relation $s$ on $\beta$, the relation isomorphism $\text{RelIso.preimage}$ maps $f$ and $s$ to a relation isomorphism between the preimage relation $f^{-1} \circ s$ on $\alpha$ and the original relation $s$ on $\beta$.

RelIso.IsWellOrder.preimage instance

{α : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) : IsWellOrder β (f ⁻¹'o r)

Full source

instance IsWellOrder.preimage {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) :
    IsWellOrder β (f ⁻¹'o r) :=
  @RelEmbedding.isWellOrder _ _ (f ⁻¹'o r) r (RelIso.preimage f r) _

Well-Order Preservation under Preimage of Equivalence

Informal description

For any well-order $r$ on a type $\alpha$ and an equivalence $f : \beta \simeq \alpha$, the preimage relation $f^{-1} \circ r$ on $\beta$ is also a well-order.

RelIso.IsWellOrder.ulift instance

{α : Type u} (r : α → α → Prop) [IsWellOrder α r] : IsWellOrder (ULift α) (ULift.down ⁻¹'o r)

Full source

instance IsWellOrder.ulift {α : Type u} (r : α → α → Prop) [IsWellOrder α r] :
    IsWellOrder (ULift α) (ULift.downULift.down ⁻¹'o r) :=
  IsWellOrder.preimage r Equiv.ulift

Well-Order Preservation under Lifting

Informal description

For any well-order $r$ on a type $\alpha$, the preimage relation $\text{ULift.down}^{-1} \circ r$ on the lifted type $\text{ULift }\alpha$ is also a well-order.

RelIso.ofSurjective definition

(f : r ↪r s) (H : Surjective f) : r ≃r s

Full source

/-- A surjective relation embedding is a relation isomorphism. -/
@[simps! apply]
noncomputable def ofSurjective (f : r ↪r s) (H : Surjective f) : r ≃r s :=
  ⟨Equiv.ofBijective f ⟨f.injective, H⟩, f.map_rel_iff⟩

Relation isomorphism induced by a surjective relation embedding

Informal description

Given a relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, if $f$ is surjective, then $f$ induces a relation isomorphism between $r$ and $s$. Specifically, the relation isomorphism is constructed by viewing $f$ as a bijective function (due to its injectivity from being an embedding and surjectivity from the hypothesis) and using the fact that $f$ preserves and reflects the relations (i.e., $r(a,b) \leftrightarrow s(f(a),f(b))$ for all $a,b \in \alpha$).

RelIso.sumLexCongr definition

 {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂} (e₁ : @RelIso α₁ β₁ r₁ s₁) (e₂ : @RelIso α₂ β₂ r₂ s₂) : Sum.Lex r₁ r₂ ≃r Sum.Lex s₁ s₂

Full source

/-- Given relation isomorphisms `r₁ ≃r s₁` and `r₂ ≃r s₂`, construct a relation isomorphism for the
lexicographic orders on the sum.
-/
def sumLexCongr {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂} (e₁ : @RelIso α₁ β₁ r₁ s₁) (e₂ : @RelIso α₂ β₂ r₂ s₂) :
    Sum.LexSum.Lex r₁ r₂ ≃r Sum.Lex s₁ s₂ :=
  ⟨Equiv.sumCongr e₁.toEquiv e₂.toEquiv, @fun a b => by
    obtain ⟨f, hf⟩ := e₁; obtain ⟨g, hg⟩ := e₂; cases a <;> cases b <;> simp [hf, hg]⟩

Lexicographic sum of relation isomorphisms

Informal description

Given relation isomorphisms $e_1 : r_1 \simeqr s_1$ between types $\alpha_1$ and $\beta_1$ and $e_2 : r_2 \simeqr s_2$ between types $\alpha_2$ and $\beta_2$, this constructs a relation isomorphism between the lexicographic orders on the sum types $\alpha_1 \oplus \alpha_2$ and $\beta_1 \oplus \beta_2$. Specifically, it shows that $\text{Sum.Lex } r_1 r_2 \simeqr \text{Sum.Lex } s_1 s_2$.

RelIso.prodLexCongr definition

 {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂} (e₁ : @RelIso α₁ β₁ r₁ s₁) (e₂ : @RelIso α₂ β₂ r₂ s₂) : Prod.Lex r₁ r₂ ≃r Prod.Lex s₁ s₂

Full source

/-- Given relation isomorphisms `r₁ ≃r s₁` and `r₂ ≃r s₂`, construct a relation isomorphism for the
lexicographic orders on the product.
-/
def prodLexCongr {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂} (e₁ : @RelIso α₁ β₁ r₁ s₁) (e₂ : @RelIso α₂ β₂ r₂ s₂) :
    Prod.LexProd.Lex r₁ r₂ ≃r Prod.Lex s₁ s₂ :=
  ⟨Equiv.prodCongr e₁.toEquiv e₂.toEquiv, by simp [Prod.lex_def, e₁.map_rel_iff, e₂.map_rel_iff,
    e₁.injective.eq_iff]⟩

Lexicographic product of relation isomorphisms

Informal description

Given relation isomorphisms $e₁ : r₁ ≃r s₁$ between types $\alpha₁$ and $\beta₁$ and $e₂ : r₂ ≃r s₂$ between types $\alpha₂$ and $\beta₂$, this constructs a relation isomorphism between the lexicographic orders on the product types $\alpha₁ \times \alpha₂$ and $\beta₁ \times \beta₂$. Specifically, it shows that $\text{Prod.Lex } r₁ r₂ \simeqr \text{Prod.Lex } s₁ s₂$.

RelIso.relIsoOfIsEmpty definition

(r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] [IsEmpty β] : r ≃r s

Full source

/-- Two relations on empty types are isomorphic. -/
def relIsoOfIsEmpty (r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] [IsEmpty β] : r ≃r s :=
  ⟨Equiv.equivOfIsEmpty α β, @fun a => isEmptyElim a⟩

Relation isomorphism between empty types

Informal description

Given two empty types $\alpha$ and $\beta$ with relations $r$ and $s$ respectively, there exists a relation isomorphism between $r$ and $s$. This isomorphism is constructed using the unique equivalence between empty types and satisfies the condition that for any (non-existent) elements $a, b \in \alpha$, the relation $r(a, b)$ holds if and only if $s(f(a), f(b))$ holds, where $f$ is the equivalence map.

RelIso.ofUniqueOfIrrefl definition

(r : α → α → Prop) (s : β → β → Prop) [IsIrrefl α r] [IsIrrefl β s] [Unique α] [Unique β] : r ≃r s

Full source

/-- Two irreflexive relations on a unique type are isomorphic. -/
def ofUniqueOfIrrefl (r : α → α → Prop) (s : β → β → Prop) [IsIrrefl α r]
    [IsIrrefl β s] [Unique α] [Unique β] : r ≃r s :=
  ⟨Equiv.ofUnique α β, iff_of_false (not_rel_of_subsingleton s _ _)
      (not_rel_of_subsingleton r _ _) ⟩

Relation isomorphism between irreflexive relations on unique types

Informal description

Given two irreflexive relations $r$ on a unique type $\alpha$ and $s$ on a unique type $\beta$, there exists a relation isomorphism between $r$ and $s$. This isomorphism is constructed using the unique equivalence between $\alpha$ and $\beta$ and satisfies the condition that for any elements $a, b \in \alpha$, the relation $r(a, b)$ holds if and only if $s(f(a), f(b))$ holds, where $f$ is the equivalence map.

RelIso.ofUniqueOfRefl definition

(r : α → α → Prop) (s : β → β → Prop) [IsRefl α r] [IsRefl β s] [Unique α] [Unique β] : r ≃r s

Full source

/-- Two reflexive relations on a unique type are isomorphic. -/
def ofUniqueOfRefl (r : α → α → Prop) (s : β → β → Prop) [IsRefl α r] [IsRefl β s]
    [Unique α] [Unique β] : r ≃r s :=
  ⟨Equiv.ofUnique α β, iff_of_true (rel_of_subsingleton s _ _) (rel_of_subsingleton r _ _)⟩

Relation isomorphism between reflexive relations on unique types

Informal description

Given two reflexive relations $r$ on a unique type $\alpha$ and $s$ on a unique type $\beta$, there exists a relation isomorphism between $r$ and $s$. This isomorphism is constructed using the unique equivalence between $\alpha$ and $\beta$ and satisfies the condition that for any elements $a, b \in \alpha$, the relation $r(a, b)$ holds if and only if $s(f(a), f(b))$ holds, where $f$ is the equivalence map.

Mathlib.Order.RelIso.Basic

Main declarations

Notation