order.hom.basic

# Order homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

• `order_hom α β` a.k.a. `α →o β`: Preorder homomorphism. An `order_hom α β` is a function `f : α → β` such that `a₁ ≤ a₂ → f a₁ ≤ f a₂`
• `order_embedding α β` a.k.a. `α ↪o β`: Relation embedding. An `order_embedding α β` is an embedding `f : α ↪ β` such that `a ≤ b ↔ f a ≤ f b`. Defined as an abbreviation of `@rel_embedding α β (≤) (≤)`.
• `order_iso`: Relation isomorphism. An `order_iso α β` is an equivalence `f : α ≃ β` such that `a ≤ b ↔ f a ≤ f b`. Defined as an abbreviation of `@rel_iso α β (≤) (≤)`.

We also define many `order_hom`s. 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.

• `order_hom.id`: identity map as `α →o α`;
• `order_hom.curry`: an order isomorphism between `α × β →o γ` and `α →o β →o γ`;
• `order_hom.comp`: composition of two bundled monotone maps;
• `order_hom.compₘ`: composition of bundled monotone maps as a bundled monotone map;
• `order_hom.const`: constant function as a bundled monotone map;
• `order_hom.prod`: combine `α →o β` and `α →o γ` into `α →o β × γ`;
• `order_hom.prodₘ`: a more bundled version of `order_hom.prod`;
• `order_hom.prod_iso`: order isomorphism between `α →o β × γ` and `(α →o β) × (α →o γ)`;
• `order_hom.diag`: diagonal embedding of `α` into `α × α` as a bundled monotone map;
• `order_hom.on_diag`: restrict a monotone map `α →o α →o β` to the diagonal;
• `order_hom.fst`: projection `prod.fst : α × β → α` as a bundled monotone map;
• `order_hom.snd`: projection `prod.snd : α × β → β` as a bundled monotone map;
• `order_hom.prod_map`: `prod.map f g` as a bundled monotone map;
• `pi.eval_order_hom`: evaluation of a function at a point `function.eval i` as a bundled monotone map;
• `order_hom.coe_fn_hom`: coercion to function as a bundled monotone map;
• `order_hom.apply`: application of a `order_hom` at a point as a bundled monotone map;
• `order_hom.pi`: combine a family of monotone maps `f i : α →o π i` into a monotone map `α →o Π i, π i`;
• `order_hom.pi_iso`: order isomorphism between `α →o Π i, π i` and `Π i, α →o π i`;
• `order_hom.subtyle.val`: embedding `subtype.val : subtype p → α` as a bundled monotone map;
• `order_hom.dual`: reinterpret a monotone map `α →o β` as a monotone map `αᵒᵈ →o βᵒᵈ`;
• `order_hom.dual_iso`: order isomorphism between `α →o β` and `(αᵒᵈ →o βᵒᵈ)ᵒᵈ`;
• `order_iso.compl`: order isomorphism `α ≃o αᵒᵈ` given by taking complements in a boolean algebra;

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

• `order_embedding.to_order_hom`: convert `α ↪o β` to `α →o β`;
• `rel_hom.to_order_hom`: convert a `rel_hom` between strict orders to a `order_hom`.

## 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

Instances for `order_hom`
@[reducible]
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 (≤) (≤)`.

@[reducible]
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 (≤) (≤)`.

@[reducible]
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)
• coe : F α β
• inv : F β α
• left_inv : (e : F),
• right_inv : (e : F),
• coe_injective' : (e g : F),
• map_le_map_iff : (f : F) {a b : α}, f a f b a b

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

You should extend this class when you extend `order_iso`.

