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)→ 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)↔ 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)↔ 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→r: RelHom
• ↪r↪r: RelEmbedding
• ≃r≃r: RelIso

ink

structure RelHom {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) : Type (maxu_1u_2)

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

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

ink

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

ink

class RelHomClass (F : Type u_1) {α : outParam (Type u_2)} {β : outParam (Type u_3)} (r : outParam (α → α → Prop)) (s : outParam (β → β → Prop)) extends FunLike : Type (max(maxu_1u_2)u_3)

• A RelHomClass sends related elements to related elements

  map_rel : (f : F) → {a b : α} → r a b → s (↑f a) (↑f b)

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

ink

theorem RelHomClass.isIrrefl {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_1} [inst : RelHomClass F r s] (f : F) [inst : IsIrrefl β s] : IsIrrefl α r

ink

theorem RelHomClass.isAsymm {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_1} [inst : RelHomClass F r s] (f : F) [inst : IsAsymm β s] : IsAsymm α r

ink

theorem RelHomClass.acc {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_1} [inst : RelHomClass F r s] (f : F) (a : α) : Acc s (↑f a) → Acc r a

ink

theorem RelHomClass.wellFounded {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_1} [inst : RelHomClass F r s] (f : F) : WellFounded s → WellFounded r

ink

instance RelHom.instRelHomClassRelHom {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : RelHomClass (r →r s) r s

Equations

• RelHom.instRelHomClassRelHom = RelHomClass.mk RelHom.map_rel'

ink

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)

ink

@[simp]

theorem RelHom.coe_fn_toFun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) : f.toFun = ↑f

ink

theorem RelHom.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : Function.Injective fun f => ↑f

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

ink

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

ink

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

ink

@[simp]

theorem RelHom.id_apply {α : Type u_1} (r : α → α → Prop) (x : α) : ↑(RelHom.id r) x = x

ink

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' := @RelHom.id.proof_1 α r }

ink

@[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 : α) : ↑(RelHom.comp g f) x = ↑g (↑f x)

ink

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

