mathlib documentation

order.rel_iso

Relation homomorphisms, embeddings, isomorphisms #

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

Main declarations #

Notation #

source
@[nolint]
structure rel_hom {α : Type u_4} {β : Type u_5} (r : α → α → Prop) (s : β → β → Prop) :
Type (max u_4 u_5)
  • to_fun : α → β
  • map_rel' : ∀ {a b : α}, r a b → s (self.to_fun a) (self.to_fun 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).

source
@[class]
structure rel_hom_class (F : Type u_4) {α : out_param (Type u_5)} {β : out_param (Type u_6)} (r : out_param (α → α → Prop)) (s : out_param (β → β → Prop)) :
Type (max u_4 u_5 u_6)
  • to_fun_like : fun_like F α (λ (_x : α), β)
  • 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_params since figuring them out from a goal is a higher-order matching problem that Lean usually can't do unaided.

Instances
source
theorem rel_hom_class.map_inf {α : Type u_1} {β : Type u_2} {F : Type u_4} [semilattice_inf α] [linear_order β] [rel_hom_class F has_lt.lt has_lt.lt] (a : F) (m n : β) :
⇑a (m ⊓ n) = ⇑a m ⊓ ⇑a n
source
theorem rel_hom_class.map_sup {α : Type u_1} {β : Type u_2} {F : Type u_4} [semilattice_sup α] [linear_order β] [rel_hom_class F gt gt] (a : F) (m n : β) :
⇑a (m ⊔ n) = ⇑a m ⊔ ⇑a n
source
@[protected]
theorem rel_hom_class.is_irrefl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_4} [rel_hom_class F r s] (f : F) [is_irrefl β s] :
is_irrefl α r
source
@[protected]
theorem rel_hom_class.is_asymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_4} [rel_hom_class F r s] (f : F) [is_asymm β s] :
is_asymm α r
source
@[protected]
theorem rel_hom_class.acc {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_4} [rel_hom_class F r s] (f : F) (a : α) :
acc s (⇑f a) → acc r a
source
@[protected]
theorem rel_hom_class.well_founded {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_4} [rel_hom_class F r s] (f : F) (h : well_founded s) :
well_founded r
source
@[protected, instance]
def rel_hom.rel_hom_class {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
rel_hom_class (r →r s) r s
Equations
source
@[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
source
@[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)
source
@[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
source
@[simp]
theorem rel_hom.coe_fn_to_fun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) :
f.to_fun = ⇑f
source
theorem rel_hom.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
function.injective coe_fn

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

source
@[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
source
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
source
@[simp]
theorem rel_hom.id_apply {α : Type u_1} (r : α → α → Prop) (x : α) :
⇑(rel_hom.id r) x = x
source
@[protected]
def rel_hom.id {α : Type u_1} (r : α → α → Prop) :
r →r r

Identity map is a relation homomorphism.

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

An increasing function is injective

source
theorem rel_hom.injective_of_increasing {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trichotomous α r] [is_irrefl β s] (f : r →r s) :
function.injective ⇑f

An increasing function is injective

source
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)) :
well_founded r ↔ well_founded s
source
structure rel_embedding {α : Type u_4} {β : Type u_5} (r : α → α → Prop) (s : β → β → Prop) :
Type (max u_4 u_5)

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

source
def subtype.rel_embedding {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
source
theorem preimage_equivalence {α : Sort u_1} {β : Sort u_2} (f : α → β) {s : β → β → Prop} (hs : equivalence s) :
equivalence (f ⁻¹'o s)
source
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
source
@[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
source
@[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
source
@[protected, instance]
def rel_embedding.rel_hom_class {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
rel_hom_class (r ↪r s) r s
Equations
source
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
source
@[simp]
theorem rel_embedding.to_rel_hom_eq_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) :
f.to_rel_hom = ↑f
source
@[simp]
theorem rel_embedding.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) :
⇑↑f = ⇑f
source
theorem rel_embedding.injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) :
function.injective ⇑f
source
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
source
@[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) :
⇑{to_embedding := f, map_rel_iff' := o} = ⇑f
source
@[simp]
theorem rel_embedding.coe_fn_to_embedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) :
⇑(f.to_embedding) = ⇑f
source
theorem rel_embedding.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
function.injective coe_fn

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

source
@[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
source
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
source
@[simp]
theorem rel_embedding.refl_apply {α : Type u_1} (r : α → α → Prop) (a : α) :
⇑(rel_embedding.refl r) a = a
source
@[protected]
def rel_embedding.refl {α : Type u_1} (r : α → α → Prop) :
r ↪r r

Identity map is a relation embedding.

Equations
source
@[protected]
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
source
@[protected, instance]
def rel_embedding.inhabited {α : Type u_1} (r : α → α → Prop) :
inhabited (r ↪r r)
Equations
source
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)
source
@[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
source
@[protected]
def rel_embedding.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
source
def rel_embedding.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
source
theorem rel_embedding.eq_preimage {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) :
r = ⇑f ⁻¹'o s
source
@[protected]
theorem rel_embedding.is_irrefl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_irrefl β s] :
is_irrefl α r
source
@[protected]
theorem rel_embedding.is_refl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_refl β s] :
is_refl α r
source
@[protected]
theorem rel_embedding.is_symm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_symm β s] :
is_symm α r
source
@[protected]
theorem rel_embedding.is_asymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_asymm β s] :
is_asymm α r
source
@[protected]
theorem rel_embedding.is_antisymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_antisymm β s] :
is_antisymm α r
source
@[protected]
theorem rel_embedding.is_trans {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_trans β s] :
is_trans α r
source
@[protected]
theorem rel_embedding.is_total {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_total β s] :
is_total α r
source
@[protected]
theorem rel_embedding.is_preorder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_preorder β s] :
is_preorder α r
source
@[protected]
theorem rel_embedding.is_partial_order {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_partial_order β s] :
is_partial_order α r
source
@[protected]
theorem rel_embedding.is_linear_order {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_linear_order β s] :
is_linear_order α r
source
@[protected]
theorem rel_embedding.is_strict_order {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_strict_order β s] :
is_strict_order α r
source
@[protected]
theorem rel_embedding.is_trichotomous {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_trichotomous β s] :
is_trichotomous α r
source
@[protected]
theorem rel_embedding.is_strict_total_order' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_strict_total_order' β s] :
is_strict_total_order' α r
source
@[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
source
@[protected]
theorem rel_embedding.well_founded {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (h : well_founded s) :
well_founded r
source
@[protected]
theorem rel_embedding.is_well_order {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_well_order β s] :
is_well_order α r
source
def rel_embedding.of_map_rel_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : α → β) [is_antisymm α r] [is_refl β 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
source
@[simp]
theorem rel_embedding.of_map_rel_iff_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : α → β) [is_antisymm α r] [is_refl β s] (hf : ∀ (a b : α), s (f a) (f b) ↔ r a b) :
⇑(rel_embedding.of_map_rel_iff f hf) = f
source
def rel_embedding.of_monotone {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trichotomous α r] [is_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
source
@[simp]
theorem rel_embedding.of_monotone_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trichotomous α r] [is_asymm β s] (f : α → β) (H : ∀ (a b : α), r a b → s (f a) (f b)) :
⇑(rel_embedding.of_monotone f H) = f
source
structure rel_iso {α : Type u_4} {β : Type u_5} (r : α → α → Prop) (s : β → β → Prop) :
Type (max u_4 u_5)

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

source
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
source
theorem rel_iso.to_equiv_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
function.injective rel_iso.to_equiv
source
@[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
source
@[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
source
@[protected, instance]
def rel_iso.rel_hom_class {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
rel_hom_class (r ≃r s) r s
Equations
source
@[simp]
theorem rel_iso.to_rel_embedding_eq_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) :
f.to_rel_embedding = ↑f
source
@[simp]
theorem rel_iso.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) :
⇑↑f = ⇑f
source
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
source
@[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) :
⇑{to_equiv := f, map_rel_iff' := o} = ⇑f
source
@[simp]
theorem rel_iso.coe_fn_to_equiv {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) :
⇑(f.to_equiv) = ⇑f
source
theorem rel_iso.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
function.injective coe_fn

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.

source
@[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
source
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
source
@[protected]
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
source
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
source
def rel_iso.simps.symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (h : r ≃r s) :
β → α

See Note [custom simps projection].

Equations
source
@[protected]
def rel_iso.refl {α : Type u_1} (r : α → α → Prop) :
r ≃r r

Identity map is a relation isomorphism.

Equations
source
@[simp]
theorem rel_iso.refl_apply {α : Type u_1} (r : α → α → Prop) (a : α) :
⇑(rel_iso.refl r) a = a
source
@[protected]
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
source
@[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₁ ᾰ)
source
@[protected, instance]
def rel_iso.inhabited {α : Type u_1} (r : α → α → Prop) :
inhabited (r ≃r r)
Equations
source
@[simp]
theorem rel_iso.default_def {α : Type u_1} (r : α → α → Prop) :
default (r ≃r r) = rel_iso.refl r
source
@[protected]
def rel_iso.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
source
@[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) :
⇑({to_equiv := f, map_rel_iff' := o}.symm) = ⇑(f.symm)
source
@[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
source
@[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
source
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
source
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)
source
@[protected]
theorem rel_iso.bijective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) :
function.bijective ⇑e
source
@[protected]
theorem rel_iso.injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) :
function.injective ⇑e
source
@[protected]
theorem rel_iso.surjective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) :
function.surjective ⇑e
source
@[simp]
theorem rel_iso.range_eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) :
set.range ⇑e = set.univ
source
@[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
source
@[protected]
def rel_iso.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
source
@[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) (ᾰ : α) :
⇑(rel_iso.of_surjective f H) ᾰ = ⇑f ᾰ
source
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
source
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
source
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
source
@[protected, instance]
def rel_iso.group {α : Type u_1} {r : α → α → Prop} :
group (r ≃r r)
Equations
source
@[simp]
theorem rel_iso.coe_one {α : Type u_1} {r : α → α → Prop} :
⇑1 = id
source
@[simp]
theorem rel_iso.coe_mul {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) :
⇑e₁ * e₂ = ⇑e₁ ∘ ⇑e₂
source
theorem rel_iso.mul_apply {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) (x : α) :
(⇑e₁ * e₂) x = ⇑e₁ (⇑e₂ x)
source
@[simp]
theorem rel_iso.inv_apply_self {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α) :
⇑e⁻¹ (⇑e x) = x
source
@[simp]
theorem rel_iso.apply_inv_self {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α) :
⇑e (⇑e⁻¹ x) = x
source
def subrel {α : Type u_1} (r : α → α → Prop) (p : set α) :
↥p → ↥p → Prop

subrel r p is the inherited relation on a subset.

Equations
source
@[simp]
theorem subrel_val {α : Type u_1} (r : α → α → Prop) (p : set α) {a b : ↥p} :
subrel r p a b ↔ r a.val b.val
source
@[protected]
def subrel.rel_embedding {α : Type u_1} (r : α → α → Prop) (p : set α) :
subrel r p ↪r r

The relation embedding from the inherited relation on a subset.

Equations
source
@[simp]
theorem subrel.rel_embedding_apply {α : Type u_1} (r : α → α → Prop) (p : set α) (a : ↥p) :
⇑(subrel.rel_embedding r p) a = a.val
source
@[protected, instance]
def subrel.is_well_order {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (p : set α) :
is_well_order ↥p (subrel r p)
source
def rel_embedding.cod_restrict {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : set β) (f : r ↪r s) (H : ∀ (a : α), ⇑f a ∈ p) :
r ↪r subrel s p

Restrict the codomain of a relation embedding.

Equations
source
@[simp]
theorem rel_embedding.cod_restrict_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : set β) (f : r ↪r s) (H : ∀ (a : α), ⇑f a ∈ p) (a : α) :
⇑(rel_embedding.cod_restrict p f H) a = ⟨⇑f a, _⟩