Instances of this typeclass
Instances of other typeclasses for `order_iso_class`
• order_iso_class.has_sizeof_inst
@[instance]
def order_iso_class.to_equiv_like (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [has_le α] [has_le β] [self : β] :
α β
@[protected, instance]
def order_iso.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [ β] :
≃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 β] [ β] :
β
Equations
@[protected]
theorem order_hom_class.monotone {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] (f : F) :
@[protected]
theorem order_hom_class.mono {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] (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 β] [ β] :
→o β)
Equations
@[simp]
theorem map_inv_le_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [ β] (f : F) {a : α} {b : β} :
a b f a
@[simp]
theorem le_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [ β] (f : F) {a : α} {b : β} :
a f a b
theorem map_lt_map_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] (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 β] [ β] (f : F) {a : α} {b : β} :
< a b < f a
@[simp]
theorem lt_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [ β] (f : F) {a : α} {b : β} :
a < 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
theorem order_hom.coe_eq {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :
f = f
@[protected, instance]
def order_hom.monotone.can_lift {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
can_lift β) →o β) coe_fn monotone

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.coe_copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem order_hom.copy_eq {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[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}  :
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 : β) :
( 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 : α × β) :
x = (f x.fst) x.snd
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 β) :
( ᾰ) = x
@[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 : β) :
( 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 : γ) :
( c).comp f = c
@[simp]
theorem order_hom.comp_const {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (γ : Type u_1) [preorder γ] (f : α →o β) (c : α) :
f.comp ( c) = (f 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 : α) :
( ᾰ) 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 : α) :
= (x, 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 γ)) :
= f.fst.prod f.snd
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_hom`s 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 : α × γ) :
(f.prod_map g) x = g 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 : ι) :
= f
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) :
→o α

`subtype.val` as a bundled monotone function.

Equations
@[protected, instance]
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 β] :
→o β) ᵒᵈ →o βᵒᵈ)

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 β) (ᾰ : αᵒᵈ) :
=
@[simp]
theorem order_hom.dual_symm_apply_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : αᵒᵈ →o βᵒᵈ) (ᾰ : α) :
@[simp]
theorem order_hom.dual_id {α : Type u_2} [preorder α] :
@[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_id {α : Type u_2} [preorder α] :
@[simp]
theorem order_hom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : βᵒᵈ →o γᵒᵈ) (f : αᵒᵈ →o βᵒᵈ) :
def order_hom.dual_iso (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :

`order_hom.dual` as an order isomorphism.

Equations
@[simp]
theorem order_hom.with_bot_map_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :
@[protected]
def order_hom.with_bot_map {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :

Lift an order homomorphism `f : α →o β` to an order homomorphism `with_bot α →o with_bot β`.

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

Lift an order homomorphism `f : α →o β` to an order homomorphism `with_top α →o with_top β`.

Equations
@[simp]
theorem order_hom.with_top_map_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :

Embeddings of partial orders that preserve `<` also preserve `≤`.

Equations
@[simp]
theorem rel_embedding.order_embedding_of_lt_embedding_apply {α : Type u_2} {β : Type u_3} {f : has_lt.lt ↪r has_lt.lt} {x : α} :
= f x
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 : α) :
(f 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 β)  :
@[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
@[protected]
def order_embedding.with_bot_map {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :

A version of `with_bot.map` for order embeddings.

Equations
@[simp]
theorem order_embedding.with_bot_map_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :
@[simp]
theorem order_embedding.with_top_map_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :
@[protected]
def order_embedding.with_top_map {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :

A version of `with_top.map` for order embeddings.

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

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} [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} [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.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 α] :
@[simp]
theorem order_iso.refl_apply {α : Type u_2} [has_le α] (x : α) :
x = 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 β) :
@[trans]
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
@[simp]
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 β) :
.trans e = e
@[simp]
theorem order_iso.trans_refl {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
e.trans = e
@[simp]
theorem order_iso.symm_trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_le α] [has_le β] [has_le γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : γ) :
((e₁.trans e₂).symm) c = (e₁.symm) ((e₂.symm) c)
theorem order_iso.symm_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_le α] [has_le β] [has_le γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
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]
theorem order_iso.coe_dual_dual (α : Type u_2) [has_le α] :
@[simp]
theorem order_iso.coe_dual_dual_symm (α : Type u_2) [has_le α] :
@[simp]
theorem order_iso.dual_dual_apply {α : Type u_2} [has_le α] (a : α) :
@[simp]
theorem order_iso.dual_dual_symm_apply {α : Type u_2} [has_le α] (a : αᵒᵈᵒᵈ) :
@[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.to_rel_iso_lt {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α ≃o β) :

Converts an `order_iso` into a `rel_iso (<) (<)`.

Equations
@[simp]
theorem order_iso.to_rel_iso_lt_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α ≃o β) (x : α) :
@[simp]
theorem order_iso.to_rel_iso_lt_symm {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α ≃o β) :
def order_iso.of_rel_iso_lt {α : Type u_1} {β : Type u_2} (e : has_lt.lt ≃r has_lt.lt) :
α ≃o β

Converts a `rel_iso (<) (<)` into an `order_iso`.

Equations
@[simp]
theorem order_iso.of_rel_iso_lt_apply {α : Type u_1} {β : Type u_2} (e : has_lt.lt ≃r has_lt.lt) (x : α) :
= e x
@[simp]
theorem order_iso.of_rel_iso_lt_symm {α : Type u_1} {β : Type u_2} (e : has_lt.lt ≃r has_lt.lt) :
@[simp]
theorem order_iso.of_rel_iso_lt_to_rel_iso_lt {α : Type u_1} {β : Type u_2} (e : α ≃o β) :
@[simp]
theorem order_iso.to_rel_iso_lt_of_rel_iso_lt {α : Type u_1} {β : Type u_2} (e : has_lt.lt ≃r has_lt.lt) :
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.of_hom_inv {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {F : Type u_1} {G : Type u_4} [ β] [ α] (f : F) (g : G) (h₁ : f.comp g = order_hom.id) (h₂ : g.comp f = order_hom.id) :
α ≃o β

To show that `f : α →o β` and `g : β →o α` make up an order isomorphism it is enough to show that `g` is the inverse of `f`

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) :
β) f =
@[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 β] :
β).symm) =
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
def strict_mono.order_iso_of_right_inverse {α : Type u_2} {β : Type u_3} [linear_order α] [preorder β] (f : α β) (h_mono : strict_mono f) (g : β α) (hg : f) :
α ≃o β

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

Equations
@[simp]
theorem strict_mono.order_iso_of_right_inverse_symm_apply {α : Type u_2} {β : Type u_3} [linear_order α] [preorder β] (f : α β) (h_mono : strict_mono f) (g : β α) (hg : f) :
(rel_iso.symm g hg)) = g
@[simp]
theorem strict_mono.order_iso_of_right_inverse_apply {α : Type u_2} {β : Type u_3} [linear_order α] [preorder β] (f : α β) (h_mono : strict_mono f) (g : β α) (hg : f) :
g hg) = f
@[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 α] (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 α] [order_bot α] [order_bot β] (f : α ≃o β) :
theorem order_iso.map_top' {α : Type u_2} {β : Type u_3} [has_le α] (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 α] [order_top α] [order_top β] (f : α ≃o β) :
theorem order_embedding.map_inf_le {α : Type u_2} {β : Type u_3} (f : α ↪o β) (x y : α) :
f (x y) f x f y
theorem order_embedding.le_map_sup {α : Type u_2} {β : Type u_3} (f : α ↪o β) (x y : α) :
f x f y f (x y)
theorem order_iso.map_inf {α : Type u_2} {β : Type u_3} (f : α ≃o β) (x y : α) :
f (x y) = f x f y
theorem order_iso.map_sup {α : Type u_2} {β : Type u_3} (f : α ≃o β) (x y : α) :
f (x y) = f x f y
theorem disjoint.map_order_iso {α : Type u_2} {β : Type u_3} [order_bot α] [order_bot β] {a b : α} (f : α ≃o β) (ha : b) :
disjoint (f a) (f b)

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

theorem codisjoint.map_order_iso {α : Type u_2} {β : Type u_3} [order_top α] [order_top β] {a b : α} (f : α ≃o β) (ha : b) :
codisjoint (f a) (f b)

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

@[simp]
theorem disjoint_map_order_iso_iff {α : Type u_2} {β : Type u_3} [order_bot α] [order_bot β] {a b : α} (f : α ≃o β) :
disjoint (f a) (f b) b
@[simp]
theorem codisjoint_map_order_iso_iff {α : Type u_2} {β : Type u_3} [order_top α] [order_top β] {a b : α} (f : α ≃o β) :
codisjoint (f a) (f b) b
@[protected]

Taking the dual then adding `⊥` is the same as adding `⊤` then taking the dual. This is the order iso form of `with_bot.of_dual`, as proven by `coe_to_dual_top_equiv_eq`.

Equations
@[simp]
theorem with_bot.to_dual_top_equiv_coe {α : Type u_2} [has_le α] (a : α) :
@[simp]
theorem with_bot.to_dual_top_equiv_symm_coe {α : Type u_2} [has_le α] (a : α) :
@[simp]
theorem with_bot.to_dual_top_equiv_bot {α : Type u_2} [has_le α] :
@[simp]
theorem with_bot.to_dual_top_equiv_symm_bot {α : Type u_2} [has_le α] :
@[protected]

Taking the dual then adding `⊤` is the same as adding `⊥` then taking the dual. This is the order iso form of `with_top.of_dual`, as proven by `coe_to_dual_bot_equiv_eq`.

Equations
@[simp]
theorem with_top.to_dual_bot_equiv_coe {α : Type u_2} [has_le α] (a : α) :
@[simp]
theorem with_top.to_dual_bot_equiv_symm_coe {α : Type u_2} [has_le α] (a : α) :
@[simp]
theorem with_top.to_dual_bot_equiv_top {α : Type u_2} [has_le α] :
@[simp]
theorem with_top.to_dual_bot_equiv_symm_top {α : Type u_2} [has_le α] :
@[simp]
theorem order_iso.with_top_congr_apply {α : Type u_2} {β : Type u_3} (e : α ≃o β) (o : option α) :
def order_iso.with_top_congr {α : Type u_2} {β : Type u_3} (e : α ≃o β) :

A version of `equiv.option_congr` for `with_top`.

Equations
@[simp]
theorem order_iso.with_top_congr_refl {α : Type u_2}  :
@[simp]
theorem order_iso.with_top_congr_symm {α : Type u_2} {β : Type u_3} (e : α ≃o β) :
@[simp]
theorem order_iso.with_top_congr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} (e₁ : α ≃o β) (e₂ : β ≃o γ) :
= (e₁.trans e₂).with_top_congr
def order_iso.with_bot_congr {α : Type u_2} {β : Type u_3} (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} (e : α ≃o β) (o : option α) :
@[simp]
theorem order_iso.with_bot_congr_refl {α : Type u_2}  :
@[simp]
theorem order_iso.with_bot_congr_symm {α : Type u_2} {β : Type u_3} (e : α ≃o β) :
@[simp]
theorem order_iso.with_bot_congr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} (e₁ : α ≃o β) (e₂ : β ≃o γ) :
= (e₁.trans e₂).with_bot_congr
theorem order_iso.is_compl {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] (f : α ≃o β) {x y : α} (h : y) :
is_compl (f x) (f y)
theorem order_iso.is_compl_iff {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] (f : α ≃o β) {x y : α} :
y is_compl (f x) (f y)
theorem order_iso.complemented_lattice {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] (f : α ≃o β)  :
theorem order_iso.complemented_lattice_iff {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] (f : α ≃o β) :