mathlib documentation

order.rel_iso

@[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 bs (c.to_fun a) (c.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).

@[instance]
def rel_hom.has_coe_to_fun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
Equations
theorem rel_hom.map_rel {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) {a b : α} :
r a bs (f a) (f b)
@[simp]
theorem rel_hom.coe_fn_mk {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : α → β) (o : ∀ {a b : α}, r a bs (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_inj {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃e₁ e₂ : r →r s⦄ :
e₁ = e₂e₁ = e₂

The map coe_fn : (r →r s) → (α → β) is injective. We can't use function.injective here but mimic its signature by using ⦃e₁ e₂⦄.

@[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 : α) :
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)
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
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 rel_hom.is_irrefl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) [is_irrefl β s] :
theorem rel_hom.is_asymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) [is_asymm β s] :
theorem rel_hom.acc {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) (a : α) :
acc s (f a)acc r a
theorem rel_hom.well_founded {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) (h : well_founded s) :
theorem rel_hom.map_inf {α : Type u_1} {β : Type u_2} [semilattice_inf α] [linear_order β] (a : has_lt.lt →r has_lt.lt) (m n : β) :
a (m n) = a m a n
theorem rel_hom.map_sup {α : Type u_1} {β : Type u_2} [semilattice_sup α] [linear_order β] (a : gt →r gt) (m n : β) :
a (m n) = a m a n
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 ys (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} [is_trichotomous α r] [is_irrefl β 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_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).

def order_embedding (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :
Type (max u_1 u_2)

An order embedding is an embedding f : α ↪ β such that a ≤ b ↔ (f a) ≤ (f b). This definition is an abbreviation of 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
@[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
@[instance]
def rel_embedding.has_coe_to_fun {α : 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) :
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_inj {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃e₁ e₂ : r ↪r s⦄ :
e₁ = e₂e₁ = e₂

The map coe_fn : (r ↪r s) → (α → β) is injective. We can't use function.injective here but mimic its signature by using ⦃e₁ e₂⦄.

@[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 : α) :
def rel_embedding.refl {α : Type u_1} (r : α → α → Prop) :
r ↪r r

Identity map is a relation embedding.

Equations
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
@[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
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) :
theorem rel_embedding.is_irrefl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_irrefl β s] :
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
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
theorem rel_embedding.is_asymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_asymm β s] :
theorem rel_embedding.is_antisymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_antisymm β s] :
theorem rel_embedding.is_trans {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_trans β s] :
theorem rel_embedding.is_total {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_total β s] :
theorem rel_embedding.is_preorder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_preorder β s] :
theorem rel_embedding.is_partial_order {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_partial_order β s] :
theorem rel_embedding.is_linear_order {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_linear_order β s] :
theorem rel_embedding.is_strict_order {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_strict_order β s] :
theorem rel_embedding.is_trichotomous {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_trichotomous β s] :
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] :
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
theorem rel_embedding.well_founded {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (h : well_founded s) :
theorem rel_embedding.is_well_order {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [is_well_order β s] :
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
@[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) :
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 bs (f a) (f b)) :
r ↪r s

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

Equations
@[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 bs (f a) (f b)) :
def rel_embedding.order_embedding_of_lt_embedding {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (f : has_lt.lt ↪r has_lt.lt) :
α ↪o β

Embeddings of partial orders that preserve < also preserve

Equations
@[simp]
def order_embedding.lt_embedding {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) :

lt is preserved by order embeddings of preorders

Equations
@[simp]
theorem order_embedding.lt_embedding_apply {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) (x : α) :
@[simp]
theorem order_embedding.le_iff_le {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) {a b : α} :
f a f b a b
@[simp]
theorem order_embedding.lt_iff_lt {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) {a b : α} :
f a < f b a < b
@[simp]
theorem order_embedding.eq_iff_eq {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) {a b : α} :
f a = f b a = b
theorem order_embedding.monotone {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) :
theorem order_embedding.strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) :
theorem order_embedding.acc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) (a : α) :
theorem order_embedding.well_founded {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) :
theorem order_embedding.is_well_order {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) [is_well_order β has_lt.lt] :
def order_embedding.dual {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) :

An order embedding is also an order embedding between dual orders.

Equations
def order_embedding.of_map_rel_iff {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] (f : α → β) (hf : ∀ (a b : α), f a f b a b) :
α ↪o β

To define an order embedding from a partial order to a preorder it suffices to give a function together with a proof that it satisfies f a ≤ f b ↔ a ≤ b.

Equations
@[simp]
theorem order_embedding.coe_of_map_rel_iff {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] {f : α → β} (h : ∀ (a b : α), f a f b a b) :
def order_embedding.of_strict_mono {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] (f : α → β) (h : strict_mono f) :
α ↪o β

A strictly monotone map from a linear order is an order embedding. -

