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

source
structure order_hom (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :
Type (max u_1 u_2)

Bundled monotone (aka, increasing) function

source
def order_hom_class (F : Type u_1) (α : out_param (Type u_2)) (β : out_param (Type u_3)) [preorder α] [preorder β] :
Type (max u_1 u_2 u_3)

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

source
def order_embedding (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :
Type (max u_1 u_2)

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

source
def order_iso (α : Type u_1) (β : Type u_2) [has_le α] [has_le β] :
Type (max u_1 u_2)

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

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

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

Equations
source
@[simp]
theorem order_hom.id_coe {α : Type u_1} [preorder α] :
⇑order_hom.id = id
source
def order_hom.id {α : Type u_1} [preorder α] :
α →o α

The identity function as bundled monotone function.

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

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

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

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

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

The composition of two bundled monotone functions.

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

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

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

Constant function bundled as a order_hom.

Equations
source
@[simp]
theorem order_hom.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →o β) (c : γ) :
(⇑(order_hom.const β) c).comp f = ⇑(order_hom.const α) c
source
@[simp]
theorem order_hom.comp_const {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (γ : Type u_3) [preorder γ] (f : α →o β) (c : α) :
f.comp (⇑(order_hom.const γ) c) = ⇑(order_hom.const γ) (⇑f c)
source
@[protected]
def order_hom.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [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
source
@[simp]
theorem order_hom.prod_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →o β) (g : α →o γ) (x : α) :
⇑(f.prod g) x = (⇑f x, ⇑g x)
source
theorem order_hom.prod_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] {f₁ f₂ : α →o β} (hf : f₁ ≤ f₂) {g₁ g₂ : α →o γ} (hg : g₁ ≤ g₂) :
f₁.prod g₁ ≤ f₂.prod g₂
source
theorem order_hom.comp_prod_comp_same {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f₁ f₂ : β →o γ) (g : α →o β) :
(f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g
source
@[simp]
theorem order_hom.prodₘ_coe_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (x : α →o β) (ᾰ : α →o γ) (x_1 : α) :
⇑(⇑(⇑order_hom.prodₘ x) ᾰ) x_1 = (⇑x x_1, ⇑ᾰ x_1)
source
def order_hom.prodₘ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [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
source
@[simp]
theorem order_hom.diag_coe {α : Type u_1} [preorder α] (x : α) :
⇑order_hom.diag x = (x, x)
source
def order_hom.diag {α : Type u_1} [preorder α] :
α →o α × α

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

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

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

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

prod.fst as a order_hom.

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

prod.snd as a order_hom.

Equations
source
@[simp]
theorem order_hom.snd_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (self : α × β) :
⇑order_hom.snd self = self.snd
source
@[simp]
theorem order_hom.fst_prod_snd {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
order_hom.fst.prod order_hom.snd = order_hom.id
source
@[simp]
theorem order_hom.fst_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →o β) (g : α →o γ) :
order_hom.fst.comp (f.prod g) = f
source
@[simp]
theorem order_hom.snd_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →o β) (g : α →o γ) :
order_hom.snd.comp (f.prod g) = g
source
def order_hom.prod_iso {α : Type u_1} {β : Type u_2} {γ : Type u_3} [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
source
@[simp]
theorem order_hom.prod_iso_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →o β × γ) :
⇑order_hom.prod_iso f = (order_hom.fst.comp f, order_hom.snd.comp f)
source
@[simp]
theorem order_hom.prod_iso_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : (α →o β) × (α →o γ)) :
⇑(rel_iso.symm order_hom.prod_iso) f = f.fst.prod f.snd
source
def order_hom.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [preorder α] [preorder β] [preorder γ] [preorder δ] (f : α →o β) (g : γ →o δ) :
α × γ →o β × δ

prod.map of two order_homs as a order_hom.

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

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

Equations
source
@[simp]
theorem pi.eval_order_hom_coe {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), preorder (π i)] (i : ι) :
⇑(pi.eval_order_hom i) = function.eval i
source
@[simp]
theorem order_hom.coe_fn_hom_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
⇑order_hom.coe_fn_hom = λ (f : α →o β), ⇑f
source
def order_hom.coe_fn_hom {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
(α →o β) →o α → β

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

Equations
source
def order_hom.apply {α : Type u_1} {β : Type u_2} [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
source
@[simp]
theorem order_hom.apply_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (x : α) :
⇑(order_hom.apply x) = function.eval x ∘ coe_fn
source
def order_hom.pi {α : Type u_1} [preorder α] {ι : Type u_5} {π : ι → Type u_6} [Π (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
source
@[simp]
theorem order_hom.pi_coe {α : Type u_1} [preorder α] {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), preorder (π i)] (f : Π (i : ι), α →o π i) (x : α) (i : ι) :
⇑(order_hom.pi f) x i = ⇑(f i) x
source
@[simp]
theorem order_hom.pi_iso_symm_apply {α : Type u_1} [preorder α] {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), preorder (π i)] (f : Π (i : ι), α →o (λ (i : ι), π i) i) :
⇑(rel_iso.symm order_hom.pi_iso) f = order_hom.pi f
source
@[simp]
theorem order_hom.pi_iso_apply {α : Type u_1} [preorder α] {ι : Type u_5} {π : ι → Type u_6} [Π (i : ι), preorder (π i)] (f : α →o Π (i : ι), π i) (i : ι) :
⇑order_hom.pi_iso f i = (pi.eval_order_hom i).comp f
source
def order_hom.pi_iso {α : Type u_1} [preorder α] {ι : Type u_5} {π : ι → Type u_6} [Π (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
source
@[simp]
theorem order_hom.subtype.val_coe {α : Type u_1} [preorder α] (p : α → Prop) :
⇑(order_hom.subtype.val p) = subtype.val
source
def order_hom.subtype.val {α : Type u_1} [preorder α] (p : α → Prop) :
subtype p →o α

subtype.val as a bundled monotone function.

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

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

Equations
source
theorem order_hom.order_hom_eq_id {α : Type u_1} [preorder α] [subsingleton α] (g : α →o α) :
g = order_hom.id
source
@[protected]
def order_hom.dual {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
(α →o β) ≃ (order_dual α →o order_dual β)

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

Equations
source
@[simp]
theorem order_hom.dual_apply_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (ᾰ : order_dual α) :
⇑(⇑order_hom.dual f) ᾰ = (⇑order_dual.to_dual ∘ ⇑f ∘ ⇑order_dual.of_dual) ᾰ
source
@[simp]
theorem order_hom.dual_symm_apply_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : order_dual α →o order_dual β) (ᾰ : α) :
⇑(⇑(order_hom.dual.symm) f) ᾰ = (⇑order_dual.of_dual ∘ ⇑f ∘ ⇑order_dual.to_dual) ᾰ
source
def order_hom.dual_iso (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :
(α →o β) ≃o order_dual (order_dual α →o order_dual β)

order_hom.dual as an order isomorphism.

Equations
source
def rel_embedding.order_embedding_of_lt_embedding {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (f : has_lt.lt ↪r has_lt.lt) :
α ↪o β

Embeddings of partial orders that preserve < also preserve ≤.

Equations
source
@[simp]
theorem rel_embedding.order_embedding_of_lt_embedding_apply {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] {f : has_lt.lt ↪r has_lt.lt} {x : α} :
⇑(f.order_embedding_of_lt_embedding) x = ⇑f x
source
def order_embedding.lt_embedding {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) :
has_lt.lt ↪r has_lt.lt

< is preserved by order embeddings of preorders.

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

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

Equations
source
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
source
@[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) :
⇑(order_embedding.of_map_le_iff f h) = f
source
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
source
@[simp]
theorem order_embedding.coe_of_strict_mono {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {f : α → β} (h : strict_mono f) :
⇑(order_embedding.of_strict_mono f h) = f
source
@[simp]
theorem order_embedding.subtype_apply {α : Type u_1} [preorder α] (p : α → Prop) :
⇑(order_embedding.subtype p) = coe
source
def order_embedding.subtype {α : Type u_1} [preorder α] (p : α → Prop) :
subtype p ↪o α

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

Equations
source
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
source
@[simp]
theorem order_embedding.to_order_hom_coe {X : Type u_1} {Y : Type u_2} [preorder X] [preorder Y] (f : X ↪o Y) :
⇑(f.to_order_hom) = ⇑f
source
def rel_hom.to_order_hom {α : Type u_1} {β : Type u_2} [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
source
@[simp]
theorem rel_hom.to_order_hom_coe {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] (f : has_lt.lt →r has_lt.lt) :
⇑(f.to_order_hom) = ⇑f
source
theorem rel_embedding.to_order_hom_injective {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] (f : has_lt.lt ↪r has_lt.lt) :
function.injective ⇑(↑f.to_order_hom)
source
def order_iso.to_order_embedding {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
α ↪o β

Reinterpret an order isomorphism as an order embedding.

Equations
source
@[simp]
theorem order_iso.coe_to_order_embedding {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
⇑(e.to_order_embedding) = ⇑e
source
@[protected]
theorem order_iso.bijective {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
function.bijective ⇑e
source
@[protected]
theorem order_iso.injective {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
function.injective ⇑e
source
@[protected]
theorem order_iso.surjective {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
function.surjective ⇑e
source
@[simp]
theorem order_iso.range_eq {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
set.range ⇑e = set.univ
source
@[simp]
theorem order_iso.apply_eq_iff_eq {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) {x y : α} :
⇑e x = ⇑e y ↔ x = y
source
def order_iso.refl (α : Type u_1) [has_le α] :
α ≃o α

Identity order isomorphism.

Equations
source
@[simp]
theorem order_iso.coe_refl {α : Type u_1} [has_le α] :
⇑(order_iso.refl α) = id
source
theorem order_iso.refl_apply {α : Type u_1} [has_le α] (x : α) :
⇑(order_iso.refl α) x = x
source
@[simp]
theorem order_iso.refl_to_equiv {α : Type u_1} [has_le α] :
(order_iso.refl α).to_equiv = equiv.refl α
source
def order_iso.symm {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
β ≃o α

Inverse of an order isomorphism.

Equations
source
@[simp]
theorem order_iso.apply_symm_apply {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (x : β) :
⇑e (⇑(e.symm) x) = x
source
@[simp]
theorem order_iso.symm_apply_apply {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (x : α) :
⇑(e.symm) (⇑e x) = x
source
@[simp]
theorem order_iso.symm_refl (α : Type u_1) [has_le α] :
(order_iso.refl α).symm = order_iso.refl α
source
theorem order_iso.apply_eq_iff_eq_symm_apply {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (x : α) (y : β) :
⇑e x = y ↔ x = ⇑(e.symm) y
source
theorem order_iso.symm_apply_eq {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) {x : α} {y : β} :
⇑(e.symm) y = x ↔ y = ⇑e x
source
@[simp]
theorem order_iso.symm_symm {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
e.symm.symm = e
source
theorem order_iso.symm_injective {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] :
function.injective order_iso.symm
source
@[simp]
theorem order_iso.to_equiv_symm {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
e.to_equiv.symm = e.symm.to_equiv
source
@[simp]
theorem order_iso.symm_image_image {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
⇑(e.symm) '' (⇑e '' s) = s
source
@[simp]
theorem order_iso.image_symm_image {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (s : set β) :
⇑e '' (⇑(e.symm) '' s) = s
source
theorem order_iso.image_eq_preimage {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
⇑e '' s = ⇑(e.symm) ⁻¹' s
source
@[simp]
theorem order_iso.preimage_symm_preimage {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
⇑e ⁻¹' (⇑(e.symm) ⁻¹' s) = s
source
@[simp]
theorem order_iso.symm_preimage_preimage {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (s : set β) :
⇑(e.symm) ⁻¹' (⇑e ⁻¹' s) = s
source
@[simp]
theorem order_iso.image_preimage {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (s : set β) :
⇑e '' (⇑e ⁻¹' s) = s
source
@[simp]
theorem order_iso.preimage_image {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) (s : set α) :
⇑e ⁻¹' (⇑e '' s) = s
source
def order_iso.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (e : α ≃o β) (e' : β ≃o γ) :
α ≃o γ

Composition of two order isomorphisms is an order isomorphism.

Equations
source
@[simp]
theorem order_iso.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (e : α ≃o β) (e' : β ≃o γ) :
⇑(e.trans e') = ⇑e' ∘ ⇑e
source
theorem order_iso.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_le α] [has_le β] [has_le γ] (e : α ≃o β) (e' : β ≃o γ) (x : α) :
⇑(e.trans e') x = ⇑e' (⇑e x)
source
@[simp]
theorem order_iso.refl_trans {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
(order_iso.refl α).trans e = e
source
@[simp]
theorem order_iso.trans_refl {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) :
e.trans (order_iso.refl β) = e
source
@[simp]
theorem order_iso.le_iff_le {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) {x y : α} :
⇑e x ≤ ⇑e y ↔ x ≤ y
source
theorem order_iso.le_symm_apply {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) {x : α} {y : β} :
x ≤ ⇑(e.symm) y ↔ ⇑e x ≤ y
source
theorem order_iso.symm_apply_le {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (e : α ≃o β) {x : α} {y : β} :
⇑(e.symm) y ≤ x ↔ y ≤ ⇑e x
source
@[protected]
theorem order_iso.monotone {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) :
monotone ⇑e
source
@[protected]
theorem order_iso.strict_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) :
strict_mono ⇑e
source
@[simp]
theorem order_iso.lt_iff_lt {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) {x y : α} :
⇑e x < ⇑e y ↔ x < y
source
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
source
def order_iso.set_congr {α : Type u_1} [preorder α] (s t : set α) (h : s = t) :
↥s ≃o ↥t

Order isomorphism between two equal sets.

Equations
source
def order_iso.set.univ {α : Type u_1} [preorder α] :
↥set.univ ≃o α

Order isomorphism between univ : set α and α.

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

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

Equations
source
@[simp]
theorem order_iso.fun_unique_apply (α : Type u_1) (β : Type u_2) [unique α] [preorder β] (f : Π (x : α), (λ (ᾰ : α), β) x) :
⇑(order_iso.fun_unique α β) f = f (default α)
source
@[simp]
theorem order_iso.fun_unique_to_equiv (α : Type u_1) (β : Type u_2) [unique α] [preorder β] :
(order_iso.fun_unique α β).to_equiv = equiv.fun_unique α β
source
@[simp]
theorem order_iso.fun_unique_symm_apply {α : Type u_1} {β : Type u_2} [unique α] [preorder β] :
⇑((order_iso.fun_unique α β).symm) = function.const α
source
def equiv.to_order_iso {α : Type u_1} {β : Type u_2} [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
source
@[simp]
theorem equiv.coe_to_order_iso {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃ β) (h₁ : monotone ⇑e) (h₂ : monotone ⇑(e.symm)) :
⇑(e.to_order_iso h₁ h₂) = ⇑e
source
@[simp]
theorem equiv.to_order_iso_to_equiv {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃ β) (h₁ : monotone ⇑e) (h₂ : monotone ⇑(e.symm)) :
(e.to_order_iso h₁ h₂).to_equiv = e
source
@[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
source
@[protected]
noncomputable def strict_mono.order_iso {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] (f : α → β) (h_mono : strict_mono f) :
α ≃o ↥(set.range f)

A strictly monotone function from a linear order is an order isomorphism between its domain and its range.

Equations
source
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
source
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
source
@[protected]
def order_iso.dual {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] (f : α ≃o β) :
order_dual α ≃o order_dual β

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

Equations
source
theorem order_iso.map_bot' {α : Type u_1} {β : Type u_2} [has_le α] [partial_order β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ (x' : α), x ≤ x') (hy : ∀ (y' : β), y ≤ y') :
⇑f x = y
source
theorem order_iso.map_bot {α : Type u_1} {β : Type u_2} [has_le α] [partial_order β] [order_bot α] [order_bot β] (f : α ≃o β) :
⇑f ⊥ = ⊥
source
theorem order_iso.map_top' {α : Type u_1} {β : Type u_2} [has_le α] [partial_order β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ (x' : α), x' ≤ x) (hy : ∀ (y' : β), y' ≤ y) :
⇑f x = y
source
theorem order_iso.map_top {α : Type u_1} {β : Type u_2} [has_le α] [partial_order β] [order_top α] [order_top β] (f : α ≃o β) :
⇑f ⊤ = ⊤
source
theorem order_embedding.map_inf_le {α : Type u_1} {β : Type u_2} [semilattice_inf α] [semilattice_inf β] (f : α ↪o β) (x y : α) :
⇑f (x ⊓ y) ≤ ⇑f x ⊓ ⇑f y
source
theorem order_iso.map_inf {α : Type u_1} {β : Type u_2} [semilattice_inf α] [semilattice_inf β] (f : α ≃o β) (x y : α) :
⇑f (x ⊓ y) = ⇑f x ⊓ ⇑f y
source
theorem disjoint.map_order_iso {α : Type u_1} {β : Type u_2} [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

source
@[simp]
theorem disjoint_map_order_iso_iff {α : Type u_1} {β : Type u_2} [semilattice_inf α] [order_bot α] [semilattice_inf β] [order_bot β] {a b : α} (f : α ≃o β) :
disjoint (⇑f a) (⇑f b) ↔ disjoint a b
source
theorem order_embedding.le_map_sup {α : Type u_1} {β : Type u_2} [semilattice_sup α] [semilattice_sup β] (f : α ↪o β) (x y : α) :
⇑f x ⊔ ⇑f y ≤ ⇑f (x ⊔ y)
source
theorem order_iso.map_sup {α : Type u_1} {β : Type u_2} [semilattice_sup α] [semilattice_sup β] (f : α ≃o β) (x y : α) :
⇑f (x ⊔ y) = ⇑f x ⊔ ⇑f y
source
theorem order_iso.is_compl {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) {x y : α} (h : is_compl x y) :
is_compl (⇑f x) (⇑f y)
source
theorem order_iso.is_compl_iff {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) {x y : α} :
is_compl x y ↔ is_compl (⇑f x) (⇑f y)
source
theorem order_iso.is_complemented {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) [is_complemented α] :
is_complemented β
source
theorem order_iso.is_complemented_iff {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) :
is_complemented α ↔ is_complemented β