# mathlib3documentation

order.rel_iso.basic

# Relation homomorphisms, embeddings, isomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main declarations #

• `rel_hom`: Relation homomorphism. A `rel_hom r s` is a function `f : α → β` such that `r a b → s (f a) (f b)`.
• `rel_embedding`: Relation embedding. A `rel_embedding r s` is an embedding `f : α ↪ β` such that `r a b ↔ s (f a) (f b)`.
• `rel_iso`: Relation isomorphism. A `rel_iso r s` is an equivalence `f : α ≃ β` such that `r a b ↔ s (f a) (f b)`.
• `sum_lex_congr`, `prod_lex_congr`: Creates a relation homomorphism between two `sum_lex` or two `prod_lex` from relation homomorphisms between their arguments.

## Notation #

• `→r`: `rel_hom`
• `↪r`: `rel_embedding`
• `≃r`: `rel_iso`
@[nolint]
structure rel_hom {α : 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)`.

Instances for `rel_hom`
@[nolint, instance]
def rel_hom_class.to_fun_like (F : Type u_5) {α : out_param (Type u_6)} {β : out_param (Type u_7)} (r : out_param α Prop)) (s : out_param β Prop)) [self : s] :
α (λ (_x : α), β)
@[class]
structure rel_hom_class (F : Type u_5) {α : out_param (Type u_6)} {β : out_param (Type u_7)} (r : out_param α Prop)) (s : out_param β Prop)) :
Type (max u_5 u_6 u_7)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_rel : (f : F) {a b : α}, r a b s (f a) (f b)

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

Instances of this typeclass
Instances of other typeclasses for `rel_hom_class`
• rel_hom_class.has_sizeof_inst
@[protected]
theorem rel_hom_class.is_irrefl {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} {F : Type u_5} [ s] (f : F) [ s] :
r
@[protected]
theorem rel_hom_class.is_asymm {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} {F : Type u_5} [ s] (f : F) [ s] :
r
@[protected]
theorem rel_hom_class.acc {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} {F : Type u_5} [ s] (f : F) (a : α) :
acc s (f a) acc r a
@[protected]
theorem rel_hom_class.well_founded {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} {F : Type u_5} [ s] (f : F) (h : well_founded s) :
@[protected, instance]
def rel_hom.rel_hom_class {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
Equations
@[protected, instance]
def rel_hom.has_coe_to_fun {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
has_coe_to_fun (r →r s) (λ (_x : r →r s), α β)

Auxiliary instance if `rel_hom_class.to_fun_like.to_has_coe_to_fun` isn't found

Equations
@[protected]
theorem rel_hom.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 rel_hom.coe_fn_mk {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : α β) (o : {a b : α}, r a b s (f a) (f b)) :
{to_fun := f, map_rel' := o} = f
@[simp]
theorem rel_hom.coe_fn_to_fun {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r →r s) :
theorem rel_hom.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :

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

@[ext]
theorem rel_hom.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 rel_hom.ext_iff {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} {f g : r →r s} :
f = g (x : α), f x = g x
@[simp]
theorem rel_hom.id_apply {α : Type u_1} (r : α α Prop) (x : α) :
@[protected, refl]
def rel_hom.id {α : Type u_1} (r : α α Prop) :
r →r r

Identity map is a relation homomorphism.

Equations
@[simp]
theorem rel_hom.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)
@[protected, trans]
def rel_hom.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
@[protected]
def rel_hom.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
def rel_hom.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
theorem injective_of_increasing {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] (f : α β) (hf : {x y : α}, r x y s (f x) (f y)) :

An increasing function is injective

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

An increasing function is injective

theorem surjective.well_founded_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)) :
structure rel_embedding {α : Type u_5} {β : Type u_6} (r : α α Prop) (s : β β Prop) :
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)`.

Instances for `rel_embedding`
def subtype.rel_embedding {X : Type u_1} (r : X X Prop) (p : X Prop) :

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