Equations
@[simp]
theorem order_embedding.coe_of_strict_mono {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {f : α → β} (h : strict_mono f) :
@[simp]
theorem order_embedding.subtype_apply {α : Type u_1} [preorder α] (p : α → Prop) :
def order_embedding.subtype {α : Type u_1} [preorder α] (p : α → Prop) :

Embedding of a subtype into the ambient type as an order_embedding.

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

def order_iso (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :
Type (max u_1 u_2)

An order isomorphism is an equivalence such that a ≤ b ↔ (f a) ≤ (f b). This definition is an abbreviation of 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
@[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
@[instance]
def rel_iso.has_coe_to_fun {α : 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.to_equiv_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
theorem rel_iso.coe_fn_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
function.injective (λ (e : r ≃r s) (x : α), e x)

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
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) :
β → α

See Note [custom simps projection].

Equations
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 : α) :
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₁ ᾰ)
@[instance]
def rel_iso.inhabited {α : Type u_1} (r : α → α → Prop) :
Equations
@[simp]
theorem rel_iso.default_def {α : Type u_1} (r : α → α → Prop) :
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)
theorem rel_iso.bijective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) :
theorem rel_iso.injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) :
theorem rel_iso.surjective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) :
@[simp]
theorem rel_iso.range_eq {α : 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
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
@[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) (ᾰ : α) :
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 r₂) (e₂ : s₁ ≃r s₂) :
sum.lex r₁ s₁ ≃r sum.lex r₂ s₂

Given relation isomorphisms r₁ ≃r r₂ and s₁ ≃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 r₂) (e₂ : s₁ ≃r s₂) :
prod.lex r₁ s₁ ≃r prod.lex r₂ s₂

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

