mathlib documentation

order.hom.basic

Order homomorphisms #

This file defines order homomorphisms, which are bundled monotone functions. A preorder homomorphism f : α →o β is a function α → β along with a proof that ∀ x y, x ≤ y → f x ≤ f y.

Main definitions #

In this file we define the following bundled monotone maps:

We also define many order_homs. In some cases we define two versions, one with suffix and one without it (e.g., order_hom.compₘ and order_hom.comp). This means that the former function is a "more bundled" version of the latter. We can't just drop the "less bundled" version because the more bundled version usually does not work with dot notation.

We also define two functions to convert other bundled maps to α →o β:

Tags #

monotone map, bundled morphism

structure order_hom (α : Type u_6) (β : Type u_7) [preorder α] [preorder β] :
Type (max u_6 u_7)

Bundled monotone (aka, increasing) function

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 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 order_hom_class (F : Type u_1) (α : out_param (Type u_2)) (β : out_param (Type u_3)) [has_le α] [has_le β] :
Type (max u_1 u_2 u_3)

order_hom_class F α b asserts that F is a type of -preserving morphisms.

@[class]
structure order_iso_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [has_le α] [has_le β] :
Type (max u_6 u_7 u_8)

order_iso_class F α β states that F is a type of order isomorphisms.

You should extend this class when you extend order_iso.

Instances
@[protected, instance]
def order_iso.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [order_iso_class F α β] :
has_coe_t F ≃o β)
Equations
@[protected, instance]
def order_iso_class.to_order_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [order_iso_class F α β] :
Equations
@[protected]
theorem order_hom_class.monotone {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_hom_class F α β] (f : F) :
@[protected]
theorem order_hom_class.mono {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_hom_class F α β] (f : F) :
@[protected, instance]
def order_hom_class.order_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_hom_class F α β] :
has_coe_t F →o β)
Equations
@[simp]
theorem map_inv_le_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [order_iso_class F α β] (f : F) {a : α} {b : β} :
@[simp]
theorem le_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [order_iso_class F α β] (f : F) {a : α} {b : β} :
theorem map_lt_map_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_iso_class F α β] (f : F) {a b : α} :
f a < f b a < b
@[simp]
theorem map_inv_lt_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_iso_class F α β] (f : F) {a : α} {b : β} :
equiv_like.inv f b < a b < f a
@[simp]
theorem lt_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_iso_class F α β] (f : F) {a : α} {b : β} :
a < equiv_like.inv f b f a < b
@[protected, instance]
def order_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
has_coe_to_fun →o β) (λ (_x : α →o β), α → β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[protected]
theorem order_hom.monotone {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :
@[protected]
theorem order_hom.mono {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :
@[protected, instance]
def order_hom.order_hom_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
order_hom_class →o β) α β
Equations
@[simp]
theorem order_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f : α →o β} :
@[simp]
theorem order_hom.coe_fun_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :
{to_fun := f, monotone' := hf} = f
@[ext]
theorem order_hom.ext {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f g : α →o β) (h : f = g) :
f = g
@[protected, instance]
def order_hom.can_lift {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
can_lift (α → β) →o β)

One can lift an unbundled monotone function to a bundled one.

Equations
@[protected]
def order_hom.copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) (f' : α → β) (h : f' = f) :
α →o β

Copy of an order_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem order_hom.id_coe {α : Type u_2} [preorder α] :
def order_hom.id {α : Type u_2} [preorder α] :
α →o α

The identity function as bundled monotone function.

Equations
@[protected, instance]
def order_hom.inhabited {α : Type u_2} [preorder α] :
inhabited →o α)
Equations
@[protected, instance]
def order_hom.preorder {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
preorder →o β)

The preorder structure of α →o β is pointwise inequality: f ≤ g ↔ ∀ a, f a ≤ g a.