Equations
theorem preimage_equivalence {α : Sort u_1} {β : Sort u_2} (f : α β) {s : β β Prop} (hs : equivalence s) :
def rel_embedding.to_rel_hom {α : 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
@[protected, instance]
def rel_embedding.rel_hom.has_coe {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
has_coe (r ↪r s) (r →r s)
Equations
@[protected, instance]
def rel_embedding.has_coe_to_fun {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
has_coe_to_fun (r ↪r s) (λ (_x : r ↪r s), α β)
Equations
@[protected, instance]
def rel_embedding.rel_hom_class {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
Equations
def rel_embedding.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 it is a composition of multiple projections.

Equations
@[simp]
theorem rel_embedding.to_rel_hom_eq_coe {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) :
@[simp]
theorem rel_embedding.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) :
theorem rel_embedding.injective {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) :
@[simp]
theorem rel_embedding.inj {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) {a b : α} :
f a = f b a = b
theorem rel_embedding.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 rel_embedding.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) :
@[simp]
theorem rel_embedding.coe_fn_to_embedding {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) :
theorem rel_embedding.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :

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

@[ext]
theorem rel_embedding.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 rel_embedding.ext_iff {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} {f g : r ↪r s} :
f = g (x : α), f x = g x
@[simp]
theorem rel_embedding.refl_apply {α : Type u_1} (r : α α Prop) (a : α) :
a = a
@[protected, refl]
def rel_embedding.refl {α : Type u_1} (r : α α Prop) :
r ↪r r

Identity map is a relation embedding.

Equations
@[protected, trans]
def rel_embedding.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
@[protected, instance]
def rel_embedding.inhabited {α : Type u_1} (r : α α Prop) :
Equations
theorem rel_embedding.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 rel_embedding.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
@[protected]
def rel_embedding.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
def rel_embedding.preimage {α : Type u_1} {β : Type u_2} (f : α β) (s : β β Prop) :

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

Equations
theorem rel_embedding.eq_preimage {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) :
@[protected]
theorem rel_embedding.is_irrefl {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
r
@[protected]
theorem rel_embedding.is_refl {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
r
@[protected]
theorem rel_embedding.is_symm {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
r
@[protected]
theorem rel_embedding.is_asymm {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
r
@[protected]
theorem rel_embedding.is_antisymm {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
r
@[protected]
theorem rel_embedding.is_trans {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
r
@[protected]
theorem rel_embedding.is_total {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
r
@[protected]
theorem rel_embedding.is_preorder {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
r
@[protected]
theorem rel_embedding.is_partial_order {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
@[protected]
theorem rel_embedding.is_linear_order {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
@[protected]
theorem rel_embedding.is_strict_order {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
@[protected]
theorem rel_embedding.is_trichotomous {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
@[protected]
theorem rel_embedding.is_strict_total_order {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s)  :
@[protected]
theorem rel_embedding.acc {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) (a : α) :
acc s (f a) acc r a
@[protected]
theorem rel_embedding.well_founded {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) (h : well_founded s) :
@[protected]
theorem rel_embedding.is_well_founded {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
@[protected]
theorem rel_embedding.is_well_order {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) [ s] :
@[protected, instance]
def subtype.well_founded_lt {α : Type u_1} [has_lt α] (p : α Prop) :
@[protected, instance]
def subtype.well_founded_gt {α : Type u_1} [has_lt α] (p : α Prop) :
def quotient.mk_rel_hom {α : Type u_1} [setoid α] {r : α α Prop} (H : (a₁ a₂ b₁ b₂ : α), a₁ b₁ a₂ b₂ r a₁ a₂ = r b₁ b₂) :
r →r

`quotient.mk` as a relation homomorphism between the relation and the lift of a relation.

Equations
@[simp]
theorem quotient.mk_rel_hom_apply {α : Type u_1} [setoid α] {r : α α Prop} (H : (a₁ a₂ b₁ b₂ : α), a₁ b₁ a₂ b₂ r a₁ a₂ = r b₁ b₂) (a : α) :
a = a
@[simp]
theorem quotient.out_rel_embedding_apply {α : Type u_1} [setoid α] {r : α α Prop} (H : (a₁ a₂ b₁ b₂ : α), a₁ b₁ a₂ b₂ r a₁ a₂ = r b₁ b₂) (ᾰ : quotient _inst_1) :
= ᾰ.out
noncomputable def quotient.out_rel_embedding {α : Type u_1} [setoid α] {r : α α Prop} (H : (a₁ a₂ b₁ b₂ : α), a₁ b₁ a₂ b₂ r a₁ a₂ = r b₁ b₂) :
↪r r

`quotient.out` as a relation embedding between the lift of a relation and the relation.

Equations
@[simp]
theorem quotient.out'_rel_embedding_apply {α : Type u_1} {s : setoid α} {r : α α Prop} (H : (a₁ a₂ b₁ b₂ : α), setoid.r a₁ b₁ setoid.r a₂ b₂ r a₁ a₂ = r b₁ b₂) (a : quotient s) :
noncomputable def quotient.out'_rel_embedding {α : Type u_1} {s : setoid α} {r : α α Prop} (H : (a₁ a₂ b₁ b₂ : α), setoid.r a₁ b₁ setoid.r a₂ b₂ r a₁ a₂ = r b₁ b₂) :
(λ (a b : quotient s), a.lift_on₂' b r H) ↪r r

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

Equations
@[simp]
theorem acc_lift₂_iff {α : Type u_1} [setoid α] {r : α α Prop} {H : (a₁ a₂ b₁ b₂ : α), a₁ b₁ a₂ b₂ r a₁ a₂ = r b₁ b₂} {a : α} :
acc H) a acc r a
@[simp]
theorem acc_lift_on₂'_iff {α : Type u_1} {s : setoid α} {r : α α Prop} {H : (a₁ a₂ b₁ b₂ : α), setoid.r a₁ b₁ setoid.r a₂ b₂ r a₁ a₂ = r b₁ b₂} {a : α} :
acc (λ (x y : quotient s), x.lift_on₂' y r H) (quotient.mk' a) acc r a
theorem well_founded_lift₂_iff {α : Type u_1} [setoid α] {r : α α Prop} {H : (a₁ a₂ b₁ b₂ : α), a₁ b₁ a₂ b₂ r a₁ a₂ = r b₁ b₂} :

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

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

Alias of the forward direction of `well_founded_lift₂_iff`.

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

Alias of the reverse direction of `well_founded_lift₂_iff`.

@[simp]
theorem well_founded_lift_on₂'_iff {α : Type u_1} {s : setoid α} {r : α α Prop} {H : (a₁ a₂ b₁ b₂ : α), setoid.r a₁ b₁ setoid.r a₂ b₂ r a₁ a₂ = r b₁ b₂} :
well_founded (λ (x y : quotient s), x.lift_on₂' y r H)
theorem well_founded.of_quotient_lift_on₂' {α : Type u_1} {s : setoid α} {r : α α Prop} {H : (a₁ a₂ b₁ b₂ : α), setoid.r a₁ b₁ setoid.r a₂ b₂ r a₁ a₂ = r b₁ b₂} :
well_founded (λ (x y : quotient s), x.lift_on₂' y r H)

Alias of the forward direction of `well_founded_lift_on₂'_iff`.

theorem well_founded.quotient_lift_on₂' {α : Type u_1} {s : setoid α} {r : α α Prop} {H : (a₁ a₂ b₁ b₂ : α), setoid.r a₁ b₁ setoid.r a₂ b₂ r a₁ a₂ = r b₁ b₂} :
well_founded (λ (x y : quotient s), x.lift_on₂' y r H)

Alias of the reverse direction of `well_founded_lift_on₂'_iff`.

def rel_embedding.of_map_rel_iff {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : α β) [ r] [ 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`.

Equations
@[simp]
theorem rel_embedding.of_map_rel_iff_coe {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : α β) [ r] [ s] (hf : (a b : α), s (f a) (f b) r a b) :
= f
def rel_embedding.of_monotone {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [ r] [ 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
@[simp]
theorem rel_embedding.of_monotone_coe {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [ r] [ s] (f : α β) (H : (a b : α), r a b s (f a) (f b)) :
= f
def rel_embedding.of_is_empty {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_empty α] :
r ↪r s

A relation embedding from an empty type.

Equations
@[simp]
theorem rel_embedding.sum_lift_rel_inl_apply {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) (val : α) :
val = sum.inl val
def rel_embedding.sum_lift_rel_inl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) :
r ↪r s

`sum.inl` as a relation embedding into `sum.lift_rel r s`.

Equations
def rel_embedding.sum_lift_rel_inr {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) :
s ↪r s

`sum.inr` as a relation embedding into `sum.lift_rel r s`.

Equations
@[simp]
theorem rel_embedding.sum_lift_rel_inr_apply {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) (val : β) :
val = sum.inr val
def rel_embedding.sum_lift_rel_map {α : 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) :
t ↪r u

`sum.map` as a relation embedding between `sum.lift_rel` relations.

Equations
@[simp]
theorem rel_embedding.sum_lift_rel_map_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) (ᾰ : α γ) :
(f.sum_lift_rel_map g) = g
@[simp]
theorem rel_embedding.sum_lex_inl_apply {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) (val : α) :
val = sum.inl val
def rel_embedding.sum_lex_inl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) :
r ↪r s

`sum.inl` as a relation embedding into `sum.lex r s`.

Equations
@[simp]
theorem rel_embedding.sum_lex_inr_apply {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) (val : β) :
val = sum.inr val
def rel_embedding.sum_lex_inr {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) :
s ↪r s

`sum.inr` as a relation embedding into `sum.lex r s`.

Equations
@[simp]
theorem rel_embedding.sum_lex_map_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) (ᾰ : α γ) :
(f.sum_lex_map g) = g
def rel_embedding.sum_lex_map {α : 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) :
t ↪r u

`sum.map` as a relation embedding between `sum.lex` relations.

Equations
def rel_embedding.prod_lex_mk_left {α : Type u_1} {β : Type u_2} {r : α α Prop} (s : β β Prop) {a : α} (h : ¬r a a) :
s ↪r s

`λ b, prod.mk a b` as a relation embedding.

Equations
@[simp]
theorem rel_embedding.prod_lex_mk_left_apply {α : Type u_1} {β : Type u_2} {r : α α Prop} (s : β β Prop) {a : α} (h : ¬r a a) (snd : β) :
snd = (a, snd)
def rel_embedding.prod_lex_mk_right {α : Type u_1} {β : Type u_2} {s : β β Prop} (r : α α Prop) {b : β} (h : ¬s b b) :
r ↪r s

`λ a, prod.mk a b` as a relation embedding.

Equations
@[simp]
theorem rel_embedding.prod_lex_mk_right_apply {α : Type u_1} {β : Type u_2} {s : β β Prop} (r : α α Prop) {b : β} (h : ¬s b b) (a : α) :
= (a, b)
@[simp]
theorem rel_embedding.prod_lex_map_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) (x : α × γ) :
(f.prod_lex_map g) x = g x
def rel_embedding.prod_lex_map {α : 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) :
t ↪r u

`prod.map` as a relation embedding.

Equations
structure rel_iso {α : Type u_5} {β : Type u_6} (r : α α Prop) (s : β β Prop) :
Type (max u_5 u_6)

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

Instances for `rel_iso`
def rel_iso.to_rel_embedding {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ≃r s) :
r ↪r s

Convert an `rel_iso` to an `rel_embedding`. This function is also available as a coercion but often it is easier to write `f.to_rel_embedding` than to write explicitly `r` and `s` in the target type.

Equations
theorem rel_iso.to_equiv_injective {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
@[protected, instance]
def rel_iso.rel_embedding.has_coe {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
has_coe (r ≃r s) (r ↪r s)
Equations
@[protected, instance]
def rel_iso.has_coe_to_fun {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
has_coe_to_fun (r ≃r s) (λ (_x : r ≃r s), α β)
Equations
@[protected, instance]
def rel_iso.rel_hom_class {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
Equations
@[simp]
theorem rel_iso.to_rel_embedding_eq_coe {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ≃r s) :
@[simp]
theorem rel_iso.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ≃r s) :
theorem rel_iso.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 rel_iso.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) :
@[simp]
theorem rel_iso.coe_fn_to_equiv {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ≃r s) :
theorem rel_iso.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :

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

@[ext]
theorem rel_iso.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 rel_iso.ext_iff {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} {f g : r ≃r s} :
f = g (x : α), f x = g x
@[protected, symm]
def rel_iso.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
def rel_iso.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 it is a composition of multiple projections.

Equations
def rel_iso.simps.symm_apply {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (h : r ≃r s) :
β α
Equations
@[protected, refl]
def rel_iso.refl {α : Type u_1} (r : α α Prop) :
r ≃r r

Identity map is a relation isomorphism.

Equations
@[simp]
theorem rel_iso.refl_apply {α : Type u_1} (r : α α Prop) (a : α) :
@[protected, trans]
def rel_iso.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
@[simp]
theorem rel_iso.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) (ᾰ : α) :
(f₁.trans f₂) = f₂ (f₁ ᾰ)
@[protected, instance]
def rel_iso.inhabited {α : Type u_1} (r : α α Prop) :
Equations
@[simp]
theorem rel_iso.default_def {α : Type u_1} (r : α α Prop) :
@[simp]
theorem rel_iso.cast_apply {α β : Type u} {r : α α Prop} {s : β β Prop} (h₁ : α = β) (h₂ : r == s) (a : α) :
(rel_iso.cast h₁ h₂) a = cast h₁ a
@[simp]
theorem rel_iso.cast_to_equiv {α β : Type u} {r : α α Prop} {s : β β Prop} (h₁ : α = β) (h₂ : r == s) :
(rel_iso.cast h₁ h₂).to_equiv =
@[protected]
def rel_iso.cast {α β : Type u} {r : α α Prop} {s : β β Prop} (h₁ : α = β) (h₂ : r == s) :
r ≃r s

A relation isomorphism between equal relations on equal types.

Equations
@[protected, simp]
theorem rel_iso.cast_symm {α β : Type u} {r : α α Prop} {s : β β Prop} (h₁ : α = β) (h₂ : r == s) :
(rel_iso.cast h₁ h₂).symm = _
@[protected, simp]
theorem rel_iso.cast_refl {α : Type u} {r : α α Prop} (h₁ : α = α := rfl) (h₂ : r == r := heq.rfl) :
h₂ =
@[protected, simp]
theorem rel_iso.cast_trans {α β γ : Type u} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (h₁ : α = β) (h₁' : β = γ) (h₂ : r == s) (h₂' : s == t) :
(rel_iso.cast h₁ h₂).trans (rel_iso.cast h₁' h₂') = _
@[protected]
def rel_iso.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
@[simp]
theorem rel_iso.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) :
@[simp]
theorem rel_iso.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 rel_iso.symm_apply_apply {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (e : r ≃r s) (x : α) :
(e.symm) (e x) = x
theorem rel_iso.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 rel_iso.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)
@[protected]
theorem rel_iso.bijective {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (e : r ≃r s) :
@[protected]
theorem rel_iso.injective {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (e : r ≃r s) :
@[protected]
theorem rel_iso.surjective {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (e : r ≃r s) :
@[simp]
theorem rel_iso.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
@[protected]
def rel_iso.preimage {α : Type u_1} {β : Type u_2} (f : α β) (s : β β Prop) :

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

Equations
@[protected, instance]
def rel_iso.is_well_order.preimage {β : Type u_2} {α : Type u} (r : α α Prop) [ r] (f : β α) :
(f ⁻¹'o r)
@[protected, instance]
def rel_iso.is_well_order.ulift {α : Type u} (r : α α Prop) [ r] :
@[simp]
theorem rel_iso.of_surjective_apply {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) (H : function.surjective f) (ᾰ : α) :
= f ᾰ
noncomputable def rel_iso.of_surjective {α : 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
def rel_iso.sum_lex_congr {α₁ : 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₁` and `r₂ ≃r s₂`, construct a relation isomorphism for the lexicographic orders on the sum.

Equations
def rel_iso.prod_lex_congr {α₁ : 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₁` and `r₂ ≃r s₂`, construct a relation isomorphism for the lexicographic orders on the product.

Equations
def rel_iso.rel_iso_of_is_empty {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_empty α] [is_empty β] :
r ≃r s

Two relations on empty types are isomorphic.

Equations
def rel_iso.rel_iso_of_unique_of_irrefl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] [unique α] [unique β] :
r ≃r s

Two irreflexive relations on a unique type are isomorphic.

Equations
def rel_iso.rel_iso_of_unique_of_refl {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [ r] [ s] [unique α] [unique β] :
r ≃r s

Two reflexive relations on a unique type are isomorphic.

Equations