Equations
@[instance]
def rel_iso.group {α : Type u_1} {r : α → α → Prop} :
group (r ≃r r)
Equations
@[simp]
theorem rel_iso.coe_one {α : Type u_1} {r : α → α → Prop} :
@[simp]
theorem rel_iso.coe_mul {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) :
e₁ * e₂ = e₁ e₂
theorem rel_iso.mul_apply {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) (x : α) :
(e₁ * e₂) x = e₁ (e₂ x)
@[simp]
theorem rel_iso.inv_apply_self {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α) :
e⁻¹ (e x) = x
@[simp]
theorem rel_iso.apply_inv_self {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α) :
e (e⁻¹ x) = x
def order_iso.to_order_embedding {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
α ↪o β

Reinterpret an order isomorphism as an order embedding.

Equations
@[simp]
theorem order_iso.coe_to_order_embedding {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
theorem order_iso.bijective {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
theorem order_iso.injective {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
theorem order_iso.surjective {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
@[simp]
theorem order_iso.range_eq {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
@[simp]
theorem order_iso.apply_eq_iff_eq {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) {x y : α} :
e x = e y x = y
def order_iso.refl (α : Type u_1) [has_le α] :
α ≃o α

Identity order isomorphism.

Equations
@[simp]
theorem order_iso.coe_refl {α : Type u_1} [has_le α] :
theorem order_iso.refl_apply {α : Type u_1} [has_le α] (x : α) :
@[simp]
theorem order_iso.refl_to_equiv {α : Type u_1} [has_le α] :
def order_iso.symm {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
β ≃o α

Inverse of an order isomorphism.

Equations
@[simp]
theorem order_iso.apply_symm_apply {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (x : β) :
e ((e.symm) x) = x
@[simp]
theorem order_iso.symm_apply_apply {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (x : α) :
(e.symm) (e x) = x
@[simp]
theorem order_iso.symm_refl (α : Type u_1) [has_le α] :
theorem order_iso.apply_eq_iff_eq_symm_apply {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (x : α) (y : β) :
e x = y x = (e.symm) y
theorem order_iso.symm_apply_eq {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) {x : α} {y : β} :
(e.symm) y = x y = e x
@[simp]
theorem order_iso.symm_symm {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
e.symm.symm = e
theorem order_iso.symm_injective {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] :
@[simp]
theorem order_iso.to_equiv_symm {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
def order_iso.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (e : α ≃o β) (e' : β ≃o γ) :
α ≃o γ

Composition of two order isomorphisms is an order isomorphism.

Equations
@[simp]
theorem order_iso.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (e : α ≃o β) (e' : β ≃o γ) :
(e.trans e') = e' e
theorem order_iso.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (e : α ≃o β) (e' : β ≃o γ) (x : α) :
(e.trans e') x = e' (e x)
@[simp]
theorem order_iso.refl_trans {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
@[simp]
theorem order_iso.trans_refl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
theorem order_iso.monotone {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) :
theorem order_iso.strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) :
@[simp]
theorem order_iso.le_iff_le {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) {x y : α} :
e x e y x y
@[simp]
theorem order_iso.lt_iff_lt {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) {x y : α} :
e x < e y x < y
@[simp]
theorem order_iso.preimage_Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (b : β) :
@[simp]
theorem order_iso.preimage_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (b : β) :
@[simp]
theorem order_iso.preimage_Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (b : β) :
@[simp]
theorem order_iso.preimage_Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (b : β) :
@[simp]
theorem order_iso.preimage_Icc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : β) :
e ⁻¹' set.Icc a b = set.Icc ((e.symm) a) ((e.symm) b)
@[simp]
theorem order_iso.preimage_Ico {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : β) :
e ⁻¹' set.Ico a b = set.Ico ((e.symm) a) ((e.symm) b)
@[simp]
theorem order_iso.preimage_Ioc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : β) :
e ⁻¹' set.Ioc a b = set.Ioc ((e.symm) a) ((e.symm) b)
@[simp]
theorem order_iso.preimage_Ioo {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : β) :
e ⁻¹' set.Ioo a b = set.Ioo ((e.symm) a) ((e.symm) b)
def order_iso.of_cmp_eq_cmp {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] (f : α → β) (g : β → α) (h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b) :
α ≃o β

To show that f : α → β, g : β → α make up an order isomorphism of linear orders, it suffices to prove cmp a (g b) = cmp (f a) b. -

Equations
def order_iso.set_congr {α : Type u_1} [preorder α] (s t : set α) (h : s = t) :

Order isomorphism between two equal sets.

Equations
def order_iso.set.univ {α : Type u_1} [preorder α] :

Order isomorphism between univ : set α and α.

Equations
def strict_mono_incr_on.order_iso {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] (f : α → β) (s : set α) (hf : strict_mono_incr_on f s) :
s ≃o (f '' s)

If a function f is strictly monotone on a set s, then it defines an order isomorphism between s and its image.

Equations
def strict_mono.order_iso {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] (f : α → β) (h_mono : strict_mono f) :

A strictly monotone function from a linear order is an order isomorphism between its domain and its range.

Equations
def strict_mono.order_iso_of_surjective {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] (f : α → β) (h_mono : strict_mono f) (h_surj : function.surjective f) :
α ≃o β

A strictly monotone surjective function from a linear order is an order isomorphism.

Equations
def subrel {α : Type u_1} (r : α → α → Prop) (p : set α) :
p → p → Prop

subrel r p is the inherited relation on a subset.

Equations
@[simp]
theorem subrel_val {α : Type u_1} (r : α → α → Prop) (p : set α) {a b : p} :
subrel r p a b r a.val b.val
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
@[simp]
theorem subrel.rel_embedding_apply {α : Type u_1} (r : α → α → Prop) (p : set α) (a : p) :
@[instance]
def subrel.is_well_order {α : Type u_1} (r : α → α → Prop) [is_well_order α r] (p : set α) :
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
@[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 : α) :
def order_iso.dual {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) :

An order isomorphism is also an order isomorphism between dual orders.

Equations
theorem order_iso.map_bot' {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ (x' : α), x x') (hy : ∀ (y' : β), y y') :
f x = y
theorem order_iso.map_bot {α : Type u_1} {β : Type u_2} [order_bot α] [order_bot β] (f : α ≃o β) :
theorem order_iso.map_top' {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ (x' : α), x' x) (hy : ∀ (y' : β), y' y) :
f x = y
theorem order_iso.map_top {α : Type u_1} {β : Type u_2} [order_top α] [order_top β] (f : α ≃o β) :
theorem order_embedding.map_inf_le {α : Type u_1} {β : Type u_2} [semilattice_inf α] [semilattice_inf β] (f : α ↪o β) (x y : α) :
f (x y) f x f y
theorem order_iso.map_inf {α : Type u_1} {β : Type u_2} [semilattice_inf α] [semilattice_inf β] (f : α ≃o β) (x y : α) :
f (x y) = f x f y
theorem order_embedding.le_map_sup {α : Type u_1} {β : Type u_2} [semilattice_sup α] [semilattice_sup β] (f : α ↪o β) (x y : α) :
f x f y f (x y)
theorem order_iso.map_sup {α : Type u_1} {β : Type u_2} [semilattice_sup α] [semilattice_sup β] (f : α ≃o β) (x y : α) :
f (x y) = f x f y
def order_iso.Iic_top {α : Type u_1} [order_top α] :

Order isomorphism between Iic (⊤ : α) and α when α has a top element

Equations
def order_iso.Ici_bot {α : Type u_1} [order_bot α] :

Order isomorphism between Ici (⊥ : α) and α when α has a bottom element

Equations
theorem order_iso.is_compl {α : Type u_1} {β : Type u_2} [bounded_lattice α] [bounded_lattice β] (f : α ≃o β) {x y : α} (h : is_compl x y) :
is_compl (f x) (f y)
theorem order_iso.is_compl_iff {α : Type u_1} {β : Type u_2} [bounded_lattice α] [bounded_lattice β] (f : α ≃o β) {x y : α} :
is_compl x y is_compl (f x) (f y)
theorem order_iso.is_complemented {α : Type u_1} {β : Type u_2} [bounded_lattice α] [bounded_lattice β] (f : α ≃o β) [is_complemented α] :
theorem order_iso.is_complemented_iff {α : Type u_1} {β : Type u_2} [bounded_lattice α] [bounded_lattice β] (f : α ≃o β) :