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 b → s (self.toFun a) (self.toFun b)

  A RelHom sends related elements to related elements

def «term_→r_» : Lean.TrailingParserDescr

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

• «term_→r_» = Lean.ParserDescr.trailingNode `«term_→r_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →r ") (Lean.ParserDescr.cat `term 26))

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

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 b → s (f a) (f b)

  A RelHomClass sends related elements to related elements

theorem RelHomClass.irrefl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) [Std.Irrefl s] : Std.Irrefl r

theorem RelHomClass.asymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_5} [FunLike F α β] [RelHomClass F r s] (f : F) [Std.Asymm s] : Std.Asymm 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) : WellFounded s → WellFounded r

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) [IsWellFounded β s] : IsWellFounded α r

@[instance_reducible]

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

theorem RelHom.map_rel {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) {a b : α} : r a b → s (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

@[simp]

theorem RelHom.coeFn_mk {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : α → β) (h : ∀ {a b : α}, r a b → s (f a) (f b)) : ⇑{ toFun := f, map_rel' := h } = 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 {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r →r s⦄ (h : ∀ (x : α), f x = g x) : f = g

theorem RelHom.ext_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r →r s} : f = g ↔ ∀ (x : α), f x = g x

def RelHom.id {α : Type u_1} (r : α → α → Prop) : r →r r

Identity map is a relation homomorphism.

Equations

• RelHom.id r = { toFun := fun (x : α) => x, map_rel' := ⋯ }

@[simp]

theorem RelHom.id_apply {α : Type u_1} (r : α → α → Prop) (x : α) : (RelHom.id r) x = 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' := ⋯ }

@[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)

theorem RelHom.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} {u : δ → δ → Prop} (h : r →r s) (g : s →r t) (f : t →r u) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem RelHom.comp_id {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) : f.comp (RelHom.id r) = f

@[simp]

theorem RelHom.id_comp {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) : (RelHom.id s).comp f = f

def RelHom.swap {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) : Function.swap r →r Function.swap s

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

Equations

• f.swap = { toFun := ⇑f, map_rel' := ⋯ }

@[simp]

theorem RelHom.swap_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) (a : α) : f.swap a = f a

def RelHom.swapEquiv {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : r →r s ≃ (Function.swap r →r Function.swap s)

RelHom.swap as an Equiv.

Equations

• RelHom.swapEquiv = { toFun := RelHom.swap, invFun := RelHom.swap, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RelHom.swapEquiv_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : Function.swap r →r Function.swap s) : RelHom.swapEquiv.symm f = f.swap

@[simp]

theorem RelHom.swapEquiv_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) : RelHom.swapEquiv f = f.swap

def RelHom.preimage {α : Type u_1} {β : Type u_2} (f : α → β) (s : β → β → Prop) : f ⁻¹'o s →r s

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

Equations

• RelHom.preimage f s = { toFun := f, map_rel' := ⋯ }

@[simp]

theorem RelHom.preimage_apply {α : Type u_1} {β : Type u_2} (f : α → β) (s : β → β → Prop) (a✝ : α) : (preimage f s) a✝ = f a✝

theorem injective_of_increasing {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Trichotomous r] [Std.Irrefl s] (f : α → β) (hf : ∀ {x y : α}, r x y → s (f x) (f y)) : Function.Injective f

An increasing function is injective

theorem RelHom.injective_of_increasing {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Trichotomous r] [Std.Irrefl s] (f : r →r s) : Function.Injective ⇑f

An increasing function is injective

theorem Function.Surjective.wellFounded_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : α → β} (hf : Surjective f) (o : ∀ {a b : α}, r a b ↔ s (f a) (f b)) : WellFounded r ↔ WellFounded s

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' : 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

def «term_↪r_» : Lean.TrailingParserDescr

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

• «term_↪r_» = Lean.ParserDescr.trailingNode `«term_↪r_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↪r ") (Lean.ParserDescr.cat `term 26))

theorem preimage_equivalence {α : Type u_5} {β : Type u_6} (f : α → β) {s : β → β → Prop} (hs : Equivalence s) : Equivalence (f ⁻¹'o s)

@[reducible]

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' := ⋯ }

@[instance_reducible]

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_reducible]

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