Equations
@[protected, instance]
def order_hom.partial_order {α : Type u_2} [preorder α] {β : Type u_1} [partial_order β] :
Equations
theorem order_hom.le_def {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f g : α →o β} :
f g ∀ (x : α), f x g x
@[simp, norm_cast]
theorem order_hom.coe_le_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f g : α →o β} :
f g f g
@[simp]
theorem order_hom.mk_le_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f g : α → β} {hf : monotone f} {hg : monotone g} :
{to_fun := f, monotone' := hf} {to_fun := g, monotone' := hg} f g
theorem order_hom.apply_mono {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f g : α →o β} {x y : α} (h₁ : f g) (h₂ : x y) :
f x g y
def order_hom.curry {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] :
× β →o γ) ≃o →o β →o γ)

Curry/uncurry as an order isomorphism between α × β →o γ and α →o β →o γ.

Equations
@[simp]
theorem order_hom.curry_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : α × β →o γ) (x : α) (y : β) :
((order_hom.curry f) x) y = f (x, y)
@[simp]
theorem order_hom.curry_symm_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : α →o β →o γ) (x : α × β) :
def order_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : β →o γ) (f : α →o β) :
α →o γ

The composition of two bundled monotone functions.

Equations
@[simp]
theorem order_hom.comp_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : β →o γ) (f : α →o β) :
(g.comp f) = g f
theorem order_hom.comp_mono {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] ⦃g₁ g₂ : β →o γ⦄ (hg : g₁ g₂) ⦃f₁ f₂ : α →o β⦄ (hf : f₁ f₂) :
g₁.comp f₁ g₂.comp f₂
def order_hom.compₘ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] :
→o γ) →o →o β) →o α →o γ

The composition of two bundled monotone functions, a fully bundled version.

Equations
@[simp]
theorem order_hom.compₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (x : β →o γ) (ᾰ : α →o β) :
@[simp]
theorem order_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :
@[simp]
theorem order_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :
@[simp]
theorem order_hom.const_coe_coe (α : Type u_1) [preorder α] {β : Type u_2} [preorder β] (b : β) :
def order_hom.const (α : Type u_1) [preorder α] {β : Type u_2} [preorder β] :
β →o α →o β

Constant function bundled as a order_hom.

Equations
@[simp]
theorem order_hom.const_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : α →o β) (c : γ) :
@[simp]
theorem order_hom.comp_const {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (γ : Type u_1) [preorder γ] (f : α →o β) (c : α) :
@[protected]
def order_hom.prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : α →o β) (g : α →o γ) :
α →o β × γ

Given two bundled monotone maps f, g, f.prod g is the map x ↦ (f x, g x) bundled as a order_hom.

Equations
@[simp]
theorem order_hom.prod_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : α →o β) (g : α →o γ) (x : α) :
(f.prod g) x = (f x, g x)
theorem order_hom.prod_mono {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] {f₁ f₂ : α →o β} (hf : f₁ f₂) {g₁ g₂ : α →o γ} (hg : g₁ g₂) :
f₁.prod g₁ f₂.prod g₂
theorem order_hom.comp_prod_comp_same {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f₁ f₂ : β →o γ) (g : α →o β) :
(f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g
@[simp]
theorem order_hom.prodₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (x : α →o β) (ᾰ : α →o γ) (x_1 : α) :
((order_hom.prodₘ x) ᾰ) x_1 = (x x_1, ᾰ x_1)
def order_hom.prodₘ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] :
→o β) →o →o γ) →o α →o β × γ

Given two bundled monotone maps f, g, f.prod g is the map x ↦ (f x, g x) bundled as a order_hom. This is a fully bundled version.

Equations
@[simp]
theorem order_hom.diag_coe {α : Type u_2} [preorder α] (x : α) :
def order_hom.diag {α : Type u_2} [preorder α] :
α →o α × α

Diagonal embedding of α into α × α as a order_hom.