• RelHom.comp g f = { toFun := fun x => ↑g (↑f x), map_rel' := @RelHom.comp.proof_1 α β γ r s t g f }

ink

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

• RelHom.swap f = { toFun := ↑f, map_rel' := @RelHom.swap.proof_1 α β r s f }

ink

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' := (_ : ∀ {a b : α}, (f ⁻¹'o s) a b → (f ⁻¹'o s) a b) }

ink

theorem injective_of_increasing {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsTrichotomous α r] [inst : IsIrrefl β s] (f : α → β) (hf : {x y : α} → r x y → s (f x) (f y)) : Function.Injective f

An increasing function is injective

ink

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

An increasing function is injective

ink

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

ink

structure RelEmbedding {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) extends Function.Embedding : Type (maxu_1u_2)

• Elements are related iff they are related after apply a RelEmbedding

  map_rel_iff' : ∀ {a b : α}, s (↑toEmbedding a) (↑toEmbedding b) ↔ r a b

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

ink

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

ink

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

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

Equations

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

ink

theorem preimage_equivalence {α : Sort u_1} {β : Sort u_2} (f : α → β) {s : β → β → Prop} (hs : Equivalence s) : Equivalence (f ⁻¹'o s)

ink

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

• RelEmbedding.toRelHom f = { toFun := f.toEmbedding.toFun, map_rel' := @RelEmbedding.toRelHom.proof_1 α β r s f }

ink

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

Equations

• RelEmbedding.instCoeRelEmbeddingRelHom = { coe := RelEmbedding.toRelHom }

ink

instance RelEmbedding.instCoeFunRelEmbeddingForAll {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : CoeFun (r ↪r s) fun x => α → β

Equations

• RelEmbedding.instCoeFunRelEmbeddingForAll = { coe := fun o => ↑o.toEmbedding }

ink

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

Equations

• RelEmbedding.instRelHomClassRelEmbedding = RelHomClass.mk RelEmbedding.instRelHomClassRelEmbedding.proof_2

ink

def RelEmbedding.Simps.apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (h : r ↪r s) : α → β

See Note [custom simps projection]. We specify this explicitly because we have a coercion not given by the FunLike instance. Todo: remove that instance?

Equations

• RelEmbedding.Simps.apply h = ↑h.toEmbedding

ink

theorem RelEmbedding.injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) : Function.Injective ↑f.toEmbedding

ink

theorem RelEmbedding.inj {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a : α} {b : α} : ↑f.toEmbedding a = ↑f.toEmbedding b ↔ a = b

ink

theorem RelEmbedding.map_rel_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a : α} {b : α} : s (↑f.toEmbedding a) (↑f.toEmbedding b) ↔ r a b

ink

theorem RelEmbedding.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : Function.Injective fun f => ↑f.toEmbedding

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

ink

theorem RelEmbedding.ext {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f : r ↪r s⦄ ⦃g : r ↪r s⦄ (h : ∀ (x : α), ↑f.toEmbedding x = ↑g.toEmbedding x) : f = g

ink

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.toEmbedding x = ↑g.toEmbedding x

ink

@[simp]

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

ink

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

Identity map is a relation embedding.

Equations

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

ink

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

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

ink

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

Equations

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

ink

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 : α) : ↑(RelEmbedding.trans f g).toEmbedding a = ↑g.toEmbedding (↑f.toEmbedding a)

ink

@[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) : ↑(RelEmbedding.trans f g).toEmbedding = ↑g.toEmbedding ∘ ↑f.toEmbedding

ink

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

• RelEmbedding.swap f = { toEmbedding := f.toEmbedding, map_rel_iff' := (_ : ∀ {a b : α}, s (↑f.toEmbedding b) (↑f.toEmbedding a) ↔ r b a) }

ink

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' := (_ : ∀ {a b : α}, s (↑f a) (↑f b) ↔ s (↑f a) (↑f b)) }

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem RelEmbedding.isAntisymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : r ↪r s → ∀ [inst : IsAntisymm β s], IsAntisymm α r

ink

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

ink

theorem RelEmbedding.isTotal {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : r ↪r s → ∀ [inst : IsTotal β s], IsTotal α r

ink

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

ink

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

ink

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

ink

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

ink

theorem RelEmbedding.isTrichotomous {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : r ↪r s → ∀ [inst : IsTrichotomous β s], IsTrichotomous α r

ink

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

ink

theorem RelEmbedding.acc {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (a : α) : Acc s (↑f.toEmbedding a) → Acc r a

ink

theorem RelEmbedding.wellFounded {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : r ↪r s → WellFounded s → WellFounded r

ink

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

ink

@[simp]

theorem Quotient.outRelEmbedding_apply {α : Type u_1} [s : Setoid α] {r : α → α → Prop} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) : ∀ (a : Quotient s), ↑(Quotient.outRelEmbedding H).toEmbedding a = Quotient.out a

ink

noncomputable def Quotient.outRelEmbedding {α : Type u_1} [s : 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

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

ink

@[simp]

theorem wellFounded_lift₂_iff {α : Type u_1} [s : 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.

ink

theorem RelEmbedding.WellFounded.quotient_lift₂ {α : Type u_1} [s : 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.

ink

theorem RelEmbedding.WellFounded.of_quotient_lift₂ {α : Type u_1} [s : 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.

ink

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

To define an 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↔ r a b.

Equations

• RelEmbedding.ofMapRelIff f hf = { toEmbedding := { toFun := f, inj' := (_ : ∀ (x x_1 : α), f x = f x_1 → x = x_1) }, map_rel_iff' := (_ : ∀ {a b : α}, s (f a) (f b) ↔ r a b) }

ink

@[simp]

theorem RelEmbedding.ofMapRelIff_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : α → β) [inst : IsAntisymm α r] [inst : IsRefl β s] (hf : ∀ (a b : α), s (f a) (f b) ↔ r a b) : ↑(RelEmbedding.ofMapRelIff f hf).toEmbedding = f

ink

def RelEmbedding.ofMonotone {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrichotomous α r] [inst : IsAsymm β 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

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

ink

@[simp]

theorem RelEmbedding.ofMonotone_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrichotomous α r] [inst : IsAsymm β s] (f : α → β) (H : (a b : α) → r a b → s (f a) (f b)) : ↑(RelEmbedding.ofMonotone f H).toEmbedding = f

ink

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

A relation embedding from an empty type.

Equations

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

ink

@[simp]

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

ink

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

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

ink

@[simp]

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

ink

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

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

ink

@[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 : α ⊕ γ), ↑(RelEmbedding.sumLiftRelMap f g).toEmbedding a = Sum.map (↑f.toEmbedding) (↑g.toEmbedding) a

ink

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

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

ink

@[simp]

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

ink

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 = { toEmbedding := { toFun := Sum.inl, inj' := (_ : Function.Injective Sum.inl) }, map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }

ink

@[simp]

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

ink

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 = { toEmbedding := { toFun := Sum.inr, inj' := (_ : Function.Injective Sum.inr) }, map_rel_iff' := (_ : ∀ {a b : β}, Sum.Lex r s (Sum.inr a) (Sum.inr b) ↔ s a b) }

ink

@[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 : α ⊕ γ), ↑(RelEmbedding.sumLexMap f g).toEmbedding a = Sum.map (↑f.toEmbedding) (↑g.toEmbedding) a

ink

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

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

ink

@[simp]

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

ink

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

λ b, Prod.mk a b as a relation embedding.

Equations

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

ink

@[simp]

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

ink

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

λ a, Prod.mk a b as a relation embedding.

Equations

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

ink

@[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 : α × γ), ↑(RelEmbedding.prodLexMap f g).toEmbedding a = Prod.map (↑f.toEmbedding) (↑g.toEmbedding) a

ink

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

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

ink

structure RelIso {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) extends Equiv : Type (maxu_1u_2)

• Elements are related iff they are related after apply a RelIso

  map_rel_iff' : ∀ {a b : α}, s (↑toEquiv a) (↑toEquiv b) ↔ r a b

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

ink

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

ink

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

Convert an 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

• RelIso.toRelEmbedding f = { toEmbedding := Equiv.toEmbedding f.toEquiv, map_rel_iff' := (_ : ∀ {a b : α}, s (↑f.toEquiv a) (↑f.toEquiv b) ↔ r a b) }

ink

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

ink

instance RelIso.instCoeOutRelIsoRelEmbedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : CoeOut (r ≃r s) (r ↪r s)

Equations

• RelIso.instCoeOutRelIsoRelEmbedding = { coe := RelIso.toRelEmbedding }

ink

instance RelIso.instCoeFunRelIsoForAll {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : CoeFun (r ≃r s) fun x => α → β

Equations

• RelIso.instCoeFunRelIsoForAll = { coe := fun f => ↑(RelIso.toRelEmbedding f).toEmbedding }

ink

instance RelIso.instRelHomClassRelIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : RelHomClass (r ≃r s) r s

Equations

• RelIso.instRelHomClassRelIso = RelHomClass.mk RelIso.instRelHomClassRelIso.proof_2

ink

theorem RelIso.map_rel_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {a : α} {b : α} : s (↑(RelIso.toRelEmbedding f).toEmbedding a) (↑(RelIso.toRelEmbedding f).toEmbedding b) ↔ r a b

ink

@[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) : ↑(RelIso.toRelEmbedding { toEquiv := f, map_rel_iff' := o }).toEmbedding = ↑f

ink

@[simp]

theorem RelIso.coe_fn_toEquiv {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) : ↑f.toEquiv = ↑(RelIso.toRelEmbedding f).toEmbedding

ink

theorem RelIso.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : Function.Injective fun f => ↑(RelIso.toRelEmbedding f).toEmbedding

The map coe_fn : (r ≃r s) → (α → β)≃r s) → (α → β)→ (α → β)→ β) is injective. Lean fails to parse function.injective (λ e : r ≃r s, (e : α → β))≃r s, (e : α → β))→ β)), so we use a trick to say the same.

ink

theorem RelIso.ext {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f : r ≃r s⦄ ⦃g : r ≃r s⦄ (h : ∀ (x : α), ↑(RelIso.toRelEmbedding f).toEmbedding x = ↑(RelIso.toRelEmbedding g).toEmbedding x) : f = g

ink

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 : α), ↑(RelIso.toRelEmbedding f).toEmbedding x = ↑(RelIso.toRelEmbedding g).toEmbedding x

ink

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

• RelIso.symm f = { toEquiv := Equiv.symm f.toEquiv, map_rel_iff' := (_ : ∀ (a b : β), r (↑(Equiv.symm f.toEquiv) a) (↑(Equiv.symm f.toEquiv) b) ↔ s a b) }

ink

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

Equations

• RelIso.Simps.apply h = ↑(RelIso.toRelEmbedding h).toEmbedding

ink

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 = ↑(RelIso.toRelEmbedding (RelIso.symm h)).toEmbedding

ink

@[simp]

theorem RelIso.refl_apply {α : Type u_1} (r : α → α → Prop) (a : α) : ↑(RelIso.toRelEmbedding (RelIso.refl r)).toEmbedding a = a

ink

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' := (_ : ∀ {a b : α}, r (↑(Equiv.refl α) a) (↑(Equiv.refl α) b) ↔ r (↑(Equiv.refl α) a) (↑(Equiv.refl α) b)) }

ink

@[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 : α), ↑(RelIso.toRelEmbedding (RelIso.trans f₁ f₂)).toEmbedding a = ↑(RelIso.toRelEmbedding f₂).toEmbedding (↑(RelIso.toRelEmbedding f₁).toEmbedding a)

ink

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

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

ink

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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 := Equiv.cast h₁, map_rel_iff' := (_ : ∀ (a b : α), s (↑(Equiv.cast h₁) a) (↑(Equiv.cast h₁) b) ↔ r a b) }

ink

@[simp]

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

ink

@[simp]

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

ink

@[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.trans (RelIso.cast h₁ h₂) (RelIso.cast h₁' h₂') = RelIso.cast (_ : α = γ) (_ : HEq r t)

ink

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

• RelIso.swap f = { toEquiv := f.toEquiv, map_rel_iff' := (_ : ∀ {a b : α}, s (↑(RelIso.toRelEmbedding f).toEmbedding b) (↑(RelIso.toRelEmbedding f).toEmbedding a) ↔ r b a) }

ink

@[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) : ↑(RelIso.toRelEmbedding (RelIso.symm { toEquiv := f, map_rel_iff' := o })).toEmbedding = ↑(Equiv.symm f)

ink

@[simp]

theorem RelIso.apply_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (x : β) : ↑(RelIso.toRelEmbedding e).toEmbedding (↑(RelIso.toRelEmbedding (RelIso.symm e)).toEmbedding x) = x

ink

@[simp]

theorem RelIso.symm_apply_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (x : α) : ↑(RelIso.toRelEmbedding (RelIso.symm e)).toEmbedding (↑(RelIso.toRelEmbedding e).toEmbedding x) = x

ink

theorem RelIso.rel_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {x : α} {y : β} : r x (↑(RelIso.toRelEmbedding (RelIso.symm e)).toEmbedding y) ↔ s (↑(RelIso.toRelEmbedding e).toEmbedding x) y

ink

theorem RelIso.symm_apply_rel {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {x : β} {y : α} : r (↑(RelIso.toRelEmbedding (RelIso.symm e)).toEmbedding x) y ↔ s x (↑(RelIso.toRelEmbedding e).toEmbedding y)

ink

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

ink

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

ink

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

ink

theorem RelIso.eq_iff_eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {a : α} {b : α} : ↑(RelIso.toRelEmbedding f).toEmbedding a = ↑(RelIso.toRelEmbedding f).toEmbedding b ↔ a = b

ink

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' := (_ : ∀ {a b : α}, s (↑f a) (↑f b) ↔ s (↑f a) (↑f b)) }

ink

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

Equations

• @RelIso.IsWellOrder.preimage = @RelIso.IsWellOrder.preimage.proof_1

ink

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

Equations

• @RelIso.IsWellOrder.ulift = @RelIso.IsWellOrder.ulift.proof_1

ink

@[simp]

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

ink

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

A surjective relation embedding is a relation isomorphism.

Equations

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

ink

def RelIso.sumLexCongr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {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₁≃r s₁ and r₂ ≃r s₂≃r s₂, construct a relation isomorphism for the lexicographic orders on the sum.

Equations

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

ink

def RelIso.prodLexCongr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {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₁≃r s₁ and r₂ ≃r s₂≃r s₂, construct a relation isomorphism for the lexicographic orders on the product.

Equations

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

ink

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

Two relations on empty types are isomorphic.

Equations

• RelIso.relIsoOfIsEmpty r s = { toEquiv := Equiv.equivOfIsEmpty α β, map_rel_iff' := (_ : ∀ (a : α) {b : α}, s (↑(Equiv.equivOfIsEmpty α β) a) (↑(Equiv.equivOfIsEmpty α β) b) ↔ r a b) }

ink

def RelIso.relIsoOfUniqueOfIrrefl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsIrrefl α r] [inst : IsIrrefl β s] [inst : Unique α] [inst : Unique β] : r ≃r s

Two irreflexive relations on a unique type are isomorphic.

Equations

• RelIso.relIsoOfUniqueOfIrrefl r s = { toEquiv := Equiv.equivOfUnique α β, map_rel_iff' := (_ : ∀ {a b : α}, s (↑(Equiv.equivOfUnique α β) a) (↑(Equiv.equivOfUnique α β) b) ↔ r a b) }

ink

def RelIso.relIsoOfUniqueOfRefl {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsRefl α r] [inst : IsRefl β s] [inst : Unique α] [inst : Unique β] : r ≃r s

Two reflexive relations on a unique type are isomorphic.

Equations

• RelIso.relIsoOfUniqueOfRefl r s = { toEquiv := Equiv.equivOfUnique α β, map_rel_iff' := (_ : ∀ {a b : α}, s (↑(Equiv.equivOfUnique α β) a) (↑(Equiv.equivOfUnique α β) b) ↔ r a b) }