instance RelEmbedding.instEmbeddingLike {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : EmbeddingLike (r ↪r s) α β

@[simp]

theorem RelEmbedding.coe_toEmbedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : r ↪r s} : ⇑f.toEmbedding = ⇑f

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 toEmbedding

@[simp]

theorem RelEmbedding.toEmbedding_inj {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f 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) : Function.Injective ⇑f

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 {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r ↪r s⦄ (h : ∀ (x : α), f x = g x) : f = g

theorem RelEmbedding.ext_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r ↪r s} : f = g ↔ ∀ (x : α), f x = g x

def RelEmbedding.refl {α : Type u_1} (r : α → α → Prop) : r ↪r r

Identity map is a relation embedding.

Equations

• RelEmbedding.refl r = { toEmbedding := Function.Embedding.refl α, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.refl_apply {α : Type u_1} (r : α → α → Prop) (a : α) : (RelEmbedding.refl r) a = a

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' := ⋯ }

@[instance_reducible]

instance RelEmbedding.instInhabited {α : Type u_1} (r : α → α → Prop) : Inhabited (r ↪r r)

Equations

• RelEmbedding.instInhabited r = { default := RelEmbedding.refl r }

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

theorem RelEmbedding.trans_assoc {α : 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 : s ↪r t) (h : t ↪r u) : (f.trans g).trans h = f.trans (g.trans h)

@[simp]

theorem RelEmbedding.trans_refl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) : f.trans (RelEmbedding.refl s) = f

@[simp]

theorem RelEmbedding.refl_trans {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) : (RelEmbedding.refl r).trans f = f

def RelEmbedding.swap {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) : Function.swap r ↪r Function.swap s

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

Equations

• f.swap = { toEmbedding := f.toEmbedding, map_rel_iff' := ⋯ }

def RelEmbedding.swapEquiv {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : r ↪r s ≃ (Function.swap r ↪r Function.swap s)

RelEmbedding.swap as an Equiv

Equations

• RelEmbedding.swapEquiv = { toFun := RelEmbedding.swap, invFun := RelEmbedding.swap, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RelEmbedding.swapEquiv_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : Function.swap r ↪r Function.swap s) : swapEquiv.symm f = f.swap

@[simp]

theorem RelEmbedding.swapEquiv_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) : swapEquiv f = f.swap

@[simp]

theorem RelEmbedding.swap_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (a : α) : f.swap a = f a

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

• RelEmbedding.preimage f s = { toEmbedding := f, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.preimage_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : β → β → Prop) (a : α) : (preimage f s) a = f a

theorem RelEmbedding.eq_preimage {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) : r = ⇑f ⁻¹'o s

theorem RelEmbedding.irrefl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Irrefl s] : Std.Irrefl r

theorem RelEmbedding.stdRefl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Refl s] : Std.Refl r

theorem RelEmbedding.symm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Symm s] : Std.Symm r

theorem RelEmbedding.asymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Asymm s] : Std.Asymm r

theorem RelEmbedding.antisymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : ∀ (x : r ↪r s) [Std.Antisymm s], Std.Antisymm r

