mathlib docs: order.rel

source

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

(∀ {x y : α}, r x y → s (f x) (f y)) → function.injective f

An increasing function is injective

source

structure rel_embedding {α : Type u_4} {β : Type u_5} :

(α → α → Prop) → (β → β → Prop) → Type (max u_4 u_5)

to_embedding : α ↪ β
map_rel_iff' : ∀ {a b : α}, r a b ↔ s (⇑(c.to_embedding) a) (⇑(c.to_embedding) b)

A relation embedding with respect to a given pair of relations r and s is an embedding f : α ↪ β such that r a b ↔ s (f a) (f b).

source

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

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

subtype.rel_embedding r p = {to_embedding := {to_fun := subtype.val p, inj' := _}, map_rel_iff' := _}

source

theorem preimage_equivalence {α : Sort u_1} {β : Sort u_2} (f : α → β) {s : β → β → Prop} :

equivalence s → equivalence (f ⁻¹'o s)

source

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

Equations

rel_embedding.has_coe_to_fun = {F := λ (_x : r ↪r s), α → β, coe := λ (o : r ↪r s), ⇑(o.to_embedding)}

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 : α} :

r a b ↔ s (⇑f a) (⇑f b)

source

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

⇑{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_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) → (r → s) is injective. We can't use function.injective here but mimic its signature by using ⦃e₁ e₂⦄.

source

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

r ↪r r

Equations

rel_embedding.refl r = {to_embedding := function.embedding.refl α, map_rel_iff' := _}

source

def rel_embedding.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} :

r ↪r s → s ↪r t → r ↪r t

Equations

f.trans g = {to_embedding := f.to_embedding.trans g.to_embedding, map_rel_iff' := _}

source

@[simp]

theorem rel_embedding.refl_apply {α : Type u_1} {r : α → α → Prop} (x : α) :

⇑(rel_embedding.refl r) x = x

source

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

source

def rel_embedding.rsymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :

r ↪r s → function.swap r ↪r function.swap s

a relation embedding is also a relation embedding between dual relations.

Equations

f.rsymm = {to_embedding := f.to_embedding, map_rel_iff' := _}

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

rel_embedding.preimage f s = {to_embedding := f, map_rel_iff' := _}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem rel_embedding.well_founded {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :

r ↪r s → well_founded s → well_founded r

source

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_monotone {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trichotomous α r] [is_asymm β s] (f : α → β) :

(∀ (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

rel_embedding.of_monotone f H = {to_embedding := {to_fun := f, inj' := _}, map_rel_iff' := _}

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

def rel_embedding.order_embedding_of_lt_embedding {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] :

has_lt.lt ↪r has_lt.lt → α ↪o β

Embeddings of partial orders that preserve

Equations

f.order_embedding_of_lt_embedding = {to_embedding := f.to_embedding, map_rel_iff' := _}

source

def order_embedding.lt_embedding {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

α ↪o β → has_lt.lt ↪r has_lt.lt

lt is preserved by order embeddings of preorders

Equations

f.lt_embedding = {to_embedding := f.to_embedding, map_rel_iff' := _}

source

@[simp]

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

⇑(f.lt_embedding) x = ⇑f x

source

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

a ≤ b ↔ ⇑f a ≤ ⇑f b

source

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

a < b ↔ ⇑f a < ⇑f b

source

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

acc has_lt.lt (⇑f a) → acc has_lt.lt a

source

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

α ↪o β → well_founded has_lt.lt → well_founded has_lt.lt

source

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

is_well_order α has_lt.lt

source

def order_embedding.osymm {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

α ↪o β → order_dual α ↪o order_dual β

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

Equations

f.osymm = {to_embedding := f.to_embedding, map_rel_iff' := _}

source

def fin.val.rel_embedding (n : ℕ) :

fin n ↪o ℕ

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

Equations

fin.val.rel_embedding n = {to_embedding := {to_fun := fin.val n, inj' := _}, map_rel_iff' := _}

source

def fin_fin.rel_embedding {m n : ℕ} :

m ≤ n → fin m ↪o fin n

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

Equations

fin_fin.rel_embedding h = {to_embedding := {to_fun := λ (_x : fin m), fin_fin.rel_embedding._match_1 h _x, inj' := _}, map_rel_iff' := _}
fin_fin.rel_embedding._match_1 h ⟨x, h'⟩ = ⟨x, _⟩

source

@[instance]

def fin.lt.is_well_order (n : ℕ) :

is_well_order (fin n) has_lt.lt

The ordering on fin n is a well order.

Equations

_ = _

source

structure rel_iso {α : Type u_4} {β : Type u_5} :

(α → α → Prop) → (β → β → Prop) → Type (max u_4 u_5)

to_equiv : α ≃ β
map_rel_iff' : ∀ {a b : α}, r a b ↔ s (⇑(c.to_equiv) a) (⇑(c.to_equiv) b)

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

source

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

source

def rel_iso.to_rel_embedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :

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

f.to_rel_embedding = {to_embedding := f.to_equiv.to_embedding, map_rel_iff' := _}

source

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

rel_iso.has_coe = {coe := rel_iso.to_rel_embedding s}

source

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

Equations

rel_iso.has_coe_to_fun = {F := λ (_x : r ≃r s), α → β, coe := λ (f : r ≃r s), ⇑f}

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 : α} :

r a b ↔ s (⇑f a) (⇑f b)

source

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)

source

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

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

function.injective rel_iso.to_equiv

source

theorem rel_iso.coe_fn_injective {α : 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) → (r → s) is injective. We can't use function.injective here but mimic its signature by using ⦃e₁ e₂⦄.

source

@[ext]

theorem rel_iso.ext {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {e₁ e₂ : r ≃r s} :

(∀ (x : α), ⇑e₁ x = ⇑e₂ x) → e₁ = e₂

source

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

r ≃r r

Identity map is a relation isomorphism.

Equations

rel_iso.refl r = {to_equiv := equiv.refl α, map_rel_iff' := _}

source

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

r ≃r s → s ≃r r

Inverse map of a relation isomorphism is a relation isomorphism.

Equations

f.symm = {to_equiv := f.to_equiv.symm, map_rel_iff' := _}

source

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

r ≃r s → s ≃r t → r ≃r t

Composition of two relation isomorphisms is a relation isomorphism.

Equations

f₁.trans f₂ = {to_equiv := f₁.to_equiv.trans f₂.to_equiv, map_rel_iff' := _}

source

def rel_iso.rsymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :

r ≃r s → function.swap r ≃r function.swap s

a relation isomorphism is also a relation isomorphism between dual relations.

Equations

f.rsymm = {to_equiv := f.to_equiv, map_rel_iff' := _}

source

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

⇑({to_equiv := f, map_rel_iff' := o}.symm) = ⇑(f.symm)

source

@[simp]

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

⇑(rel_iso.refl r) x = x

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) (g : s ≃r t) (a : α) :

⇑(f.trans g) a = ⇑g (⇑f a)

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

theorem rel_iso.bijective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) :

function.bijective ⇑e

source

theorem rel_iso.injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) :

function.injective ⇑e

source

theorem rel_iso.surjective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) :

function.surjective ⇑e

source

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

rel_iso.preimage f s = {to_equiv := f, map_rel_iff' := _}

source

def rel_iso.of_surjective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) :

function.surjective ⇑f → r ≃r s

A surjective relation embedding is a relation isomorphism.

Equations

rel_iso.of_surjective f H = {to_equiv := equiv.of_bijective ⇑f _, map_rel_iff' := _}

source

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

⇑(rel_iso.of_surjective f H) = ⇑f

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} :

r₁ ≃r r₂ → s₁ ≃r s₂ → sum.lex r₁ s₁ ≃r sum.lex r₂ s₂

Equations

e₁.sum_lex_congr e₂ = {to_equiv := e₁.to_equiv.sum_congr e₂.to_equiv, map_rel_iff' := _}

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} :

r₁ ≃r r₂ → s₁ ≃r s₂ → prod.lex r₁ s₁ ≃r prod.lex r₂ s₂

Equations

e₁.prod_lex_congr e₂ = {to_equiv := e₁.to_equiv.prod_congr e₂.to_equiv, map_rel_iff' := _}

source

@[instance]

def rel_iso.group {α : Type u_1} {r : α → α → Prop} :

group (r ≃r r)

Equations

rel_iso.group = {mul := λ (f₁ f₂ : r ≃r r), f₂.trans f₁, mul_assoc := _, one := rel_iso.refl r, one_mul := _, mul_one := _, inv := rel_iso.symm r, mul_left_inv := _}

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 set_coe_embedding {α : Type u_1} (p : set α) :

↥p ↪ α

A subset p : set α embeds into α

Equations

set_coe_embedding p = {to_fun := subtype.val (λ (x : α), x ∈ p), inj' := _}

source

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

↥p → ↥p → Prop

subrel r p is the inherited relation on a subset.

Equations

subrel r p = subtype.val ⁻¹'o r

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

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

subrel r p ↪r r

Equations

subrel.rel_embedding r p = {to_embedding := set_coe_embedding p, map_rel_iff' := _}

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

@[instance]

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

is_well_order ↥p (subrel r p)

Equations

_ = _

source

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 subrel s p

Restrict the codomain of a relation embedding

Equations

rel_embedding.cod_restrict p f H = {to_embedding := function.embedding.cod_restrict p f.to_embedding H, map_rel_iff' := _}

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, _⟩

source

def order_iso.osymm {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

α ≃o β → order_dual α ≃o order_dual β

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

Equations

f.osymm = {to_equiv := f.to_equiv, map_rel_iff' := _}

source

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

⇑f ⊥ = ⊥

source

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

⇑f ⊤ = ⊤

source

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

⇑f (a₁ ⊓ a₂) ≤ ⇑f a₁ ⊓ ⇑f a₂

source

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

⇑f (a₁ ⊓ a₂) = ⇑f a₁ ⊓ ⇑f a₂

source

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

⇑f a₁ ⊔ ⇑f a₂ ≤ ⇑f (a₁ ⊔ a₂)

source

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

⇑f (a₁ ⊔ a₂) = ⇑f a₁ ⊔ ⇑f a₂

mathlib documentation

order.rel_iso

General documentation

Additional documentation

Library

mathlib documentation

order.​rel_iso

General documentation

Additional documentation

Library

order.rel_iso