# Relation homomorphisms, embeddings, isomorphisms #

This file defines relation homomorphisms, embeddings, isomorphisms and order embeddings and isomorphisms.

## Main declarations #

• RelHom: Relation homomorphism. A RelHom r s is a function f : α → β such that r a b → s (f a) (f b).
• RelEmbedding: Relation embedding. A RelEmbedding r s is an embedding f : α ↪ β such that r a b ↔ s (f a) (f b).
• RelIso: Relation isomorphism. A RelIso r s is an equivalence f : α ≃ β such that r a b ↔ s (f a) (f b).
• sumLexCongr, prodLexCongr: Creates a relation homomorphism between two Sum.Lex or two Prod.Lex from relation homomorphisms between their arguments.

## Notation #

• →r: RelHom
• ↪r: RelEmbedding
• ≃r: RelIso
structure RelHom {α : Type u_5} {β : Type u_6} (r : ααProp) (s : ββProp) :
Type (max u_5 u_6)

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).

• toFun : αβ

The underlying function of a RelHom

• map_rel' : ∀ {a b : α}, r a bs (self.toFun a) (self.toFun b)

A RelHom sends related elements to related elements

Instances For
theorem RelHom.map_rel' {α : Type u_5} {β : Type u_6} {r : ααProp} {s : ββProp} (self : r →r s) {a : α} {b : α} :
r a bs (self.toFun a) (self.toFun b)

A RelHom sends related elements to related elements

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).

Equations
Instances For
class RelHomClass (F : Type u_5) {α : Type u_6} {β : Type u_7} (r : outParam (ααProp)) (s : outParam (ββProp)) [FunLike F α β] :

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 outParams since figuring them out from a goal is a higher-order matching problem that Lean usually can't do unaided.

• map_rel : ∀ (f : F) {a b : α}, r a bs (f a) (f b)

A RelHomClass sends related elements to related elements

Instances
theorem RelHomClass.map_rel {F : Type u_5} {α : Type u_6} {β : Type u_7} {r : outParam (ααProp)} {s : outParam (ββProp)} [FunLike F α β] [self : RelHomClass F r s] (f : F) {a : α} {b : α} :
r a bs (f a) (f b)

A RelHomClass sends related elements to related elements

theorem RelHomClass.isIrrefl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) [IsIrrefl β s] :
theorem RelHomClass.isAsymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) [IsAsymm β s] :
IsAsymm α r
theorem RelHomClass.acc {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) (a : α) :
Acc s (f a)Acc r a
theorem RelHomClass.wellFounded {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) :
theorem RelHomClass.isWellFounded {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) [] :
instance RelHom.instFunLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
FunLike (r →r s) α β
Equations
• RelHom.instFunLike = { coe := fun (o : r →r s) => o.toFun, coe_injective' := }
instance RelHom.instRelHomClass {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
RelHomClass (r →r s) r s
Equations
• =
theorem RelHom.map_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r →r s) {a : α} {b : α} :
r a bs (f a) (f b)
@[simp]
theorem RelHom.coe_fn_toFun {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r →r s) :
f.toFun = f
theorem RelHom.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
Function.Injective fun (f : r →r s) => f

The map coe_fn : (r →r s) → (α → β) is injective.

theorem RelHom.ext_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r →r s} {g : r →r s} :
f = g ∀ (x : α), f x = g x
theorem RelHom.ext {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} ⦃f : r →r s ⦃g : r →r s (h : ∀ (x : α), f x = g x) :
f = g
@[simp]
theorem RelHom.id_apply {α : Type u_1} (r : ααProp) (x : α) :
(RelHom.id r) x = x
def RelHom.id {α : Type u_1} (r : ααProp) :
r →r r

Identity map is a relation homomorphism.