Equations
@[simp]
theorem order_hom.on_diag_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o α →o β) (ᾰ : α) :
(f.on_diag) ᾰ = (f ᾰ)
def order_hom.on_diag {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o α →o β) :
α →o β

Restriction of f : α →o α →o β to the diagonal.

Equations
def order_hom.fst {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
α × β →o α

prod.fst as a order_hom.

Equations
@[simp]
theorem order_hom.fst_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (self : α × β) :
def order_hom.snd {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
α × β →o β

prod.snd as a order_hom.

Equations
@[simp]
theorem order_hom.snd_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (self : α × β) :
@[simp]
theorem order_hom.fst_prod_snd {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
@[simp]
theorem order_hom.fst_comp_prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : α →o β) (g : α →o γ) :
@[simp]
theorem order_hom.snd_comp_prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : α →o β) (g : α →o γ) :
def order_hom.prod_iso {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] :
→o β × γ) ≃o →o β) × →o γ)

Order isomorphism between the space of monotone maps to β × γ and the product of the spaces of monotone maps to β and γ.

Equations
@[simp]
theorem order_hom.prod_iso_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : α →o β × γ) :
@[simp]
theorem order_hom.prod_iso_symm_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : →o β) × →o γ)) :
def order_hom.prod_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [preorder α] [preorder β] [preorder γ] [preorder δ] (f : α →o β) (g : γ →o δ) :
α × γ →o β × δ

prod.map of two order_homs as a order_hom.

Equations
@[simp]
theorem order_hom.prod_map_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [preorder α] [preorder β] [preorder γ] [preorder δ] (f : α →o β) (g : γ →o δ) (x : α × γ) :
def pi.eval_order_hom {ι : Type u_6} {π : ι → Type u_7} [Π (i : ι), preorder (π i)] (i : ι) :
(Π (j : ι), π j) →o π i

Evaluation of an unbundled function at a point (function.eval) as a order_hom.

Equations
@[simp]
theorem pi.eval_order_hom_coe {ι : Type u_6} {π : ι → Type u_7} [Π (i : ι), preorder (π i)] (i : ι) :
@[simp]
theorem order_hom.coe_fn_hom_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
def order_hom.coe_fn_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
→o β) →o α → β

The "forgetful functor" from α →o β to α → β that takes the underlying function, is monotone.

Equations
def order_hom.apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (x : α) :
→o β) →o β

Function application λ f, f a (for fixed a) is a monotone function from the monotone function space α →o β to β. See also pi.eval_order_hom.

Equations
@[simp]
theorem order_hom.apply_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (x : α) :
def order_hom.pi {α : Type u_2} [preorder α] {ι : Type u_6} {π : ι → Type u_7} [Π (i : ι), preorder (π i)] (f : Π (i : ι), α →o π i) :
α →o Π (i : ι), π i

Construct a bundled monotone map α →o Π i, π i from a family of monotone maps f i : α →o π i.

Equations
@[simp]
theorem order_hom.pi_coe {α : Type u_2} [preorder α] {ι : Type u_6} {π : ι → Type u_7} [Π (i : ι), preorder (π i)] (f : Π (i : ι), α →o π i) (x : α) (i : ι) :
(order_hom.pi f) x i = (f i) x
@[simp]
theorem order_hom.pi_iso_symm_apply {α : Type u_2} [preorder α] {ι : Type u_6} {π : ι → Type u_7} [Π (i : ι), preorder (π i)] (f : Π (i : ι), α →o (λ (i : ι), π i) i) :
@[simp]
theorem order_hom.pi_iso_apply {α : Type u_2} [preorder α] {ι : Type u_6} {π : ι → Type u_7} [Π (i : ι), preorder (π i)] (f : α →o Π (i : ι), π i) (i : ι) :
def order_hom.pi_iso {α : Type u_2} [preorder α] {ι : Type u_6} {π : ι → Type u_7} [Π (i : ι), preorder (π i)] :
→o Π (i : ι), π i) ≃o Π (i : ι), α →o π i

