# mathlibdocumentation

order.rel_iso

@[nolint]
structure rel_hom {α : Type u_4} {β : Type u_5} :
(α → α → Prop)(β → β → 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⦄ :
(∀ (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

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

Identity map is a relation homomorphism.

Equations
def rel_hom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} :
s →r tr →r sr →r t

Composition of two relation homomorphisms is a relation homomorphism.

Equations
@[simp]
theorem rel_hom.id_apply {α : Type u_1} {r : α → α → Prop} (x : α) :

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

def rel_hom.swap {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
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) [ s] :
r

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

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} :
r →r s

theorem injective_of_increasing {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [ r] [ s] (f : α → β) :
(∀ {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} [ 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 : α → β} :
(∀ {a b : α}, r a b s (f a) (f b))

structure rel_embedding {α : Type u_4} {β : Type u_5} :
(α → α → Prop)(β → β → 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} :
equivalence (f ⁻¹'o s)

def rel_embedding.to_rel_hom {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
r ↪r sr →r s

A relation embedding is also a relation homomorphism

Equations
@[instance]
def 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_embedding.has_coe_to_fun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :

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 : α} :
r a b s (f a) (f b)

@[simp]
theorem rel_embedding.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)) :

@[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⦄ :
(∀ (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

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} :
r ↪r ss ↪r tr ↪r t

Composition of two relation embeddings is a relation embedding.

Equations
@[instance]
def rel_embedding.inhabited {α : Type u_1} (r : α → α → Prop) :

Equations
@[simp]
theorem rel_embedding.refl_apply {α : Type u_1} {r : α → α → Prop} (x : α) :
x = x

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem rel_embedding.is_strict_total_order' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r 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} :
r ↪r s

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

def rel_embedding.of_monotone {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [ r] [ s] (f : α → β) :
(∀ (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} [ r] [ s] (f : α → β) (H : ∀ (a b : α), r a bs (f a) (f b)) :
= f

def rel_embedding.order_embedding_of_lt_embedding {α : Type u_1} {β : Type u_2}  :
α ↪o β

Embeddings of partial orders that preserve < also preserve ≤

Equations
def order_embedding.lt_embedding {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
α ↪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 : α) :

theorem order_embedding.map_le_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) {a b : α} :
a b f a f b

theorem order_embedding.map_lt_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) {a b : α} :
a < b f a < f 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 : α) :
(f a)

theorem order_embedding.well_founded {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

theorem order_embedding.is_well_order {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β)  :

def order_embedding.dual {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
α ↪o β

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

Equations

The inclusion map fin n → ℕ is a relation embedding.

Equations
def fin_fin.rel_embedding {m n : } :
m nfin m ↪o fin n

The inclusion map fin m → fin n is an order embedding.

Equations
@[instance]
def fin.lt.is_well_order (n : ) :

The ordering on fin n is a well order.

structure rel_iso {α : Type u_4} {β : Type u_5} :
(α → α → Prop)(β → β → 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} :
r ≃r sr ↪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.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 : α} :
r a b s (f a) (f b)

theorem rel_iso.map_rel_iff'' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {x y : α} :
r x y s (f x) (f y)

@[simp]
theorem rel_iso.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)) :

@[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.injective_to_equiv {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :

theorem rel_iso.injective_coe_fn {α : 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⦄ :
(∀ (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.refl {α : Type u_1} (r : α → α → Prop) :
r ≃r r

Identity map is a relation isomorphism.

Equations
def rel_iso.symm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
r ≃r ss ≃r r

Inverse map of a relation isomorphism is a relation isomorphism.

Equations
def rel_iso.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} :
r ≃r ss ≃r tr ≃r t

Composition of two relation isomorphisms is a relation isomorphism.

Equations
@[instance]
def rel_iso.inhabited {α : Type u_1} (r : α → α → Prop) :

Equations
def rel_iso.swap {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :
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 : α}, r a b s (f a) (f b)) :

@[simp]
theorem rel_iso.refl_apply {α : Type u_1} {r : α → α → Prop} (x : α) :

@[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) (g : s ≃r t) (a : α) :
(f.trans g) a = g (f a)

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

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
def rel_iso.of_surjective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) :
r ≃r s

A surjective relation embedding is a relation isomorphism.

Equations
@[simp]
theorem rel_iso.of_surjective_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (H : function.surjective f) :

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} :
r₁ ≃r r₂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} :
r₁ ≃r r₂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 β] :
α ≃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.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 β) :

def set_coe_embedding {α : Type u_1} (p : set α) :
p α

A subset p : set α embeds into α

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

subrel r p is the inherited relation on a subset.

Equations
• p =
@[simp]
theorem subrel_val {α : Type u_1} (r : α → α → Prop) (p : set α) {a b : p} :
p a b r a.val b.val

def subrel.rel_embedding {α : Type u_1} (r : α → α → Prop) (p : set α) :
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) :
p) a = a.val

@[instance]
def subrel.is_well_order {α : Type u_1} (r : α → α → Prop) [ r] (p : set α) :
(subrel r p)

def rel_embedding.cod_restrict {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : set β) (f : r ↪r s) :
(∀ (a : α), f a p)r ↪r 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 : α) :
H) a = f a, _⟩

def order_iso.dual {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
α ≃o β

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

Equations
theorem order_iso.map_bot {α : Type u_1} {β : Type u_2} [order_bot α] [order_bot β] (f : α ≃o β) :

theorem rel_iso.map_top {α : Type u_1} {β : Type u_2} [order_top α] [order_top β] (f : α ≃o β) :

theorem rel_embedding.map_inf_le {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} (f : α ↪o β) :
f (a₁ a₂) f a₁ f a₂

theorem rel_iso.map_inf {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} (f : α ≃o β) :
f (a₁ a₂) = f a₁ f a₂

theorem rel_embedding.le_map_sup {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} (f : α ↪o β) :
f a₁ f a₂ f (a₁ a₂)

theorem rel_iso.map_sup {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} (f : α ≃o β) :
f (a₁ a₂) = f a₁ f a₂