Equations
• = { toFun := fun (x : α) => x, map_rel' := }
Instances For
@[simp]
theorem RelHom.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (g : s →r t) (f : r →r s) (x : α) :
(g.comp f) x = g (f x)
def RelHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (g : s →r t) (f : r →r s) :
r →r t

Composition of two relation homomorphisms is a relation homomorphism.

Equations
• g.comp f = { toFun := fun (x : α) => g (f x), map_rel' := }
Instances For
def RelHom.swap {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r →r s) :

A relation homomorphism is also a relation homomorphism between dual relations.

Equations
• f.swap = { toFun := f, map_rel' := }
Instances For
def RelHom.preimage {α : Type u_1} {β : Type u_2} (f : αβ) (s : ββProp) :

A function is a relation homomorphism from the preimage relation of s to s.

Equations
• = { toFun := f, map_rel' := }
Instances For
theorem injective_of_increasing {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [] [IsIrrefl β s] (f : αβ) (hf : ∀ {x y : α}, r x ys (f x) (f y)) :

An increasing function is injective

theorem RelHom.injective_of_increasing {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] [IsIrrefl β s] (f : r →r s) :

An increasing function is injective

theorem Function.Surjective.wellFounded_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : αβ} (hf : ) (o : ∀ {a b : α}, r a b s (f a) (f b)) :
structure RelEmbedding {α : Type u_5} {β : Type u_6} (r : ααProp) (s : ββProp) extends :
Type (max u_5 u_6)

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).

• toFun : αβ
• inj' : Function.Injective self.toFun
• map_rel_iff' : ∀ {a b : α}, s (self.toEmbedding a) (self.toEmbedding b) r a b

Elements are related iff they are related after apply a RelEmbedding

Instances For
theorem RelEmbedding.map_rel_iff' {α : Type u_5} {β : Type u_6} {r : ααProp} {s : ββProp} (self : r ↪r s) {a : α} {b : α} :
s (self.toEmbedding a) (self.toEmbedding b) r a b

Elements are related iff they are related after apply a RelEmbedding

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).

Equations
Instances For
def Subtype.relEmbedding {X : Type u_5} (r : XXProp) (p : XProp) :
Subtype.val ⁻¹'o r ↪r r

The induced relation on a subtype is an embedding under the natural inclusion.

Equations
• = { toEmbedding := , map_rel_iff' := }
Instances For
theorem preimage_equivalence {α : Type u_5} {β : Type u_6} (f : αβ) {s : ββProp} (hs : ) :
def RelEmbedding.toRelHom {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) :
r →r s

A relation embedding is also a relation homomorphism

Equations
• f.toRelHom = { toFun := f.toFun, map_rel' := }
Instances For
instance RelEmbedding.instCoeRelHom {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
Coe (r ↪r s) (r →r s)
Equations
• RelEmbedding.instCoeRelHom = { coe := RelEmbedding.toRelHom }
instance RelEmbedding.instFunLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
FunLike (r ↪r s) α β
Equations
• RelEmbedding.instFunLike = { coe := fun (x : r ↪r s) => x.toFun, coe_injective' := }
instance RelEmbedding.instRelHomClass {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
RelHomClass (r ↪r s) r s
Equations
• =
instance RelEmbedding.instEmbeddingLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
EmbeddingLike (r ↪r s) α β
Equations
• =
@[simp]
theorem RelEmbedding.coe_toEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ↪r s} :
f.toEmbedding = f
@[simp]
theorem RelEmbedding.coe_toRelHom {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ↪r s} :
f.toRelHom = f
theorem RelEmbedding.toEmbedding_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
Function.Injective RelEmbedding.toEmbedding
@[simp]
theorem RelEmbedding.toEmbedding_inj {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ↪r s} {g : r ↪r s} :
f.toEmbedding = g.toEmbedding f = g
theorem RelEmbedding.injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) :
theorem RelEmbedding.inj {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) {a : α} {b : α} :
f a = f b a = b
theorem RelEmbedding.map_rel_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) {a : α} {b : α} :
s (f a) (f b) r a b
@[simp]
theorem RelEmbedding.coe_mk {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : α β} {h : ∀ {a b : α}, s (f a) (f b) r a b} :
{ toEmbedding := f, map_rel_iff' := h } = f
theorem RelEmbedding.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
Function.Injective fun (f : r ↪r s) => f

The map coe_fn : (r ↪r s) → (α → β) is injective.

theorem RelEmbedding.ext_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ↪r s} {g : r ↪r s} :
f = g ∀ (x : α), f x = g x
theorem RelEmbedding.ext {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} ⦃f : r ↪r s ⦃g : r ↪r s (h : ∀ (x : α), f x = g x) :
f = g
@[simp]
theorem RelEmbedding.refl_apply {α : Type u_1} (r : ααProp) (a : α) :
a = a
def RelEmbedding.refl {α : Type u_1} (r : ααProp) :
r ↪r r

Identity map is a relation embedding.

Equations
• = { toEmbedding := , map_rel_iff' := }
Instances For
def RelEmbedding.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ↪r s) (g : s ↪r t) :
r ↪r t

Composition of two relation embeddings is a relation embedding.

Equations
• f.trans g = { toEmbedding := f.trans g.toEmbedding, map_rel_iff' := }
Instances For
instance RelEmbedding.instInhabited {α : Type u_1} (r : ααProp) :
Equations
• = { default := }
theorem RelEmbedding.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ↪r s) (g : s ↪r t) (a : α) :
(f.trans g) a = g (f a)
@[simp]
theorem RelEmbedding.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ↪r s) (g : s ↪r t) :
(f.trans g) = g f
def RelEmbedding.swap {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) :

A relation embedding is also a relation embedding between dual relations.

Equations
• f.swap = { toEmbedding := f.toEmbedding, map_rel_iff' := }
Instances For
def RelEmbedding.preimage {α : Type u_1} {β : Type u_2} (f : α β) (s : ββProp) :
f ⁻¹'o s ↪r s

If f is injective, then it is a relation embedding from the preimage relation of s to s.

Equations
• = { toEmbedding := f, map_rel_iff' := }
Instances For
theorem RelEmbedding.eq_preimage {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) :
r = f ⁻¹'o s
theorem RelEmbedding.isIrrefl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [IsIrrefl β s] :
theorem RelEmbedding.isRefl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [IsRefl β s] :
IsRefl α r
theorem RelEmbedding.isSymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [IsSymm β s] :
IsSymm α r
theorem RelEmbedding.isAsymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [IsAsymm β s] :
IsAsymm α r
theorem RelEmbedding.isAntisymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
r ↪r s∀ [inst : ],
theorem RelEmbedding.isTrans {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
r ↪r s∀ [inst : IsTrans β s], IsTrans α r
theorem RelEmbedding.isTotal {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
r ↪r s∀ [inst : IsTotal β s], IsTotal α r
theorem RelEmbedding.isPreorder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
r ↪r s∀ [inst : ],
theorem RelEmbedding.isPartialOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
r ↪r s∀ [inst : ],
theorem RelEmbedding.isLinearOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
r ↪r s∀ [inst : ],
theorem RelEmbedding.isStrictOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
r ↪r s∀ [inst : ],
theorem RelEmbedding.isTrichotomous {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
r ↪r s∀ [inst : ],
theorem RelEmbedding.isStrictTotalOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
r ↪r s∀ [inst : ],
theorem RelEmbedding.acc {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) (a : α) :
Acc s (f a)Acc r a
theorem RelEmbedding.wellFounded {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
r ↪r s
theorem RelEmbedding.isWellFounded {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) [] :
theorem RelEmbedding.isWellOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
r ↪r s∀ [inst : ],
instance Subtype.wellFoundedLT {α : Type u_1} [LT α] [] (p : αProp) :
Equations
• =
instance Subtype.wellFoundedGT {α : Type u_1} [LT α] [] (p : αProp) :
Equations
• =
@[simp]
theorem Quotient.mkRelHom_apply {α : Type u_1} [] {r : ααProp} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) (a : α) :
a =
def Quotient.mkRelHom {α : Type u_1} [] {r : ααProp} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) :
r →r

Quotient.mk' as a relation homomorphism between the relation and the lift of a relation.

Equations
• = { toFun := Quotient.mk', map_rel' := }
Instances For
@[simp]
theorem Quotient.outRelEmbedding_apply {α : Type u_1} [] {r : ααProp} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) :
∀ (a : Quotient inst✝), = a.out
noncomputable def Quotient.outRelEmbedding {α : Type u_1} [] {r : ααProp} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) :
↪r r

Quotient.out as a relation embedding between the lift of a relation and the relation.

Equations
• = { toEmbedding := , map_rel_iff' := }
Instances For
@[simp]
theorem Quotient.out'RelEmbedding_apply {α : Type u_1} :
∀ {x : } {r : ααProp} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) (a : ), = a.out'
noncomputable def Quotient.out'RelEmbedding {α : Type u_1} :
{x : } → {r : ααProp} → (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) → (fun (a b : ) => a.liftOn₂' b r H) ↪r r

Quotient.out' as a relation embedding between the lift of a relation and the relation.

Equations
• = { toFun := Quotient.out', inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem acc_lift₂_iff {α : Type u_1} [] {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
@[simp]
theorem acc_liftOn₂'_iff {α : Type u_1} {s : } {r : ααProp} {H : ∀ (a₁ a₂ b₁ b₂ : α), Setoid.r a₁ b₁Setoid.r a₂ b₂r a₁ a₂ = r b₁ b₂} {a : α} :
Acc (fun (x y : ) => x.liftOn₂' y r H) Acc r a
@[simp]
theorem wellFounded_lift₂_iff {α : Type u_1} [] {r : ααProp} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂} :

A relation is well founded iff its lift to a quotient is.

theorem WellFounded.of_quotient_lift₂ {α : Type u_1} [] {r : ααProp} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂} :

Alias of the forward direction of wellFounded_lift₂_iff.

A relation is well founded iff its lift to a quotient is.

theorem WellFounded.quotient_lift₂ {α : Type u_1} [] {r : ααProp} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂} :

Alias of the reverse direction of wellFounded_lift₂_iff.

A relation is well founded iff its lift to a quotient is.

@[simp]
theorem wellFounded_liftOn₂'_iff {α : Type u_1} {s : } {r : ααProp} {H : ∀ (a₁ a₂ b₁ b₂ : α), Setoid.r a₁ b₁Setoid.r a₂ b₂r a₁ a₂ = r b₁ b₂} :
(WellFounded fun (x y : ) => x.liftOn₂' y r H)
theorem WellFounded.of_quotient_liftOn₂' {α : Type u_1} {s : } {r : ααProp} {H : ∀ (a₁ a₂ b₁ b₂ : α), Setoid.r a₁ b₁Setoid.r a₂ b₂r a₁ a₂ = r b₁ b₂} :
(WellFounded fun (x y : ) => x.liftOn₂' y r H)

Alias of the forward direction of wellFounded_liftOn₂'_iff.

theorem WellFounded.quotient_liftOn₂' {α : Type u_1} {s : } {r : ααProp} {H : ∀ (a₁ a₂ b₁ b₂ : α), Setoid.r a₁ b₁Setoid.r a₂ b₂r a₁ a₂ = r b₁ b₂} :
WellFounded fun (x y : ) => x.liftOn₂' y r H

Alias of the reverse direction of wellFounded_liftOn₂'_iff.

def RelEmbedding.ofMapRelIff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : αβ) [] [IsRefl β s] (hf : ∀ (a b : α), s (f a) (f b) r a b) :
r ↪r s

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.

Equations
• = { toFun := f, inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.ofMapRelIff_coe {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : αβ) [] [IsRefl β s] (hf : ∀ (a b : α), s (f a) (f b) r a b) :
= f
def RelEmbedding.ofMonotone {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] [IsAsymm β s] (f : αβ) (H : ∀ (a b : α), r a bs (f a) (f b)) :
r ↪r s

It suffices to prove f is monotone between strict relations to show it is a relation embedding.

Equations
• = { toFun := f, inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.ofMonotone_coe {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] [IsAsymm β s] (f : αβ) (H : ∀ (a b : α), r a bs (f a) (f b)) :
= f
def RelEmbedding.ofIsEmpty {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [] :
r ↪r s

A relation embedding from an empty type.

Equations
• = { toEmbedding := Function.Embedding.ofIsEmpty, map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.sumLiftRelInl_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : α) :
val = Sum.inl val
def RelEmbedding.sumLiftRelInl {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :
r ↪r

Sum.inl as a relation embedding into Sum.LiftRel r s.

Equations
• = { toFun := Sum.inl, inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.sumLiftRelInr_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : β) :
val = Sum.inr val
def RelEmbedding.sumLiftRelInr {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :
s ↪r

Sum.inr as a relation embedding into Sum.LiftRel r s.

Equations
• = { toFun := Sum.inr, inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.sumLiftRelMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :
∀ (a : α γ), (f.sumLiftRelMap g) a = Sum.map (⇑f) (⇑g) a
def RelEmbedding.sumLiftRelMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :

Sum.map as a relation embedding between Sum.LiftRel relations.

Equations
• f.sumLiftRelMap g = { toFun := Sum.map f g, inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.sumLexInl_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : α) :
val = Sum.inl val
def RelEmbedding.sumLexInl {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :

Sum.inl as a relation embedding into Sum.Lex r s.

Equations
• = { toFun := Sum.inl, inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.sumLexInr_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (val : β) :
val = Sum.inr val
def RelEmbedding.sumLexInr {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :

Sum.inr as a relation embedding into Sum.Lex r s.

Equations
• = { toFun := Sum.inr, inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.sumLexMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :
∀ (a : α γ), (f.sumLexMap g) a = Sum.map (⇑f) (⇑g) a
def RelEmbedding.sumLexMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :

Sum.map as a relation embedding between Sum.Lex relations.

Equations
• f.sumLexMap g = { toFun := Sum.map f g, inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.prodLexMkLeft_apply {α : Type u_1} {β : Type u_2} {r : ααProp} (s : ββProp) {a : α} (h : ¬r a a) (snd : β) :
snd = (a, snd)
def RelEmbedding.prodLexMkLeft {α : Type u_1} {β : Type u_2} {r : ααProp} (s : ββProp) {a : α} (h : ¬r a a) :

fun b ↦ Prod.mk a b as a relation embedding.

Equations
• = { toFun := , inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.prodLexMkRight_apply {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) {b : β} (h : ¬s b b) (a : α) :
a = (a, b)
def RelEmbedding.prodLexMkRight {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) {b : β} (h : ¬s b b) :

fun a ↦ Prod.mk a b as a relation embedding.

Equations
• = { toFun := fun (a : α) => (a, b), inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.prodLexMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :
∀ (a : α × γ), (f.prodLexMap g) a = Prod.map (⇑f) (⇑g) a
def RelEmbedding.prodLexMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : ααProp} {s : ββProp} {t : γγProp} {u : δδProp} (f : r ↪r s) (g : t ↪r u) :

Prod.map as a relation embedding.

Equations
• f.prodLexMap g = { toFun := Prod.map f g, inj' := , map_rel_iff' := }
Instances For
structure RelIso {α : Type u_5} {β : Type u_6} (r : ααProp) (s : ββProp) extends :
Type (max u_5 u_6)

A relation isomorphism is an equivalence that is also a relation embedding.

• toFun : αβ
• invFun : βα
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_rel_iff' : ∀ {a b : α}, s (self.toEquiv a) (self.toEquiv b) r a b

Elements are related iff they are related after apply a RelIso

Instances For
theorem RelIso.map_rel_iff' {α : Type u_5} {β : Type u_6} {r : ααProp} {s : ββProp} (self : r ≃r s) {a : α} {b : α} :
s (self.toEquiv a) (self.toEquiv b) r a b

Elements are related iff they are related after apply a RelIso

A relation isomorphism is an equivalence that is also a relation embedding.

Equations
Instances For
def RelIso.toRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
r ↪r s

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.

Equations
• f.toRelEmbedding = { toEmbedding := f.toEmbedding, map_rel_iff' := }
Instances For
theorem RelIso.toEquiv_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
Function.Injective RelIso.toEquiv
instance RelIso.instCoeOutRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
CoeOut (r ≃r s) (r ↪r s)
Equations
• RelIso.instCoeOutRelEmbedding = { coe := RelIso.toRelEmbedding }
instance RelIso.instFunLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
FunLike (r ≃r s) α β
Equations
• RelIso.instFunLike = { coe := fun (x : r ≃r s) => x.toRelEmbedding, coe_injective' := }
instance RelIso.instRelHomClass {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
RelHomClass (r ≃r s) r s
Equations
• =
instance RelIso.instEquivLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
EquivLike (r ≃r s) α β
Equations
• RelIso.instEquivLike = { coe := fun (f : r ≃r s) => f, inv := fun (f : r ≃r s) => f.symm, left_inv := , right_inv := , coe_injective' := }
@[simp]
theorem RelIso.coe_toRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
f.toRelEmbedding = f
@[simp]
theorem RelIso.coe_toEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
f.toEmbedding = f
theorem RelIso.map_rel_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) {a : α} {b : α} :
s (f a) (f b) r a b
@[simp]
theorem RelIso.coe_fn_mk {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : α β) (o : ∀ ⦃a b : α⦄, s (f a) (f b) r a b) :
{ toEquiv := f, map_rel_iff' := o } = f
@[simp]
theorem RelIso.coe_fn_toEquiv {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
f.toEquiv = f
theorem RelIso.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
Function.Injective fun (f : r ≃r s) => f

The map DFunLike.coe : (r ≃r s) → (α → β) is injective.

theorem RelIso.ext_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ≃r s} {g : r ≃r s} :
f = g ∀ (x : α), f x = g x
theorem RelIso.ext {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} ⦃f : r ≃r s ⦃g : r ≃r s (h : ∀ (x : α), f x = g x) :
f = g
def RelIso.symm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
s ≃r r

Inverse map of a relation isomorphism is a relation isomorphism.

Equations
• f.symm = { toEquiv := f.symm, map_rel_iff' := }
Instances For
def RelIso.Simps.apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (h : r ≃r s) :
αβ

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.

Equations
Instances For
def RelIso.Simps.symm_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (h : r ≃r s) :
βα

See Note [custom simps projection].

Equations
• = h.symm
Instances For
@[simp]
theorem RelIso.refl_apply {α : Type u_1} (r : ααProp) (a : α) :
(RelIso.refl r) a = a
def RelIso.refl {α : Type u_1} (r : ααProp) :
r ≃r r

Identity map is a relation isomorphism.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
@[simp]
theorem RelIso.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f₁ : r ≃r s) (f₂ : s ≃r t) :
∀ (a : α), (f₁.trans f₂) a = f₂ (f₁ a)
def RelIso.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f₁ : r ≃r s) (f₂ : s ≃r t) :
r ≃r t

Composition of two relation isomorphisms is a relation isomorphism.

Equations
• f₁.trans f₂ = { toEquiv := f₁.trans f₂.toEquiv, map_rel_iff' := }
Instances For
instance RelIso.instInhabited {α : Type u_1} (r : ααProp) :
Equations
• = { default := }
@[simp]
theorem RelIso.default_def {α : Type u_1} (r : ααProp) :
default =
@[simp]
theorem RelIso.cast_toEquiv {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} (h₁ : α = β) (h₂ : HEq r s) :
(RelIso.cast h₁ h₂).toEquiv =
@[simp]
theorem RelIso.cast_apply {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} (h₁ : α = β) (h₂ : HEq r s) (a : α) :
(RelIso.cast h₁ h₂) a = cast h₁ a
def RelIso.cast {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} (h₁ : α = β) (h₂ : HEq r s) :
r ≃r s

A relation isomorphism between equal relations on equal types.

Equations
• RelIso.cast h₁ h₂ = { toEquiv := , map_rel_iff' := }
Instances For
@[simp]
theorem RelIso.cast_symm {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} (h₁ : α = β) (h₂ : HEq r s) :
(RelIso.cast h₁ h₂).symm =
@[simp]
theorem RelIso.cast_refl {α : Type u} {r : ααProp} (h₁ : optParam (α = α) ) (h₂ : optParam (HEq r r) ) :
RelIso.cast h₁ h₂ =
@[simp]
theorem RelIso.cast_trans {α : Type u} {β : Type u} {γ : 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₂') =
def RelIso.swap {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :

a relation isomorphism is also a relation isomorphism between dual relations.

Equations
• f.swap = { toEquiv := f.toEquiv, map_rel_iff' := }
Instances For
@[simp]
theorem RelIso.coe_fn_symm_mk {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : α β) (o : ∀ {a b : α}, s (f a) (f b) r a b) :
{ toEquiv := f, map_rel_iff' := o }.symm = f.symm
@[simp]
theorem RelIso.apply_symm_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) (x : β) :
e (e.symm x) = x
@[simp]
theorem RelIso.symm_apply_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) (x : α) :
e.symm (e x) = x
theorem RelIso.rel_symm_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) {x : α} {y : β} :
r x (e.symm y) s (e x) y
theorem RelIso.symm_apply_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) {x : β} {y : α} :
r (e.symm x) y s x (e y)
@[simp]
theorem RelIso.self_trans_symm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) :
e.trans e.symm =
@[simp]
theorem RelIso.symm_trans_self {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) :
e.symm.trans e =
theorem RelIso.bijective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) :
theorem RelIso.injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) :
theorem RelIso.surjective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) :
theorem RelIso.eq_iff_eq {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) {a : α} {b : α} :
f a = f b a = b
def RelIso.preimage {α : Type u_1} {β : Type u_2} (f : α β) (s : ββProp) :
f ⁻¹'o s ≃r s

Any equivalence lifts to a relation isomorphism between s and its preimage.

Equations
• = { toEquiv := f, map_rel_iff' := }
Instances For
instance RelIso.IsWellOrder.preimage {β : Type u_2} {α : Type u} (r : ααProp) [] (f : β α) :
IsWellOrder β (f ⁻¹'o r)
Equations
• =
instance RelIso.IsWellOrder.ulift {α : Type u} (r : ααProp) [] :
IsWellOrder (ULift.down ⁻¹'o r)
Equations
• =
@[simp]
theorem RelIso.ofSurjective_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) (H : ) (a : α) :
a = f a
noncomputable def RelIso.ofSurjective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) (H : ) :
r ≃r s

A surjective relation embedding is a relation isomorphism.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
def RelIso.sumLexCongr {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} {r₁ : α₁α₁Prop} {r₂ : α₂α₂Prop} {s₁ : β₁β₁Prop} {s₂ : β₂β₂Prop} (e₁ : r₁ ≃r s₁) (e₂ : r₂ ≃r s₂) :
Sum.Lex r₁ r₂ ≃r Sum.Lex s₁ s₂

Given relation isomorphisms r₁ ≃r s₁ and r₂ ≃r s₂, construct a relation isomorphism for the lexicographic orders on the sum.

Equations
• e₁.sumLexCongr e₂ = { toEquiv := e₁.sumCongr e₂.toEquiv, map_rel_iff' := }
Instances For
def RelIso.prodLexCongr {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} {r₁ : α₁α₁Prop} {r₂ : α₂α₂Prop} {s₁ : β₁β₁Prop} {s₂ : β₂β₂Prop} (e₁ : r₁ ≃r s₁) (e₂ : r₂ ≃r s₂) :
Prod.Lex r₁ r₂ ≃r Prod.Lex s₁ s₂

Given relation isomorphisms r₁ ≃r s₁ and r₂ ≃r s₂, construct a relation isomorphism for the lexicographic orders on the product.

Equations
• e₁.prodLexCongr e₂ = { toEquiv := e₁.prodCongr e₂.toEquiv, map_rel_iff' := }
Instances For
def RelIso.relIsoOfIsEmpty {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [] [] :
r ≃r s

Two relations on empty types are isomorphic.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
def RelIso.relIsoOfUniqueOfIrrefl {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsIrrefl α r] [IsIrrefl β s] [] [] :
r ≃r s

Two irreflexive relations on a unique type are isomorphic.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
def RelIso.relIsoOfUniqueOfRefl {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsRefl α r] [IsRefl β s] [] [] :
r ≃r s

Two reflexive relations on a unique type are isomorphic.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For