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

• OrderHom α β a.k.a. α →o β: Preorder homomorphism. An OrderHom α β is a function f : α → β such that a₁ ≤ a₂ → f a₁ ≤ f a₂
• OrderEmbedding α β a.k.a. α ↪o β: Relation embedding. An OrderEmbedding α β is an embedding f : α ↪ β such that a ≤ b ↔ f a ≤ f b. Defined as an abbreviation of @RelEmbedding α β (≤) (≤).
• OrderIso: Relation isomorphism. An OrderIso α β is an equivalence f : α ≃ β such that a ≤ b ↔ f a ≤ f b. Defined as an abbreviation of @RelIso α β (≤) (≤).

We also define many OrderHoms. In some cases we define two versions, one with ₘ suffix and one without it (e.g., OrderHom.compₘ and OrderHom.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.

• OrderHom.id: identity map as α →o α;
• OrderHom.curry: an order isomorphism between α × β →o γ and α →o β →o γ;
• OrderHom.comp: composition of two bundled monotone maps;
• OrderHom.compₘ: composition of bundled monotone maps as a bundled monotone map;
• OrderHom.const: constant function as a bundled monotone map;
• OrderHom.prod: combine α →o β and α →o γ into α →o β × γ;
• OrderHom.prodₘ: a more bundled version of OrderHom.prod;
• OrderHom.prodIso: order isomorphism between α →o β × γ and (α →o β) × (α →o γ);
• OrderHom.diag: diagonal embedding of α into α × α as a bundled monotone map;
• OrderHom.onDiag: restrict a monotone map α →o α →o β to the diagonal;
• OrderHom.fst: projection Prod.fst : α × β → α as a bundled monotone map;
• OrderHom.snd: projection Prod.snd : α × β → β as a bundled monotone map;
• OrderHom.prodMap: prod.map f g as a bundled monotone map;
• Pi.evalOrderHom: evaluation of a function at a point Function.eval i as a bundled monotone map;
• OrderHom.coeFnHom: coercion to function as a bundled monotone map;
• OrderHom.apply: application of an OrderHom at a point as a bundled monotone map;
• OrderHom.pi: combine a family of monotone maps f i : α →o π i into a monotone map α →o Π i, π i;
• OrderHom.piIso: order isomorphism between α →o Π i, π i and Π i, α →o π i;
• OrderHom.subtype.val: embedding Subtype.val : Subtype p → α as a bundled monotone map;
• OrderHom.dual: reinterpret a monotone map α →o β as a monotone map αᵒᵈ →o βᵒᵈ;
• OrderHom.dualIso: order isomorphism between α →o β and (αᵒᵈ →o βᵒᵈ)ᵒᵈ;
• OrderHom.compl: order isomorphism α ≃o αᵒᵈ given by taking complements in a boolean algebra;

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

• OrderEmbedding.toOrderHom: convert α ↪o β to α →o β;
• RelHom.toOrderHom: convert a RelHom between strict orders to an OrderHom.

## Tags #

monotone map, bundled morphism

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

Bundled monotone (aka, increasing) function

• toFun : αβ

The underlying function of an OrderHom.

• monotone' : Monotone self.toFun

The underlying function of an OrderHom is monotone.

Instances For
theorem OrderHom.monotone' {α : Type u_6} {β : Type u_7} [] [] (self : α →o β) :
Monotone self.toFun

The underlying function of an OrderHom is monotone.

Notation for an OrderHom.

Equations
Instances For
@[reducible, inline]
abbrev OrderEmbedding (α : Type u_6) (β : Type u_7) [LE α] [LE β] :
Type (max u_6 u_7)

An order embedding is an embedding f : α ↪ β such that a ≤ b ↔ (f a) ≤ (f b). This definition is an abbreviation of RelEmbedding (≤) (≤).

Equations
• (α ↪o β) = ((fun (x x_1 : α) => x x_1) ↪r fun (x x_1 : β) => x x_1)
Instances For

Notation for an OrderEmbedding.

Equations
Instances For
@[reducible, inline]
abbrev OrderIso (α : Type u_6) (β : Type u_7) [LE α] [LE β] :
Type (max u_6 u_7)

An order isomorphism is an equivalence such that a ≤ b ↔ (f a) ≤ (f b). This definition is an abbreviation of RelIso (≤) (≤).

Equations
• (α ≃o β) = ((fun (x x_1 : α) => x x_1) ≃r fun (x x_1 : β) => x x_1)
Instances For

Notation for an OrderIso.

Equations
Instances For
@[reducible, inline]
abbrev OrderHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [LE α] [LE β] [FunLike F α β] :

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

Equations
Instances For
class OrderIsoClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [LE α] [LE β] [EquivLike F α β] :

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

You should extend this class when you extend OrderIso.

• map_le_map_iff : ∀ (f : F) {a b : α}, f a f b a b

An order isomorphism respects ≤.

Instances
@[simp]
theorem OrderIsoClass.map_le_map_iff {F : Type u_6} {α : Type u_7} {β : Type u_8} [LE α] [LE β] [EquivLike F α β] [self : ] (f : F) {a : α} {b : α} :
f a f b a b

An order isomorphism respects ≤.

def OrderIsoClass.toOrderIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [] (f : F) :
α ≃o β

Turn an element of a type F satisfying OrderIsoClass F α β into an actual OrderIso. This is declared as the default coercion from F to α ≃o β.

Equations
• f = let __src := f; { toEquiv := __src, map_rel_iff' := }
Instances For
instance instCoeTCOrderIsoOfOrderIsoClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [] :
CoeTC F (α ≃o β)

Any type satisfying OrderIsoClass can be cast into OrderIso via OrderIsoClass.toOrderIso.

Equations
• instCoeTCOrderIsoOfOrderIsoClass = { coe := OrderIsoClass.toOrderIso }
@[instance 100]
instance OrderIsoClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [] :
Equations
• =
theorem OrderHomClass.monotone {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] (f : F) :
theorem OrderHomClass.mono {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] (f : F) :
def OrderHomClass.toOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] (f : F) :
α →o β

Turn an element of a type F satisfying OrderHomClass F α β into an actual OrderHom. This is declared as the default coercion from F to α →o β.

Equations
• f = { toFun := f, monotone' := }
Instances For
instance OrderHomClass.instCoeTCOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] :
CoeTC F (α →o β)

Any type satisfying OrderHomClass can be cast into OrderHom via OrderHomClass.toOrderHom.

Equations
• OrderHomClass.instCoeTCOrderHom = { coe := OrderHomClass.toOrderHom }
@[simp]
theorem map_inv_le_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [] (f : F) {a : α} {b : β} :
a b f a
@[simp]
theorem le_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [] (f : F) {a : α} {b : β} :
a f a b
theorem map_lt_map_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [EquivLike 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} [] [] [EquivLike F α β] [] (f : F) {a : α} {b : β} :
< a b < f a
@[simp]
theorem lt_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [EquivLike F α β] [] (f : F) {a : α} {b : β} :
a < f a < b
instance OrderHom.instFunLike {α : Type u_2} {β : Type u_3} [] [] :
FunLike (α →o β) α β
Equations
• OrderHom.instFunLike = { coe := OrderHom.toFun, coe_injective' := }
instance OrderHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [] [] :
OrderHomClass (α →o β) α β
Equations
• =
@[simp]
theorem OrderHom.coe_mk {α : Type u_2} {β : Type u_3} [] [] (f : αβ) (hf : ) :
{ toFun := f, monotone' := hf } = f
theorem OrderHom.monotone {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :
theorem OrderHom.mono {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :
def OrderHom.Simps.coe {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :
αβ

See Note [custom simps projection]. We give this manually so that we use toFun as the projection directly instead.

Equations
Instances For
@[simp]
theorem OrderHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :
f.toFun = f
theorem OrderHom.ext {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) (g : α →o β) (h : f = g) :
f = g
@[simp]
theorem OrderHom.coe_eq {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :
f = f
@[simp]
theorem OrderHomClass.coe_coe {α : Type u_2} {β : Type u_3} [] [] {F : Type u_6} [FunLike F α β] [] (f : F) :
f = f
instance OrderHom.canLift {α : Type u_2} {β : Type u_3} [] [] :
CanLift (αβ) (α →o β) DFunLike.coe Monotone

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

Equations
• =
def OrderHom.copy {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) (f' : αβ) (h : f' = f) :
α →o β

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

Equations
• f.copy f' h = { toFun := f', monotone' := }
Instances For
@[simp]
theorem OrderHom.coe_copy {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem OrderHom.copy_eq {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) (f' : αβ) (h : f' = f) :
f.copy f' h = f
@[simp]
theorem OrderHom.id_coe {α : Type u_2} [] :
OrderHom.id = id
def OrderHom.id {α : Type u_2} [] :
α →o α

The identity function as bundled monotone function.

Equations
• OrderHom.id = { toFun := id, monotone' := }
Instances For
instance OrderHom.instInhabited {α : Type u_2} [] :
Inhabited (α →o α)
Equations
• OrderHom.instInhabited = { default := OrderHom.id }
instance OrderHom.instPreorder {α : Type u_2} {β : Type u_3} [] [] :
Preorder (α →o β)

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

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem OrderHom.curry_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : α × β →o γ) (x : α) (y : β) :
((OrderHom.curry f) x) y = f (x, y)
@[simp]
theorem OrderHom.curry_symm_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : α →o β →o γ) (x : α × β) :
((RelIso.symm OrderHom.curry) f) x = (f x.1) x.2
@[simp]
theorem OrderHom.comp_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (g : β →o γ) (f : α →o β) :
(g.comp f) = g f
def OrderHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (g : β →o γ) (f : α →o β) :
α →o γ

The composition of two bundled monotone functions.

Equations
• g.comp f = { toFun := g f, monotone' := }
Instances For
theorem OrderHom.comp_mono {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] ⦃g₁ : β →o γ ⦃g₂ : β →o γ (hg : g₁ g₂) ⦃f₁ : α →o β ⦃f₂ : α →o β (hf : f₁ f₂) :
g₁.comp f₁ g₂.comp f₂
@[simp]
theorem OrderHom.compₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (x : β →o γ) :
∀ (a : α →o β), ((OrderHom.compₘ x) a) = x a
def OrderHom.compₘ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] :
(β →o γ) →o (α →o β) →o α →o γ

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

Equations
• OrderHom.compₘ = OrderHom.curry { toFun := fun (f : (β →o γ) × (α →o β)) => f.1.comp f.2, monotone' := }
Instances For
@[simp]
theorem OrderHom.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :
f.comp OrderHom.id = f
@[simp]
theorem OrderHom.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :
OrderHom.id.comp f = f
@[simp]
theorem OrderHom.const_coe_coe (α : Type u_6) [] {β : Type u_7} [] (b : β) :
(() b) =
def OrderHom.const (α : Type u_6) [] {β : Type u_7} [] :
β →o α →o β

Constant function bundled as an OrderHom.

Equations
• = { toFun := fun (b : β) => { toFun := , monotone' := }, monotone' := }
Instances For
@[simp]
theorem OrderHom.const_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : α →o β) (c : γ) :
(() c).comp f = () c
@[simp]
theorem OrderHom.comp_const {α : Type u_2} {β : Type u_3} [] [] (γ : Type u_6) [] (f : α →o β) (c : α) :
f.comp (() c) = () (f c)
@[simp]
theorem OrderHom.prod_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : α →o β) (g : α →o γ) (x : α) :
(f.prod g) x = (f x, g x)
def OrderHom.prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (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 OrderHom.

Equations
• f.prod g = { toFun := fun (x : α) => (f x, g x), monotone' := }
Instances For
theorem OrderHom.prod_mono {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f₁ : α →o β} {f₂ : α →o β} (hf : f₁ f₂) {g₁ : α →o γ} {g₂ : α →o γ} (hg : g₁ g₂) :
f₁.prod g₁ f₂.prod g₂
theorem OrderHom.comp_prod_comp_same {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f₁ : β →o γ) (f₂ : β →o γ) (g : α →o β) :
(f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g
@[simp]
theorem OrderHom.prodₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (x : α →o β) :
∀ (a : α →o γ) (x_1 : α), ((OrderHom.prodₘ x) a) x_1 = (x x_1, a x_1)
def OrderHom.prodₘ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] :
(α →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 OrderHom. This is a fully bundled version.

Equations
• OrderHom.prodₘ = OrderHom.curry { toFun := fun (f : (α →o β) × (α →o γ)) => f.1.prod f.2, monotone' := }
Instances For
@[simp]
theorem OrderHom.diag_coe {α : Type u_2} [] (x : α) :
OrderHom.diag x = (x, x)
def OrderHom.diag {α : Type u_2} [] :
α →o α × α

Diagonal embedding of α into α × α as an OrderHom.

Equations
• OrderHom.diag = OrderHom.id.prod OrderHom.id
Instances For
@[simp]
theorem OrderHom.onDiag_coe {α : Type u_2} {β : Type u_3} [] [] (f : α →o α →o β) :
∀ (a : α), f.onDiag a = (f a) a
def OrderHom.onDiag {α : Type u_2} {β : Type u_3} [] [] (f : α →o α →o β) :
α →o β

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

Equations
• f.onDiag = ((RelIso.symm OrderHom.curry) f).comp OrderHom.diag
Instances For
@[simp]
theorem OrderHom.fst_coe {α : Type u_2} {β : Type u_3} [] [] (self : α × β) :
OrderHom.fst self = self.1
def OrderHom.fst {α : Type u_2} {β : Type u_3} [] [] :
α × β →o α

Prod.fst as an OrderHom.

Equations
• OrderHom.fst = { toFun := Prod.fst, monotone' := }
Instances For
@[simp]
theorem OrderHom.snd_coe {α : Type u_2} {β : Type u_3} [] [] (self : α × β) :
OrderHom.snd self = self.2
def OrderHom.snd {α : Type u_2} {β : Type u_3} [] [] :
α × β →o β

Prod.snd as an OrderHom.

Equations
• OrderHom.snd = { toFun := Prod.snd, monotone' := }
Instances For
@[simp]
theorem OrderHom.fst_prod_snd {α : Type u_2} {β : Type u_3} [] [] :
OrderHom.fst.prod OrderHom.snd = OrderHom.id
@[simp]
theorem OrderHom.fst_comp_prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : α →o β) (g : α →o γ) :
OrderHom.fst.comp (f.prod g) = f
@[simp]
theorem OrderHom.snd_comp_prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : α →o β) (g : α →o γ) :
OrderHom.snd.comp (f.prod g) = g
@[simp]
theorem OrderHom.prodIso_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : α →o β × γ) :
OrderHom.prodIso f = (OrderHom.fst.comp f, OrderHom.snd.comp f)
@[simp]
theorem OrderHom.prodIso_symm_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : (α →o β) × (α →o γ)) :
(RelIso.symm OrderHom.prodIso) f = f.1.prod f.2
def OrderHom.prodIso {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] :
(α →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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem OrderHom.prodMap_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] (f : α →o β) (g : γ →o δ) :
∀ (a : α × γ), (f.prodMap g) a = Prod.map (f) (g) a
def OrderHom.prodMap {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] (f : α →o β) (g : γ →o δ) :
α × γ →o β × δ

Prod.map of two OrderHoms as an OrderHom.

Equations
• f.prodMap g = { toFun := Prod.map f g, monotone' := }
Instances For
@[simp]
theorem Pi.evalOrderHom_coe {ι : Type u_6} {π : ιType u_7} [(i : ι) → Preorder (π i)] (i : ι) :
def Pi.evalOrderHom {ι : 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 an OrderHom.

Equations
• = { toFun := , monotone' := }
Instances For
@[simp]
theorem OrderHom.coeFnHom_coe {α : Type u_2} {β : Type u_3} [] [] :
OrderHom.coeFnHom = fun (f : α →o β) => f
def OrderHom.coeFnHom {α : Type u_2} {β : Type u_3} [] [] :
(α →o β) →o αβ

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

Equations
• OrderHom.coeFnHom = { toFun := fun (f : α →o β) => f, monotone' := }
Instances For
@[simp]
theorem OrderHom.apply_coe {α : Type u_2} {β : Type u_3} [] [] (x : α) :
() = fun (f : α →o β) => f
def OrderHom.apply {α : Type u_2} {β : Type u_3} [] [] (x : α) :
(α →o β) →o β

Function application fun f => f a (for fixed a) is a monotone function from the monotone function space α →o β to β. See also Pi.evalOrderHom.

Equations
• = ().comp OrderHom.coeFnHom
Instances For
@[simp]
theorem OrderHom.pi_coe {α : Type u_2} [] {ι : Type u_6} {π : ιType u_7} [(i : ι) → Preorder (π i)] (f : (i : ι) → α →o π i) (x : α) (i : ι) :
() x i = (f i) x
def OrderHom.pi {α : Type u_2} [] {ι : 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
• = { toFun := fun (x : α) (i : ι) => (f i) x, monotone' := }
Instances For
@[simp]
theorem OrderHom.piIso_symm_apply {α : Type u_2} [] {ι : Type u_6} {π : ιType u_7} [(i : ι) → Preorder (π i)] (f : (i : ι) → α →o π i) :
(RelIso.symm OrderHom.piIso) f =
@[simp]
theorem OrderHom.piIso_apply {α : Type u_2} [] {ι : Type u_6} {π : ιType u_7} [(i : ι) → Preorder (π i)] (f : α →o (i : ι) → π i) (i : ι) :
OrderHom.piIso f i = ().comp f
def OrderHom.piIso {α : Type u_2} [] {ι : 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
• OrderHom.piIso = { toFun := fun (f : α →o (i : ι) → π i) (i : ι) => ().comp f, invFun := OrderHom.pi, left_inv := , right_inv := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderHom.Subtype.val_coe {α : Type u_2} [] (p : αProp) :
= Subtype.val
def OrderHom.Subtype.val {α : Type u_2} [] (p : αProp) :
→o α

Subtype.val as a bundled monotone function.

Equations
• = { toFun := Subtype.val, monotone' := }
Instances For
@[simp]
theorem Subtype.orderEmbedding_apply_coe {α : Type u_2} [] {p : αProp} {q : αProp} (h : ∀ (a : α), p aq a) (x : { x : α // p x }) :
() = x
def Subtype.orderEmbedding {α : Type u_2} [] {p : αProp} {q : αProp} (h : ∀ (a : α), p aq a) :
{ x : α // p x } ↪o { x : α // q x }

Subtype.impEmbedding as an order embedding.

Equations
• = let __src := ; { toEmbedding := __src, map_rel_iff' := }
Instances For
instance OrderHom.unique {α : Type u_2} [] [] :
Unique (α →o α)

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

Equations
• OrderHom.unique = { default := OrderHom.id, uniq := }
theorem OrderHom.orderHom_eq_id {α : Type u_2} [] [] (g : α →o α) :
g = OrderHom.id
@[simp]
theorem OrderHom.dual_apply_coe {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :
∀ (a : αᵒᵈ), (OrderHom.dual f) a = (OrderDual.toDual f OrderDual.ofDual) a
@[simp]
theorem OrderHom.dual_symm_apply_coe {α : Type u_2} {β : Type u_3} [] [] (f : αᵒᵈ →o βᵒᵈ) :
∀ (a : α), (OrderHom.dual.symm f) a = (OrderDual.ofDual f OrderDual.toDual) a
def OrderHom.dual {α : Type u_2} {β : Type u_3} [] [] :
(α →o β) (αᵒᵈ →o βᵒᵈ)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem OrderHom.dual_id {α : Type u_2} [] :
OrderHom.dual OrderHom.id = OrderHom.id
@[simp]
theorem OrderHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (g : β →o γ) (f : α →o β) :
OrderHom.dual (g.comp f) = (OrderHom.dual g).comp (OrderHom.dual f)
@[simp]
theorem OrderHom.symm_dual_id {α : Type u_2} [] :
OrderHom.dual.symm OrderHom.id = OrderHom.id
@[simp]
theorem OrderHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (g : βᵒᵈ →o γᵒᵈ) (f : αᵒᵈ →o βᵒᵈ) :
OrderHom.dual.symm (g.comp f) = (OrderHom.dual.symm g).comp (OrderHom.dual.symm f)
def OrderHom.dualIso (α : Type u_8) (β : Type u_9) [] [] :

OrderHom.dual as an order isomorphism.

Equations
• = { toEquiv := OrderHom.dual.trans OrderDual.toDual, map_rel_iff' := }
Instances For
@[simp]
theorem OrderHom.withBotMap_coe {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :
f.withBotMap =
def OrderHom.withBotMap {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :

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

Equations
• f.withBotMap = { toFun := , monotone' := }
Instances For
@[simp]
theorem OrderHom.withTopMap_coe {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :
f.withTopMap =
def OrderHom.withTopMap {α : Type u_2} {β : Type u_3} [] [] (f : α →o β) :

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

Equations
• f.withTopMap = { toFun := , monotone' := }
Instances For
def RelEmbedding.orderEmbeddingOfLTEmbedding {α : Type u_2} {β : Type u_3} [] [] (f : (fun (x x_1 : α) => x < x_1) ↪r fun (x x_1 : β) => x < x_1) :
α ↪o β

Embeddings of partial orders that preserve < also preserve ≤.

Equations
• f.orderEmbeddingOfLTEmbedding = { toEmbedding := f.toEmbedding, map_rel_iff' := }
Instances For
@[simp]
theorem RelEmbedding.orderEmbeddingOfLTEmbedding_apply {α : Type u_2} {β : Type u_3} [] [] {f : (fun (x x_1 : α) => x < x_1) ↪r fun (x x_1 : β) => x < x_1} {x : α} :
f.orderEmbeddingOfLTEmbedding x = f x
def OrderEmbedding.ltEmbedding {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) :
(fun (x x_1 : α) => x < x_1) ↪r fun (x x_1 : β) => x < x_1

< is preserved by order embeddings of preorders.

Equations
• f.ltEmbedding = { toEmbedding := f.toEmbedding, map_rel_iff' := }
Instances For
@[simp]
theorem OrderEmbedding.ltEmbedding_apply {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) (x : α) :
f.ltEmbedding x = f x
@[simp]
theorem OrderEmbedding.le_iff_le {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) {a : α} {b : α} :
f a f b a b
@[simp]
theorem OrderEmbedding.lt_iff_lt {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) {a : α} {b : α} :
f a < f b a < b
theorem OrderEmbedding.eq_iff_eq {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) {a : α} {b : α} :
f a = f b a = b
theorem OrderEmbedding.monotone {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) :
theorem OrderEmbedding.strictMono {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) :
theorem OrderEmbedding.acc {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) (a : α) :
Acc (fun (x x_1 : β) => x < x_1) (f a)Acc (fun (x x_1 : α) => x < x_1) a
theorem OrderEmbedding.wellFounded {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) :
(WellFounded fun (x x_1 : β) => x < x_1)WellFounded fun (x x_1 : α) => x < x_1
theorem OrderEmbedding.isWellOrder {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) [IsWellOrder β fun (x x_1 : β) => x < x_1] :
IsWellOrder α fun (x x_1 : α) => x < x_1
def OrderEmbedding.dual {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) :

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

Equations
• f.dual = { toEmbedding := f.toEmbedding, map_rel_iff' := }
Instances For
theorem OrderEmbedding.wellFoundedLT {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) [] :

A preorder which embeds into a well-founded preorder is itself well-founded.

theorem OrderEmbedding.wellFoundedGT {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) [] :

A preorder which embeds into a preorder in which (· > ·) is well-founded also has (· > ·) well-founded.

@[simp]
theorem OrderEmbedding.withBotMap_apply {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) :
f.withBotMap =
def OrderEmbedding.withBotMap {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) :

A version of WithBot.map for order embeddings.

Equations
• f.withBotMap = let __src := f.optionMap; { toFun := , inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderEmbedding.withTopMap_apply {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) :
f.withTopMap =
def OrderEmbedding.withTopMap {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) :

A version of WithTop.map for order embeddings.

Equations
• f.withTopMap = let __src := f.dual.withBotMap.dual; { toFun := , inj' := , map_rel_iff' := }
Instances For
def OrderEmbedding.ofMapLEIff {α : Type u_6} {β : Type u_7} [] [] (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
Instances For
@[simp]
theorem OrderEmbedding.coe_ofMapLEIff {α : Type u_6} {β : Type u_7} [] [] {f : αβ} (h : ∀ (a b : α), f a f b a b) :
= f
def OrderEmbedding.ofStrictMono {α : Type u_6} {β : Type u_7} [] [] (f : αβ) (h : ) :
α ↪o β

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

Equations
Instances For
@[simp]
theorem OrderEmbedding.coe_ofStrictMono {α : Type u_6} {β : Type u_7} [] [] {f : αβ} (h : ) :
= f
@[simp]
theorem OrderEmbedding.subtype_apply {α : Type u_2} [] (p : αProp) :
= Subtype.val
def OrderEmbedding.subtype {α : Type u_2} [] (p : αProp) :
↪o α

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

Equations
• = { toEmbedding := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderEmbedding.toOrderHom_coe {X : Type u_6} {Y : Type u_7} [] [] (f : X ↪o Y) :
f.toOrderHom = f
def OrderEmbedding.toOrderHom {X : Type u_6} {Y : Type u_7} [] [] (f : X ↪o Y) :
X →o Y

Convert an OrderEmbedding to an OrderHom.

Equations
• f.toOrderHom = { toFun := f, monotone' := }
Instances For
@[simp]
theorem OrderEmbedding.ofIsEmpty_apply {α : Type u_2} {β : Type u_3} [] [] [] (a : α) :
OrderEmbedding.ofIsEmpty a =
def OrderEmbedding.ofIsEmpty {α : Type u_2} {β : Type u_3} [] [] [] :
α ↪o β

The trivial embedding from an empty preorder to another preorder

Equations
• OrderEmbedding.ofIsEmpty = { toFun := fun (a : α) => , inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderEmbedding.coe_ofIsEmpty {α : Type u_2} {β : Type u_3} [] [] [] :
OrderEmbedding.ofIsEmpty = fun (a : α) =>
theorem Disjoint.of_orderEmbedding {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) [] [] {a₁ : α} {a₂ : α} :
Disjoint (f a₁) (f a₂)Disjoint a₁ a₂

If the images by an order embedding of two elements are disjoint, then they are themselves disjoint.

theorem Codisjoint.of_orderEmbedding {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) [] [] {a₁ : α} {a₂ : α} :
Codisjoint (f a₁) (f a₂)Codisjoint a₁ a₂

If the images by an order embedding of two elements are codisjoint, then they are themselves codisjoint.

theorem IsCompl.of_orderEmbedding {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) [] [] {a₁ : α} {a₂ : α} :
IsCompl (f a₁) (f a₂)IsCompl a₁ a₂

If the images by an order embedding of two elements are complements, then they are themselves complements.

@[simp]
theorem RelHom.toOrderHom_coe {α : Type u_2} {β : Type u_3} [] [] (f : (fun (x x_1 : α) => x < x_1) →r fun (x x_1 : β) => x < x_1) :
f.toOrderHom = f
def RelHom.toOrderHom {α : Type u_2} {β : Type u_3} [] [] (f : (fun (x x_1 : α) => x < x_1) →r fun (x x_1 : β) => x < x_1) :
α →o β

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

Equations
• f.toOrderHom = { toFun := f, monotone' := }
Instances For
theorem RelEmbedding.toOrderHom_injective {α : Type u_2} {β : Type u_3} [] [] (f : (fun (x x_1 : α) => x < x_1) ↪r fun (x x_1 : β) => x < x_1) :
Function.Injective f.toRelHom.toOrderHom
instance OrderIso.instEquivLike {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
EquivLike (α ≃o β) α β
Equations
• OrderIso.instEquivLike = { coe := fun (f : α ≃o β) => f.toFun, inv := fun (f : α ≃o β) => f.invFun, left_inv := , right_inv := , coe_injective' := }
instance OrderIso.instOrderIsoClass {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
OrderIsoClass (α ≃o β) α β
Equations
• =
@[simp]
theorem OrderIso.toFun_eq_coe {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f : α ≃o β} :
f.toFun = f
theorem OrderIso.ext {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f : α ≃o β} {g : α ≃o β} (h : f = g) :
f = g
def OrderIso.toOrderEmbedding {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
α ↪o β

Reinterpret an order isomorphism as an order embedding.

Equations
• e.toOrderEmbedding =
Instances For
@[simp]
theorem OrderIso.coe_toOrderEmbedding {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
e.toOrderEmbedding = e
theorem OrderIso.bijective {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
theorem OrderIso.injective {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
theorem OrderIso.surjective {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
theorem OrderIso.apply_eq_iff_eq {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : α} :
e x = e y x = y
def OrderIso.refl (α : Type u_6) [LE α] :
α ≃o α

Identity order isomorphism.

Equations
Instances For
@[simp]
theorem OrderIso.coe_refl {α : Type u_2} [LE α] :
() = id
@[simp]
theorem OrderIso.refl_apply {α : Type u_2} [LE α] (x : α) :
() x = x
@[simp]
theorem OrderIso.refl_toEquiv {α : Type u_2} [LE α] :
().toEquiv =
def OrderIso.symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
β ≃o α

Inverse of an order isomorphism.

Equations
• e.symm =
Instances For
@[simp]
theorem OrderIso.apply_symm_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) (x : β) :
e (e.symm x) = x
@[simp]
theorem OrderIso.symm_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) (x : α) :
e.symm (e x) = x
@[simp]
theorem OrderIso.symm_refl (α : Type u_6) [LE α] :
().symm =
theorem OrderIso.apply_eq_iff_eq_symm_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) (x : α) (y : β) :
e x = y x = e.symm y
theorem OrderIso.symm_apply_eq {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
e.symm y = x y = e x
@[simp]
theorem OrderIso.symm_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
e.symm.symm = e
theorem OrderIso.symm_bijective {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
Function.Bijective OrderIso.symm
theorem OrderIso.symm_injective {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
Function.Injective OrderIso.symm
@[simp]
theorem OrderIso.toEquiv_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
e.symm = e.symm.toEquiv
def OrderIso.trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e : α ≃o β) (e' : β ≃o γ) :
α ≃o γ

Composition of two order isomorphisms is an order isomorphism.

Equations
Instances For
@[simp]
theorem OrderIso.coe_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e : α ≃o β) (e' : β ≃o γ) :
(e.trans e') = e' e
@[simp]
theorem OrderIso.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e : α ≃o β) (e' : β ≃o γ) (x : α) :
(e.trans e') x = e' (e x)
@[simp]
theorem OrderIso.refl_trans {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
().trans e = e
@[simp]
theorem OrderIso.trans_refl {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
e.trans () = e
@[simp]
theorem OrderIso.symm_trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : γ) :
(e₁.trans e₂).symm c = e₁.symm (e₂.symm c)
theorem OrderIso.symm_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
@[simp]
theorem OrderIso.self_trans_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
e.trans e.symm =
@[simp]
theorem OrderIso.symm_trans_self {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) :
e.symm.trans e =
@[simp]
theorem OrderIso.arrowCongr_apply {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [] [] [] [] (f : α ≃o γ) (g : β ≃o δ) (p : α →o β) :
(f.arrowCongr g) p = (g).comp (p.comp f.symm)
@[simp]
theorem OrderIso.arrowCongr_symm_apply {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [] [] [] [] (f : α ≃o γ) (g : β ≃o δ) (p : γ →o δ) :
(RelIso.symm (f.arrowCongr g)) p = (g.symm).comp (p.comp f)
def OrderIso.arrowCongr {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [] [] [] [] (f : α ≃o γ) (g : β ≃o δ) :
(α →o β) ≃o (γ →o δ)

An order isomorphism between the domains and codomains of two prosets of order homomorphisms gives an order isomorphism between the two function prosets.

Equations
• f.arrowCongr g = { toFun := fun (p : α →o β) => (g).comp (p.comp f.symm), invFun := fun (p : γ →o δ) => (g.symm).comp (p.comp f), left_inv := , right_inv := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.conj_apply {α : Type u_6} {β : Type u_7} [] [] (f : α ≃o β) (a : α →o α) :
f.conj a = (f).comp (a.comp f.symm)
@[simp]
theorem OrderIso.conj_symm_apply {α : Type u_6} {β : Type u_7} [] [] (f : α ≃o β) :
∀ (a : β →o β), f.conj.symm a = EquivLike.inv (f.arrowCongr f) a
def OrderIso.conj {α : Type u_6} {β : Type u_7} [] [] (f : α ≃o β) :
(α →o α) (β →o β)

If α and β are order-isomorphic then the two orders of order-homomorphisms from α and β to themselves are order-isomorphic.

Equations
• f.conj = (f.arrowCongr f)
Instances For
def OrderIso.prodComm {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
α × β ≃o β × α

Prod.swap as an OrderIso.

Equations
• OrderIso.prodComm = { toEquiv := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.coe_prodComm {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
OrderIso.prodComm = Prod.swap
@[simp]
theorem OrderIso.prodComm_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
OrderIso.prodComm.symm = OrderIso.prodComm
def OrderIso.dualDual (α : Type u_2) [LE α] :

The order isomorphism between a type and its double dual.

Equations
Instances For
@[simp]
theorem OrderIso.coe_dualDual (α : Type u_2) [LE α] :
= OrderDual.toDual OrderDual.toDual
@[simp]
theorem OrderIso.coe_dualDual_symm (α : Type u_2) [LE α] :
.symm = OrderDual.ofDual OrderDual.ofDual
@[simp]
theorem OrderIso.dualDual_apply {α : Type u_2} [LE α] (a : α) :
a = OrderDual.toDual (OrderDual.toDual a)
@[simp]
theorem OrderIso.dualDual_symm_apply {α : Type u_2} [LE α] (a : αᵒᵈᵒᵈ) :
.symm a = OrderDual.ofDual (OrderDual.ofDual a)
theorem OrderIso.le_iff_le {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : α} :
e x e y x y
theorem OrderIso.le_symm_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
x e.symm y e x y
theorem OrderIso.symm_apply_le {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} :
e.symm y x y e x
theorem OrderIso.monotone {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) :
theorem OrderIso.strictMono {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) :
@[simp]
theorem OrderIso.lt_iff_lt {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) {x : α} {y : α} :
e x < e y x < y
def OrderIso.toRelIsoLT {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) :
(fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1

Converts an OrderIso into a RelIso (<) (<).

Equations
• e.toRelIsoLT = { toEquiv := e.toEquiv, map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.toRelIsoLT_apply {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) (x : α) :
e.toRelIsoLT x = e x
@[simp]
theorem OrderIso.toRelIsoLT_symm {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) :
e.toRelIsoLT.symm = e.symm.toRelIsoLT
def OrderIso.ofRelIsoLT {α : Type u_6} {β : Type u_7} [] [] (e : (fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1) :
α ≃o β

Converts a RelIso (<) (<) into an OrderIso.

Equations
• = { toEquiv := e.toEquiv, map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.ofRelIsoLT_apply {α : Type u_6} {β : Type u_7} [] [] (e : (fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1) (x : α) :
x = e x
@[simp]
theorem OrderIso.ofRelIsoLT_symm {α : Type u_6} {β : Type u_7} [] [] (e : (fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1) :
.symm = OrderIso.ofRelIsoLT e.symm
@[simp]
theorem OrderIso.ofRelIsoLT_toRelIsoLT {α : Type u_6} {β : Type u_7} [] [] (e : α ≃o β) :
OrderIso.ofRelIsoLT e.toRelIsoLT = e
@[simp]
theorem OrderIso.toRelIsoLT_ofRelIsoLT {α : Type u_6} {β : Type u_7} [] [] (e : (fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1) :
.toRelIsoLT = e
def OrderIso.ofCmpEqCmp {α : Type u_6} {β : Type u_7} [] [] (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
• = let_fun gf := ; { toFun := f, invFun := g, left_inv := , right_inv := , map_rel_iff' := }
Instances For
def OrderIso.ofHomInv {α : Type u_2} {β : Type u_3} [] [] {F : Type u_6} {G : Type u_7} [FunLike F α β] [] [FunLike G β α] [] (f : F) (g : G) (h₁ : (f).comp g = OrderHom.id) (h₂ : (g).comp f = OrderHom.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
• OrderIso.ofHomInv f g h₁ h₂ = { toFun := f, invFun := g, left_inv := , right_inv := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.funUnique_apply (α : Type u_6) (β : Type u_7) [] [] (f : (i : α) → (fun (a : α) => β) i) :
() f = f default
@[simp]
theorem OrderIso.funUnique_toEquiv (α : Type u_6) (β : Type u_7) [] [] :
().toEquiv =
def OrderIso.funUnique (α : Type u_6) (β : Type u_7) [] [] :
(αβ) ≃o β

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

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.funUnique_symm_apply {α : Type u_6} {β : Type u_7} [] [] :
().symm =
def Equiv.toOrderIso {α : Type u_2} {β : Type u_3} [] [] (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
• e.toOrderIso h₁ h₂ = { toEquiv := e, map_rel_iff' := }
Instances For
@[simp]
theorem Equiv.coe_toOrderIso {α : Type u_2} {β : Type u_3} [] [] (e : α β) (h₁ : Monotone e) (h₂ : Monotone e.symm) :
(e.toOrderIso h₁ h₂) = e
@[simp]
theorem Equiv.toOrderIso_toEquiv {α : Type u_2} {β : Type u_3} [] [] (e : α β) (h₁ : Monotone e) (h₂ : Monotone e.symm) :
(e.toOrderIso h₁ h₂).toEquiv = e
@[simp]
theorem StrictMono.orderIsoOfRightInverse_apply {α : Type u_2} {β : Type u_3} [] [] (f : αβ) (h_mono : ) (g : βα) (hg : ) :
@[simp]
theorem StrictMono.orderIsoOfRightInverse_symm_apply {α : Type u_2} {β : Type u_3} [] [] (f : αβ) (h_mono : ) (g : βα) (hg : ) :
def StrictMono.orderIsoOfRightInverse {α : Type u_2} {β : Type u_3} [] [] (f : αβ) (h_mono : ) (g : βα) (hg : ) :
α ≃o β

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

Equations
Instances For
def OrderIso.dual {α : Type u_2} {β : Type u_3} [LE α] [LE β] (f : α ≃o β) :

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

Equations
• f.dual = { toEquiv := f.toEquiv, map_rel_iff' := }
Instances For
theorem OrderIso.map_bot' {α : Type u_2} {β : Type u_3} [LE α] [] (f : α ≃o β) {x : α} {y : β} (hx : ∀ (x' : α), x x') (hy : ∀ (y' : β), y y') :
f x = y
theorem OrderIso.map_bot {α : Type u_2} {β : Type u_3} [LE α] [] [] [] (f : α ≃o β) :
theorem OrderIso.map_top' {α : Type u_2} {β : Type u_3} [LE α] [] (f : α ≃o β) {x : α} {y : β} (hx : ∀ (x' : α), x' x) (hy : ∀ (y' : β), y' y) :
f x = y
theorem OrderIso.map_top {α : Type u_2} {β : Type u_3} [LE α] [] [] [] (f : α ≃o β) :
theorem OrderEmbedding.map_inf_le {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) (x : α) (y : α) :
f (x y) f x f y
theorem OrderEmbedding.le_map_sup {α : Type u_2} {β : Type u_3} [] [] (f : α ↪o β) (x : α) (y : α) :
f x f y f (x y)
theorem OrderIso.map_inf {α : Type u_2} {β : Type u_3} [] [] (f : α ≃o β) (x : α) (y : α) :
f (x y) = f x f y
theorem OrderIso.map_sup {α : Type u_2} {β : Type u_3} [] [] (f : α ≃o β) (x : α) (y : α) :
f (x y) = f x f y
theorem Disjoint.map_orderIso {α : Type u_2} {β : Type u_3} [] [] [] [] {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

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

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

@[simp]
theorem disjoint_map_orderIso_iff {α : Type u_2} {β : Type u_3} [] [] [] [] {a : α} {b : α} (f : α ≃o β) :
Disjoint (f a) (f b) Disjoint a b
@[simp]
theorem codisjoint_map_orderIso_iff {α : Type u_2} {β : Type u_3} [] [] [] [] {a : α} {b : α} (f : α ≃o β) :
Codisjoint (f a) (f b)
def WithBot.toDualTopEquiv {α : Type u_2} [LE α] :

Taking the dual then adding ⊥ is the same as adding ⊤ then taking the dual. This is the order iso form of WithBot.ofDual, as proven by coe_toDualTopEquiv_eq.

Equations
• WithBot.toDualTopEquiv =
Instances For
@[simp]
theorem WithBot.toDualTopEquiv_coe {α : Type u_2} [LE α] (a : α) :
WithBot.toDualTopEquiv (OrderDual.toDual a) = OrderDual.toDual a
@[simp]
theorem WithBot.toDualTopEquiv_symm_coe {α : Type u_2} [LE α] (a : α) :
WithBot.toDualTopEquiv.symm (OrderDual.toDual a) = (OrderDual.toDual a)
@[simp]
theorem WithBot.toDualTopEquiv_bot {α : Type u_2} [LE α] :
WithBot.toDualTopEquiv =
@[simp]
theorem WithBot.toDualTopEquiv_symm_bot {α : Type u_2} [LE α] :
WithBot.toDualTopEquiv.symm =
theorem WithBot.coe_toDualTopEquiv_eq {α : Type u_2} [LE α] :
WithBot.toDualTopEquiv = OrderDual.toDual WithBot.ofDual
def WithTop.toDualBotEquiv {α : Type u_2} [LE α] :

Taking the dual then adding ⊤ is the same as adding ⊥ then taking the dual. This is the order iso form of WithTop.ofDual, as proven by coe_toDualBotEquiv_eq.

Equations
• WithTop.toDualBotEquiv =
Instances For
@[simp]
theorem WithTop.toDualBotEquiv_coe {α : Type u_2} [LE α] (a : α) :
WithTop.toDualBotEquiv (OrderDual.toDual a) = OrderDual.toDual a
@[simp]
theorem WithTop.toDualBotEquiv_symm_coe {α : Type u_2} [LE α] (a : α) :
WithTop.toDualBotEquiv.symm (OrderDual.toDual a) = (OrderDual.toDual a)
@[simp]
theorem WithTop.toDualBotEquiv_top {α : Type u_2} [LE α] :
WithTop.toDualBotEquiv =
@[simp]
theorem WithTop.toDualBotEquiv_symm_top {α : Type u_2} [LE α] :
WithTop.toDualBotEquiv.symm =
theorem WithTop.coe_toDualBotEquiv {α : Type u_2} [LE α] :
WithTop.toDualBotEquiv = OrderDual.toDual WithTop.ofDual
@[simp]
theorem OrderIso.withTopCongr_apply {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) :
∀ (a : ), e.withTopCongr a = Option.map (e) a
def OrderIso.withTopCongr {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) :

A version of Equiv.optionCongr for WithTop.

Equations
• e.withTopCongr = let __src := e.toOrderEmbedding.withTopMap; { toEquiv := e.optionCongr, map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.withTopCongr_refl {α : Type u_2} [] :
().withTopCongr =
@[simp]
theorem OrderIso.withTopCongr_symm {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) :
e.withTopCongr.symm = e.symm.withTopCongr
@[simp]
theorem OrderIso.withTopCongr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
e₁.withTopCongr.trans e₂.withTopCongr = (e₁.trans e₂).withTopCongr
@[simp]
theorem OrderIso.withBotCongr_apply {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) :
∀ (a : ), e.withBotCongr a = Option.map (e) a
def OrderIso.withBotCongr {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) :

A version of Equiv.optionCongr for WithBot.

Equations
• e.withBotCongr = let __src := e.toOrderEmbedding.withBotMap; { toEquiv := e.optionCongr, map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.withBotCongr_refl {α : Type u_2} [] :
().withBotCongr =
@[simp]
theorem OrderIso.withBotCongr_symm {α : Type u_2} {β : Type u_3} [] [] (e : α ≃o β) :
e.withBotCongr.symm = e.symm.withBotCongr
@[simp]
theorem OrderIso.withBotCongr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
e₁.withBotCongr.trans e₂.withBotCongr = (e₁.trans e₂).withBotCongr
theorem OrderIso.isCompl {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α ≃o β) {x : α} {y : α} (h : IsCompl x y) :
IsCompl (f x) (f y)
theorem OrderIso.isCompl_iff {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α ≃o β) {x : α} {y : α} :
IsCompl x y IsCompl (f x) (f y)
theorem OrderIso.complementedLattice {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α ≃o β) :
theorem OrderIso.complementedLattice_iff {α : Type u_2} {β : Type u_3} [] [] [] [] (f : α ≃o β) :