Order isomorphism between bundled monotone maps α →o Π i, π i and families of bundled monotone maps Π i, α →o π i.

Equations
@[simp]
theorem order_hom.subtype.val_coe {α : Type u_2} [preorder α] (p : α → Prop) :
def order_hom.subtype.val {α : Type u_2} [preorder α] (p : α → Prop) :

subtype.val as a bundled monotone function.

Equations
def order_hom.unique {α : Type u_2} [preorder α] [subsingleton α] :
unique →o α)

There is a unique monotone map from a subsingleton to itself.

Equations
theorem order_hom.order_hom_eq_id {α : Type u_2} [preorder α] [subsingleton α] (g : α →o α) :
@[protected]
def order_hom.dual {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :

Reinterpret a bundled monotone function as a monotone function between dual orders.

Equations
@[simp]
theorem order_hom.dual_apply_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) (ᾰ : order_dual α) :
@[simp]
theorem order_hom.dual_symm_apply_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : order_dual α →o order_dual β) (ᾰ : α) :
@[simp]
theorem order_hom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : β →o γ) (f : α →o β) :
@[simp]
theorem order_hom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : order_dual β →o order_dual γ) (f : order_dual α →o order_dual β) :
def order_hom.dual_iso (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :

order_hom.dual as an order isomorphism.

Equations
def rel_embedding.order_embedding_of_lt_embedding {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :

< is preserved by order embeddings of preorders.

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

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

Equations
def order_embedding.of_map_le_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_le_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_2} [preorder α] (p : α → Prop) :
def order_embedding.subtype {α : Type u_2} [preorder α] (p : α → Prop) :

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

Equations
def order_embedding.to_order_hom {X : Type u_1} {Y : Type u_2} [preorder X] [preorder Y] (f : X ↪o Y) :
X →o Y

Convert an order_embedding to a order_hom.

Equations
@[simp]
theorem order_embedding.to_order_hom_coe {X : Type u_1} {Y : Type u_2} [preorder X] [preorder Y] (f : X ↪o Y) :
def rel_hom.to_order_hom {α : Type u_2} {β : Type u_3} [partial_order α] [preorder β] (f : has_lt.lt →r has_lt.lt) :
α →o β

A bundled expression of the fact that a map between partial orders that is strictly monotone is weakly monotone.

Equations
@[simp]
theorem rel_hom.to_order_hom_coe {α : Type u_2} {β : Type u_3} [partial_order α] [preorder β] (f : has_lt.lt →r has_lt.lt) :
@[protected, instance]
def order_iso.order_iso_class {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] :
order_iso_class ≃o β) α β
Equations
@[simp]
theorem order_iso.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] {f : α ≃o β} :
@[ext]
theorem order_iso.ext {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] {f g : α ≃o β} (h : f = g) :
f = g
def order_iso.to_order_embedding {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
@[protected]
theorem order_iso.bijective {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
@[protected]
theorem order_iso.injective {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
@[protected]
theorem order_iso.surjective {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
@[simp]
theorem order_iso.range_eq {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
@[simp]
theorem order_iso.apply_eq_iff_eq {α : Type u_2} {β : Type u_3} [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_2} [has_le α] :
theorem order_iso.refl_apply {α : Type u_2} [has_le α] (x : α) :
@[simp]
theorem order_iso.refl_to_equiv {α : Type u_2} [has_le α] :
def order_iso.symm {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
β ≃o α

Inverse of an order isomorphism.

Equations
@[simp]
theorem order_iso.apply_symm_apply {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (x : β) :
e ((e.symm) x) = x
@[simp]
theorem order_iso.symm_apply_apply {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (x : α) (y : β) :
e x = y x = (e.symm) y
theorem order_iso.symm_apply_eq {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) {x : α} {y : β} :
(e.symm) y = x y = e x
@[simp]
theorem order_iso.symm_symm {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
e.symm.symm = e
theorem order_iso.symm_injective {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] :
@[simp]
theorem order_iso.to_equiv_symm {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
@[simp]
theorem order_iso.symm_image_image {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
(e.symm) '' (e '' s) = s
@[simp]
theorem order_iso.image_symm_image {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set β) :
e '' ((e.symm) '' s) = s
theorem order_iso.image_eq_preimage {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
e '' s = (e.symm) ⁻¹' s
@[simp]
theorem order_iso.preimage_symm_preimage {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
@[simp]
theorem order_iso.symm_preimage_preimage {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set β) :
@[simp]
theorem order_iso.image_preimage {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set β) :
e '' (e ⁻¹' s) = s
@[simp]
theorem order_iso.preimage_image {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
e ⁻¹' (e '' s) = s
def order_iso.trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [has_le α] [has_le β] [has_le γ] (e : α ≃o β) (e' : β ≃o γ) :
(e.trans e') = e' e
theorem order_iso.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
@[simp]
theorem order_iso.trans_refl {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
def order_iso.prod_comm {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] :
α × β ≃o β × α

prod.swap as an order_iso.

Equations
@[simp]
theorem order_iso.coe_prod_comm {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] :
@[simp]
theorem order_iso.prod_comm_symm {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] :
def order_iso.dual_dual (α : Type u_2) [has_le α] :

The order isomorphism between a type and its double dual.

Equations
@[simp]
@[simp]
theorem order_iso.le_iff_le {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) {x y : α} :
e x e y x y
theorem order_iso.le_symm_apply {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) {x : α} {y : β} :
x (e.symm) y e x y
theorem order_iso.symm_apply_le {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) {x : α} {y : β} :
(e.symm) y x y e x
@[protected]
theorem order_iso.monotone {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α ≃o β) :
@[protected]
theorem order_iso.strict_mono {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α ≃o β) :
@[simp]
theorem order_iso.lt_iff_lt {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α ≃o β) {x y : α} :
e x < e y x < y
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_2} [preorder α] (s t : set α) (h : s = t) :

Order isomorphism between two equal sets.

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

Order isomorphism between univ : set α and α.

Equations
def order_iso.fun_unique (α : Type u_1) (β : Type u_2) [unique α] [preorder β] :
(α → β) ≃o β

Order isomorphism between α → β and β, where α has a unique element.

Equations
@[simp]
theorem order_iso.fun_unique_apply (α : Type u_1) (β : Type u_2) [unique α] [preorder β] (f : Π (x : α), (λ (a' : α), (λ (ᾰ : α), β) a') x) :
@[simp]
theorem order_iso.fun_unique_to_equiv (α : Type u_1) (β : Type u_2) [unique α] [preorder β] :
@[simp]
theorem order_iso.fun_unique_symm_apply {α : Type u_1} {β : Type u_2} [unique α] [preorder β] :
def equiv.to_order_iso {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α β) (h₁ : monotone e) (h₂ : monotone (e.symm)) :
α ≃o β

If e is an equivalence with monotone forward and inverse maps, then e is an order isomorphism.

Equations
@[simp]
theorem equiv.coe_to_order_iso {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α β) (h₁ : monotone e) (h₂ : monotone (e.symm)) :
(e.to_order_iso h₁ h₂) = e
@[simp]
theorem equiv.to_order_iso_to_equiv {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α β) (h₁ : monotone e) (h₂ : monotone (e.symm)) :
(e.to_order_iso h₁ h₂).to_equiv = e
@[protected]
noncomputable def strict_mono_on.order_iso {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] (f : α → β) (s : set α) (hf : strict_mono_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
@[protected]
noncomputable 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
noncomputable 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 strict_mono.order_iso_of_right_inverse {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] (f : α → β) (h_mono : strict_mono f) (g : β → α) (hg : function.right_inverse g f) :
α ≃o β

A strictly monotone function with a right inverse is an order isomorphism.

Equations
@[protected]
def order_iso.dual {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (f : α ≃o β) :

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

Equations
theorem order_iso.map_bot' {α : Type u_2} {β : Type u_3} [has_le α] [partial_order β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ (x' : α), x x') (hy : ∀ (y' : β), y y') :
f x = y
theorem order_iso.map_bot {α : Type u_2} {β : Type u_3} [has_le α] [partial_order β] [order_bot α] [order_bot β] (f : α ≃o β) :
theorem order_iso.map_top' {α : Type u_2} {β : Type u_3} [has_le α] [partial_order β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ (x' : α), x' x) (hy : ∀ (y' : β), y' y) :
f x = y
theorem order_iso.map_top {α : Type u_2} {β : Type u_3} [has_le α] [partial_order β] [order_top α] [order_top β] (f : α ≃o β) :
theorem order_embedding.map_inf_le {α : Type u_2} {β : Type u_3} [semilattice_inf α] [semilattice_inf β] (f : α ↪o β) (x y : α) :
f (x y) f x f y
theorem order_iso.map_inf {α : Type u_2} {β : Type u_3} [semilattice_inf α] [semilattice_inf β] (f : α ≃o β) (x y : α) :
f (x y) = f x f y
theorem disjoint.map_order_iso {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_bot α] [semilattice_inf β] [order_bot β] {a b : α} (f : α ≃o β) (ha : disjoint a b) :
disjoint (f a) (f b)

Note that this goal could also be stated (disjoint on f) a b

@[simp]
theorem disjoint_map_order_iso_iff {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_bot α] [semilattice_inf β] [order_bot β] {a b : α} (f : α ≃o β) :
disjoint (f a) (f b) disjoint a b
theorem order_embedding.le_map_sup {α : Type u_2} {β : Type u_3} [semilattice_sup α] [semilattice_sup β] (f : α ↪o β) (x y : α) :
f x f y f (x y)
theorem order_iso.map_sup {α : Type u_2} {β : Type u_3} [semilattice_sup α] [semilattice_sup β] (f : α ≃o β) (x y : α) :
f (x y) = f x f y
@[protected]
def with_bot.to_dual_top {α : Type u_2} [has_le α] :

Taking the dual then adding is the same as adding then taking the dual.

Equations
@[protected]
def with_top.to_dual_bot {α : Type u_2} [has_le α] :

Taking the dual then adding is the same as adding then taking the dual.

Equations
@[simp]
theorem order_iso.with_top_congr_apply {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) (o : option α) :
def order_iso.with_top_congr {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) :

A version of equiv.option_congr for with_top.

Equations
@[simp]
theorem order_iso.with_top_congr_symm {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) :
@[simp]
theorem order_iso.with_top_congr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [partial_order α] [partial_order β] [partial_order γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
def order_iso.with_bot_congr {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) :

A version of equiv.option_congr for with_bot.

Equations
@[simp]
theorem order_iso.with_bot_congr_apply {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) (o : option α) :
@[simp]
theorem order_iso.with_bot_congr_symm {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) :
@[simp]
theorem order_iso.with_bot_congr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [partial_order α] [partial_order β] [partial_order γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
theorem order_iso.is_compl {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) {x y : α} (h : is_compl x y) :
is_compl (f x) (f y)
theorem order_iso.is_compl_iff {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) {x y : α} :
is_compl x y is_compl (f x) (f y)
theorem order_iso.is_complemented {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) [is_complemented α] :
theorem order_iso.is_complemented_iff {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) :
@[simp]
theorem order_iso.compl_apply (α : Type u_2) [boolean_algebra α] (ᾰ : α) :
def order_iso.compl (α : Type u_2) [boolean_algebra α] :

Taking complements as an order isomorphism to the order dual.

Equations
@[simp]
theorem compl_strict_anti (α : Type u_2) [boolean_algebra α] :
theorem compl_antitone (α : Type u_2) [boolean_algebra α] :