theorem RelEmbedding.isTrans {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : ∀ (x : r ↪r s) [IsTrans β s], IsTrans α r

theorem RelEmbedding.total {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : ∀ (x : r ↪r s) [Std.Total s], Std.Total r

theorem RelEmbedding.isPreorder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : ∀ (x : r ↪r s) [IsPreorder β s], IsPreorder α r

theorem RelEmbedding.isPartialOrder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : ∀ (x : r ↪r s) [IsPartialOrder β s], IsPartialOrder α r

theorem RelEmbedding.isLinearOrder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : ∀ (x : r ↪r s) [IsLinearOrder β s], IsLinearOrder α r

theorem RelEmbedding.isStrictOrder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : ∀ (x : r ↪r s) [IsStrictOrder β s], IsStrictOrder α r

theorem RelEmbedding.trichotomous {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : ∀ (x : r ↪r s) [Std.Trichotomous s], Std.Trichotomous r

theorem RelEmbedding.isStrictTotalOrder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : ∀ (x : r ↪r s) [IsStrictTotalOrder β s], IsStrictTotalOrder α r

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} : ∀ (x : r ↪r s), WellFounded s → WellFounded r

theorem RelEmbedding.isWellFounded {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [IsWellFounded β s] : IsWellFounded α r

theorem RelEmbedding.isWellOrder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : ∀ (x : r ↪r s) [IsWellOrder β s], IsWellOrder α r

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

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

Equations

• Subtype.relEmbedding r p = { toEmbedding := Function.Embedding.subtype p, map_rel_iff' := ⋯ }

@[simp]

theorem Subtype.relEmbedding_apply {X : Type u_5} (r : X → X → Prop) (p : X → Prop) (self : Subtype p) : (relEmbedding r p) self = ↑self

instance Subtype.wellFoundedLT {α : Type u_1} [LT α] [WellFoundedLT α] (p : α → Prop) : WellFoundedLT (Subtype p)

instance Subtype.wellFoundedGT {α : Type u_1} [LT α] [WellFoundedGT α] (p : α → Prop) : WellFoundedGT (Subtype p)

def Quotient.mkRelHom {α : Type u_1} {x✝ : 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 as a relation homomorphism between the relation and the lift of a relation.

Equations

• Quotient.mkRelHom H = { toFun := Quotient.mk x✝, map_rel' := ⋯ }

@[simp]

theorem Quotient.mkRelHom_apply {α : Type u_1} {x✝ : Setoid α} {r : α → α → Prop} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) (a : α) : (mkRelHom H) a = ⟦a⟧

noncomputable def Quotient.outRelEmbedding {α : Type u_1} {x✝ : Setoid α} {r : α → α → Prop} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) : Quotient.lift₂ r H ↪r r

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

Equations

• Quotient.outRelEmbedding H = { toEmbedding := Function.Embedding.quotientOut α, map_rel_iff' := ⋯ }

@[simp]

theorem Quotient.outRelEmbedding_apply {α : Type u_1} {x✝ : Setoid α} {r : α → α → Prop} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) (a✝ : Quotient x✝) : (outRelEmbedding H) a✝ = a✝.out

@[simp]

theorem acc_lift₂_iff {α : Type u_1} {x✝ : 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

@[simp]

theorem acc_liftOn₂'_iff {α : Type u_1} {s : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ a₂ b₁ b₂ : α), s a₁ b₁ → s a₂ b₂ → r a₁ a₂ = r b₁ b₂} {a : α} : Acc (fun (x y : Quotient s) => x.liftOn₂' y r H) (Quotient.mk'' a) ↔ Acc r a

@[simp]

theorem wellFounded_lift₂_iff {α : Type u_1} {x✝ : 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

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

theorem WellFounded.quotient_lift₂ {α : Type u_1} {x✝ : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} : WellFounded r → WellFounded (Quotient.lift₂ r H)

Alias of the reverse direction of wellFounded_lift₂_iff.

---

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

theorem WellFounded.of_quotient_lift₂ {α : Type u_1} {x✝ : 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

Alias of the forward 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 : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ a₂ b₁ b₂ : α), s a₁ b₁ → s a₂ b₂ → r a₁ a₂ = r b₁ b₂} : (WellFounded fun (x y : Quotient s) => x.liftOn₂' y r H) ↔ WellFounded r

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

Alias of the reverse direction of wellFounded_liftOn₂'_iff.

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

Alias of the forward direction of wellFounded_liftOn₂'_iff.

def RelEmbedding.ofMapRelIff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : α → β) [Std.Antisymm r] [Std.Refl 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

• RelEmbedding.ofMapRelIff f hf = { toFun := f, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.ofMapRelIff_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : α → β) [Std.Antisymm r] [Std.Refl s] (hf : ∀ (a b : α), s (f a) (f b) ↔ r a b) : ⇑(ofMapRelIff f hf) = f

def RelEmbedding.ofMonotone {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Trichotomous r] [Std.Asymm s] (f : α → β) (H : ∀ (a b : α), r a b → s (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

• RelEmbedding.ofMonotone f H = { toFun := f, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.ofMonotone_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Trichotomous r] [Std.Asymm s] (f : α → β) (H : ∀ (a b : α), r a b → s (f a) (f b)) : ⇑(ofMonotone f H) = f

def RelEmbedding.ofIsEmpty {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] : r ↪r s

A relation embedding from an empty type.

Equations

• RelEmbedding.ofIsEmpty r s = { toEmbedding := Function.Embedding.ofIsEmpty, map_rel_iff' := ⋯ }

def RelEmbedding.sumLiftRelInl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) : r ↪r Sum.LiftRel r s

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

Equations

• RelEmbedding.sumLiftRelInl r s = { toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.sumLiftRelInl_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (val : α) : (sumLiftRelInl r s) val = Sum.inl val

def RelEmbedding.sumLiftRelInr {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) : s ↪r Sum.LiftRel r s

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

Equations

• RelEmbedding.sumLiftRelInr r s = { toFun := Sum.inr, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.sumLiftRelInr_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (val : β) : (sumLiftRelInr r s) val = Sum.inr val

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.LiftRel r t ↪r Sum.LiftRel s u

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

Equations

• f.sumLiftRelMap g = { toFun := Sum.map ⇑f ⇑g, inj' := ⋯, map_rel_iff' := ⋯ }

@[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.sumLexInl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) : r ↪r Sum.Lex r s

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

Equations

• RelEmbedding.sumLexInl r s = { toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.sumLexInl_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (val : α) : (sumLexInl r s) val = Sum.inl val

def RelEmbedding.sumLexInr {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) : s ↪r Sum.Lex r s

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

Equations

• RelEmbedding.sumLexInr r s = { toFun := Sum.inr, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.sumLexInr_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (val : β) : (sumLexInr r s) val = Sum.inr val

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.Lex r t ↪r Sum.Lex s u

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

Equations

• f.sumLexMap g = { toFun := Sum.map ⇑f ⇑g, inj' := ⋯, map_rel_iff' := ⋯ }

@[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.prodLexMkLeft {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (s : β → β → Prop) {a : α} (h : ¬r a a) : s ↪r Prod.Lex r s

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

Equations

• RelEmbedding.prodLexMkLeft s h = { toFun := Prod.mk a, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.prodLexMkLeft_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (s : β → β → Prop) {a : α} (h : ¬r a a) (snd : β) : (prodLexMkLeft s h) snd = (a, snd)

def RelEmbedding.prodLexMkRight {α : Type u_1} {β : Type u_2} {s : β → β → Prop} (r : α → α → Prop) {b : β} (h : ¬s b b) : r ↪r Prod.Lex r s

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

Equations

• RelEmbedding.prodLexMkRight r h = { toFun := fun (a : α) => (a, b), inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.prodLexMkRight_apply {α : Type u_1} {β : Type u_2} {s : β → β → Prop} (r : α → α → Prop) {b : β} (h : ¬s b b) (a : α) : (prodLexMkRight r h) a = (a, b)

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.Lex r t ↪r Prod.Lex s u

Prod.map as a relation embedding.

Equations

• f.prodLexMap g = { toFun := Prod.map ⇑f ⇑g, inj' := ⋯, map_rel_iff' := ⋯ }

@[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✝

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

def «term_≃r_» : Lean.TrailingParserDescr

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

Equations

• «term_≃r_» = Lean.ParserDescr.trailingNode `«term_≃r_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃r ") (Lean.ParserDescr.cat `term 26))

@[reducible]

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' := ⋯ }

theorem RelIso.toEquiv_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : Function.Injective toEquiv

@[instance_reducible]

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_reducible]

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

@[instance_reducible]

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' := ⋯ }

theorem RelIso.coe_toRelEmbedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) : ⇑f.toRelEmbedding = ⇑f

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 {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r ≃r s⦄ (h : ∀ (x : α), f x = g x) : f = g

theorem RelIso.ext_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r ≃r s} : f = g ↔ ∀ (x : α), f x = g x

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' := ⋯ }

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

• RelIso.Simps.apply h = ⇑h

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

• RelIso.Simps.symm_apply h = ⇑h.symm

def RelIso.refl {α : Type u_1} (r : α → α → Prop) : r ≃r r

Identity map is a relation isomorphism.

Equations

• RelIso.refl r = { toEquiv := Equiv.refl α, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.refl_apply {α : Type u_1} (r : α → α → Prop) (a : α) : (RelIso.refl r) a = 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' := ⋯ }

@[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✝)

@[instance_reducible]

instance RelIso.instInhabited {α : Type u_1} (r : α → α → Prop) : Inhabited (r ≃r r)

Equations

• RelIso.instInhabited r = { default := RelIso.refl r }

@[simp]

theorem RelIso.default_def {α : Type u_1} (r : α → α → Prop) : default = RelIso.refl r

@[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

@[simp]

theorem RelIso.symm_comp_self {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : ⇑e.symm ∘ ⇑e = id

@[simp]

theorem RelIso.self_comp_symm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : ⇑e ∘ ⇑e.symm = id

@[simp]

theorem RelIso.symm_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).symm a = f.symm (g.symm a)

theorem RelIso.symm_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (b : α) : f.symm.symm b = f b

theorem RelIso.apply_eq_iff_eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {x y : α} : f x = f y ↔ x = y

theorem RelIso.symm_apply_eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {x : β} {y : α} : e.symm x = y ↔ x = e y

theorem RelIso.eq_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {x : β} {y : α} : y = e.symm x ↔ e y = x

@[deprecated RelIso.eq_symm_apply (since := "2026-07-26")]

theorem RelIso.apply_eq_iff_eq_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {x : α} {y : β} (f : r ≃r s) : f x = y ↔ x = f.symm y

@[simp]

theorem RelIso.symm_symm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : e.symm.symm = e

theorem RelIso.symm_bijective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : Function.Bijective RelIso.symm

@[simp]

theorem RelIso.refl_symm {α : Type u_1} {r : α → α → Prop} : (RelIso.refl r).symm = RelIso.refl r

@[simp]

theorem RelIso.trans_refl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : e.trans (RelIso.refl s) = e

@[simp]

theorem RelIso.refl_trans {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : (RelIso.refl r).trans e = e

@[simp]

theorem RelIso.symm_trans_self {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : e.symm.trans e = RelIso.refl s

@[simp]

theorem RelIso.self_trans_symm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : e.trans e.symm = RelIso.refl r

theorem RelIso.trans_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} {δ : Type u_5} {u : δ → δ → Prop} (ab : r ≃r s) (bc : s ≃r t) (cd : t ≃r u) : (ab.trans bc).trans cd = ab.trans (bc.trans cd)

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

A relation isomorphism between equal relations on equal types.

Equations

• RelIso.cast h₁ h₂ = { toEquiv := Equiv.cast h₁, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.cast_toEquiv {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} (h₁ : α = β) (h₂ : r ≍ s) : (RelIso.cast h₁ h₂).toEquiv = Equiv.cast h₁

@[simp]

theorem RelIso.cast_apply {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} (h₁ : α = β) (h₂ : r ≍ s) (a : α) : (RelIso.cast h₁ h₂) a = cast h₁ a

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

theorem RelIso.cast_refl {α : Type u} {r : α → α → Prop} (h₁ : α = α := ⋯) (h₂ : r ≍ r := ⋯) : RelIso.cast h₁ h₂ = RelIso.refl r

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

def RelIso.swap {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) : Function.swap r ≃r Function.swap s

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

Equations

• f.swap = { toEquiv := ↑f, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.swap_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a : α) : f.swap a = f a

@[simp]

theorem RelIso.swap_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a✝ : β) : f.swap.symm a✝ = EquivLike.inv f a✝

def RelIso.swapEquiv {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : r ≃r s ≃ (Function.swap r ≃r Function.swap s)

RelIso.swap as an Equiv.

Equations

• RelIso.swapEquiv = { toFun := RelIso.swap, invFun := RelIso.swap, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RelIso.swapEquiv_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : Function.swap r ≃r Function.swap s) : swapEquiv.symm f = f.swap

@[simp]

theorem RelIso.swapEquiv_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) : swapEquiv f = f.swap

def RelIso.compl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) : rᶜ ≃r sᶜ

A relation isomorphism is also a relation isomorphism between complemented relations.

Equations

• f.compl = { toEquiv := ↑f, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.compl_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a : α) : f.compl a = f a

@[simp]

theorem RelIso.compl_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a✝ : β) : f.compl.symm a✝ = EquivLike.inv f a✝

def RelIso.complEquiv {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : r ≃r s ≃ (rᶜ ≃r sᶜ)

RelIso.compl as an Equiv.

Equations

• RelIso.complEquiv = { toFun := RelIso.compl, invFun := fun (f : rᶜ ≃r sᶜ) => { toEquiv := ↑f, map_rel_iff' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RelIso.complEquiv_apply_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a : α) : (complEquiv f) a = f a

@[simp]

theorem RelIso.complEquiv_symm_apply_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : rᶜ ≃r sᶜ) (a : α) : (complEquiv.symm f) a = f a

@[simp]

theorem RelIso.complEquiv_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : rᶜ ≃r sᶜ) (a✝ : β) : (complEquiv.symm f).symm a✝ = EquivLike.inv f a✝

@[simp]

theorem RelIso.complEquiv_apply_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a✝ : β) : (complEquiv f).symm a✝ = EquivLike.inv f a✝

@[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

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)

theorem RelIso.bijective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : Function.Bijective ⇑e

theorem RelIso.injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : Function.Injective ⇑e

theorem RelIso.surjective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : Function.Surjective ⇑e

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.copy {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (f : α → β) (g : β → α) (hf : f = ⇑e) (hg : g = ⇑e.symm) : r ≃r s

Copy of a RelIso with a new toFun and invFun equal to the old ones. Useful to fix definitional equalities.

Equations

• e.copy f g hf hg = { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.coe_copy {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (f : α → β) (g : β → α) (hf : f = ⇑e) (hg : g = ⇑e.symm) : ⇑(e.copy f g hf hg) = f

theorem RelIso.copy_eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (f : α → β) (g : β → α) (hf : f = ⇑e) (hg : g = ⇑e.symm) : e.copy f g hf hg = e

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

• RelIso.preimage f s = { toEquiv := f, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.preimage_apply {α : Type u_1} {β : Type u_2} (f : α ≃ β) (s : β → β → Prop) (a : α) : (RelIso.preimage f s) a = f a

@[simp]

theorem RelIso.preimage_symm_apply {α : Type u_1} {β : Type u_2} (f : α ≃ β) (s : β → β → Prop) (a : β) : (RelIso.preimage f s).symm a = f.symm a

instance RelIso.IsWellOrder.preimage {β : Type u_2} {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) : IsWellOrder β (⇑f ⁻¹'o r)

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

noncomputable def RelIso.ofSurjective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (H : Function.Surjective ⇑f) : r ≃r s

A surjective relation embedding is a relation isomorphism.

Equations

• RelIso.ofSurjective f H = { toEquiv := f.equivOfSurjective H, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.ofSurjective_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (H : Function.Surjective ⇑f) (a : α) : (ofSurjective f H) a = f a

noncomputable def RelIso.embeddingSurjectiveEquivIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : { f : r ↪r s // Function.Surjective ⇑f } ≃ (r ≃r s)

Surjective relation embeddings are equivalent to relation isomorphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RelIso.embeddingSurjectiveEquivIso_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : { f : r ↪r s // Function.Surjective ⇑f }) : embeddingSurjectiveEquivIso f = ofSurjective ↑f ⋯

@[simp]

theorem RelIso.embeddingSurjectiveEquivIso_symm_apply_coe_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a : α) : ↑(embeddingSurjectiveEquivIso.symm f) a = f.toEquiv a

def RelIso.relHomCongr {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) : r₁ →r s₁ ≃ (r₂ →r s₂)

Transport a RelHom across a pair of RelIsos, by pre- and post-composition.

This is Equiv.arrowCongr for RelHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RelIso.relHomCongr_symm_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ →r s₂) : (e₁.relHomCongr e₂).symm f₂ = e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom)

@[simp]

theorem RelIso.relHomCongr_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ →r s₁) : (e₁.relHomCongr e₂) f₁ = e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom)

theorem RelIso.relHomCongr_symm_apply_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ →r s₂) (x : α₁) : ((e₁.relHomCongr e₂).symm f₂) x = e₂.symm (f₂ (e₁ x))

theorem RelIso.relHomCongr_apply_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ →r s₁) (x : α₂) : ((e₁.relHomCongr e₂) f₁) x = e₂ (f₁ (e₁.symm x))

def RelIso.relEmbeddingCongr {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) : r₁ ↪r s₁ ≃ (r₂ ↪r s₂)

Transport a RelEmbedding across a pair of RelIsos, by pre- and post-composition.

This is Equiv.embeddingCongr for RelEmbedding.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RelIso.relEmbeddingCongr_symm_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ ↪r s₂) : (e₁.relEmbeddingCongr e₂).symm f₂ = (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding

@[simp]

theorem RelIso.relEmbeddingCongr_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ ↪r s₁) : (e₁.relEmbeddingCongr e₂) f₁ = (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding

theorem RelIso.relEmbeddingCongr_symm_apply_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ ↪r s₂) (a✝ : α₁) : ((e₁.relEmbeddingCongr e₂).symm f₂) a✝ = e₂.symm (f₂ (e₁ a✝))

theorem RelIso.relEmbeddingCongr_apply_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ ↪r s₁) (a✝ : α₂) : ((e₁.relEmbeddingCongr e₂) f₁) a✝ = e₂ (f₁ (e₁.symm a✝))

def RelIso.relIsoCongr {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) : r₁ ≃r s₁ ≃ (r₂ ≃r s₂)

Transport a RelIso across a pair of RelIsos, by pre- and post-composition.

This is Equiv.equivCongr for RelIso.

Equations

• e₁.relIsoCongr e₂ = { toFun := fun (f₁ : r₁ ≃r s₁) => (e₁.symm.trans f₁).trans e₂, invFun := fun (f₂ : r₂ ≃r s₂) => (e₁.trans f₂).trans e₂.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RelIso.relIsoCongr_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ ≃r s₁) : (e₁.relIsoCongr e₂) f₁ = (e₁.symm.trans f₁).trans e₂

@[simp]

theorem RelIso.relIsoCongr_symm_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ ≃r s₂) : (e₁.relIsoCongr e₂).symm f₂ = (e₁.trans f₂).trans e₂.symm

theorem RelIso.relIsoCongr_apply_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ ≃r s₁) (a✝ : α₂) : ((e₁.relIsoCongr e₂) f₁) a✝ = e₂ (f₁ (e₁.symm a✝))

theorem RelIso.relIsoCongr_symm_apply_apply {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop} {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ ≃r s₂) (a✝ : α₁) : ((e₁.relIsoCongr e₂).symm f₂) a✝ = e₂.symm (f₂ (e₁ a✝))

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' := ⋯ }

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' := ⋯ }

def RelIso.relIsoOfIsEmpty {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] [IsEmpty β] : r ≃r s

Two relations on empty types are isomorphic.

Equations

• RelIso.relIsoOfIsEmpty r s = { toEquiv := Equiv.equivOfIsEmpty α β, map_rel_iff' := ⋯ }

def RelIso.sumLexEmpty {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsEmpty β] : Sum.Lex r s ≃r r

The lexicographic sum of r plus an empty relation is isomorphic to r.

Equations

• RelIso.sumLexEmpty r s = { toEquiv := Equiv.sumEmpty α β, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.sumLexEmpty_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsEmpty β] (a✝ : α ⊕ β) : (sumLexEmpty r s) a✝ = Sum.elim id (fun (a : β) => isEmptyElim a) a✝

@[simp]

theorem RelIso.sumLexEmpty_symm_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsEmpty β] (val : α) : (sumLexEmpty r s).symm val = Sum.inl val

def RelIso.emptySumLex {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] : Sum.Lex r s ≃r s

The lexicographic sum of an empty relation plus s is isomorphic to s.

Equations

• RelIso.emptySumLex r s = { toEquiv := Equiv.emptySum α β, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.emptySumLex_symm_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] (a✝ : β) : (emptySumLex r s).symm a✝ = Sum.inr a✝

@[simp]

theorem RelIso.emptySumLex_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] (a✝ : α ⊕ β) : (emptySumLex r s) a✝ = (Equiv.sumEmpty β α) a✝.swap

def RelIso.ofUniqueOfIrrefl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Irrefl r] [Std.Irrefl s] [Unique α] [Unique β] : r ≃r s

Two irreflexive relations on a unique type are isomorphic.

Equations

• RelIso.ofUniqueOfIrrefl r s = { toEquiv := Equiv.ofUnique α β, map_rel_iff' := ⋯ }

def RelIso.ofUniqueOfRefl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Refl r] [Std.Refl s] [Unique α] [Unique β] : r ≃r s

Two reflexive relations on a unique type are isomorphic.

Equations

• RelIso.ofUniqueOfRefl r s = { toEquiv := Equiv.ofUnique α β, map_rel_iff' := ⋯ }

def RelHom.toMap {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α → β) : r →r Relation.Map r f f

A function f : α → β induces a relation homomorphism from an α-relation r to Relation.Map r f f.

Equations

• RelHom.toMap r f = { toFun := f, map_rel' := ⋯ }

@[simp]

theorem RelHom.coe_toMap {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α → β) : ⇑(toMap r f) = f

def RelEmbedding.toMap {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ↪ β) : r ↪r Relation.Map r ⇑f ⇑f

An embedding f : α ↪ β induces a relation embedding from an α-relation r to Relation.Map r f f.

Equations

• RelEmbedding.toMap r f = { toEmbedding := f, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.coe_toMap {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ↪ β) : ⇑(toMap r f) = ⇑f

def RelIso.toMap {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ≃ β) : r ≃r Relation.Map r ⇑f ⇑f

An equivalence f : α ≃ β induces a relation isomorphism from an α-relation r to Relation.Map r f f.

Equations

• RelIso.toMap r f = { toEquiv := f, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.coe_toMap {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ≃ β) : ⇑(toMap r f) = ⇑f

@[simp]

theorem RelIso.toEquiv_toMap {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ≃ β) : ↑(toMap r f) = f

@[simp]

theorem RelIso.coe_symm_toMap {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ≃ β) : ⇑(toMap r f).symm = ⇑f.symm

@[simp]

theorem RelIso.toEquiv_symm_toMap {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ≃ β) : ↑(toMap r f).symm = f.symm

def RelHom.ofOnFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α → β) : Function.onFun r f →r r

For a β-relation r, a function f : α → β induces a relation homomorphism from r.onFun f to r.

Equations

• RelHom.ofOnFun r f = { toFun := f, map_rel' := ⋯ }

@[simp]

theorem RelHom.coe_ofOnFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α → β) : ⇑(ofOnFun r f) = f

def RelEmbedding.ofOnFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ↪ β) : Function.onFun r ⇑f ↪r r

For a β-relation r, an embedding f : α ↪ β induces a relation embedding from r.onFun f to r.

Equations

• RelEmbedding.ofOnFun r f = { toEmbedding := f, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.coe_ofOnFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ↪ β) : ⇑(ofOnFun r f) = ⇑f

def RelIso.ofOnFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ≃ β) : Function.onFun r ⇑f ≃r r

For a β-relation r, an equivalence f : α ≃ β induces a relation isomorphism from r.onFun f to r.

Equations

• RelIso.ofOnFun r f = { toEquiv := f, map_rel_iff' := ⋯ }

@[simp]

theorem RelIso.coe_ofOnFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ≃ β) : ⇑(ofOnFun r f) = ⇑f

@[simp]

theorem RelIso.toEquiv_ofOnFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ≃ β) : ↑(ofOnFun r f) = f

@[simp]

theorem RelIso.coe_symm_ofOnFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ≃ β) : ⇑(ofOnFun r f).symm = ⇑f.symm

@[simp]

theorem RelIso.toEquiv_symm_ofOnFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ≃ β) : ↑(ofOnFun r f).symm = f.symm