mathlib3 documentation

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:

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_6) (β : Type u_7) [preorder α] [preorder β] :
Type (max u_6 u_7)

Bundled monotone (aka, increasing) function

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

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

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

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

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

You should extend this class when you extend order_iso.

Instances of this typeclass
Instances of other typeclasses for order_iso_class
  • order_iso_class.has_sizeof_inst
source
@[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 : order_iso_class F α β] :
equiv_like F α β
source
@[protected, instance]
def order_iso.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [order_iso_class F α β] :
has_coe_t F (α ≃o β)
Equations
source
@[protected, instance]
def order_iso_class.to_order_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [order_iso_class F α β] :
order_hom_class F α β
Equations
source
@[protected]
theorem order_hom_class.monotone {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_hom_class F α β] (f : F) :
monotone ⇑f
source
@[protected]
theorem order_hom_class.mono {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_hom_class F α β] (f : F) :
monotone ⇑f
source
@[protected, instance]
def order_hom_class.order_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_hom_class F α β] :
has_coe_t F (α →o β)
Equations
source
@[simp]
theorem map_inv_le_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [order_iso_class F α β] (f : F) {a : α} {b : β} :
equiv_like.inv f b ≤ a ↔ b ≤ ⇑f a
source
@[simp]
theorem le_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [order_iso_class F α β] (f : F) {a : α} {b : β} :
a ≤ equiv_like.inv f b ↔ ⇑f a ≤ b
source
theorem map_lt_map_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_iso_class F α β] (f : F) {a b : α} :
⇑f a < ⇑f b ↔ a < b
source
@[simp]
theorem map_inv_lt_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_iso_class F α β] (f : F) {a : α} {b : β} :
equiv_like.inv f b < a ↔ b < ⇑f a
source
@[simp]
theorem lt_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_iso_class F α β] (f : F) {a : α} {b : β} :
a < equiv_like.inv f b ↔ ⇑f a < b
source
@[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
source
@[protected]
theorem order_hom.monotone {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :
monotone ⇑f
source
@[protected]
theorem order_hom.mono {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :
monotone ⇑f
source
@[protected, instance]
def order_hom.order_hom_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
order_hom_class (α →o β) α β
Equations
source
@[simp]
theorem order_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f : α →o β} :
f.to_fun = ⇑f
source
@[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
source
@[ext]
theorem order_hom.ext {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f g : α →o β) (h : ⇑f = ⇑g) :
f = g
source
theorem order_hom.coe_eq {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :
↑f = f
source
@[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
source
@[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
source
@[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'
source
theorem order_hom.copy_eq {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
@[simp]
theorem order_hom.id_coe {α : Type u_2} [preorder α] :
⇑order_hom.id = id
source
def order_hom.id {α : Type u_2} [preorder α] :
α →o α

The identity function as bundled monotone function.

Equations
source
@[protected, instance]
def order_hom.inhabited {α : Type u_2} [preorder α] :
inhabited (α →o α)
Equations
source
@[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
source
@[protected, instance]
def order_hom.partial_order {α : Type u_2} [preorder α] {β : Type u_1} [partial_order β] :
partial_order (α →o β)
Equations
source
theorem order_hom.le_def {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f g : α →o β} :
f ≤ g ↔ ∀ (x : α), ⇑f x ≤ ⇑g x
source
@[simp, norm_cast]
theorem order_hom.coe_le_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f g : α →o β} :
⇑f ≤ ⇑g ↔ f ≤ g
source
@[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
source
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
source
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
source
@[simp]
theorem order_hom.curry_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (f : α × β →o γ) (x : α) (y : β) :
⇑(⇑(⇑order_hom.curry f) x) y = ⇑f (x, y)
source
@[simp]
theorem order_hom.curry_symm_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : β →o γ) (f : α →o β) :
⇑(g.comp f) = ⇑g ∘ ⇑f
source
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₂
source
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
source
@[simp]
theorem order_hom.compₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (x : β →o γ) (ᾰ : α →o β) :
⇑(⇑(⇑order_hom.compₘ x) ᾰ) = ⇑x ∘ ⇑ᾰ
source
@[simp]
theorem order_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :
f.comp order_hom.id = f
source
@[simp]
theorem order_hom.id_comp {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} [preorder α] [preorder β] (γ : Type u_1) [preorder γ] (f : α →o β) (c : α) :
f.comp (⇑(order_hom.const γ) c) = ⇑(order_hom.const γ) (⇑f c)
source
@[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
source
@[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)
source
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₂
source
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
source
@[simp]
theorem order_hom.prodₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (x : α →o β) (ᾰ : α →o γ) (x_1 : α) :
⇑(⇑(⇑order_hom.prodₘ x) ᾰ) x_1 = (⇑x x_1, ⇑ᾰ x_1)
source
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
source
@[simp]
theorem order_hom.diag_coe {α : Type u_2} [preorder α] (x : α) :
⇑order_hom.diag x = (x, x)
source
def order_hom.diag {α : Type u_2} [preorder α] :
α →o α × α

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

Equations
source
@[simp]
theorem order_hom.on_diag_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o α →o β) (ᾰ : α) :
⇑(f.on_diag) ᾰ = ⇑(⇑f ᾰ) ᾰ
source
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
source
def order_hom.fst {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
α × β →o α

prod.fst as a order_hom.

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

prod.snd as a order_hom.

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

prod.map of two order_homs as a order_hom.

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

subtype.val as a bundled monotone function.

Equations
source
@[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
source
theorem order_hom.order_hom_eq_id {α : Type u_2} [preorder α] [subsingleton α] (g : α →o α) :
g = order_hom.id
source
@[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
source
@[simp]
theorem order_hom.dual_apply_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) (ᾰ : αᵒᵈ) :
⇑(⇑order_hom.dual f) ᾰ = (⇑order_dual.to_dual ∘ ⇑f ∘ ⇑order_dual.of_dual) ᾰ
source
@[simp]
theorem order_hom.dual_symm_apply_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : αᵒᵈ →o βᵒᵈ) (ᾰ : α) :
⇑(⇑(order_hom.dual.symm) f) ᾰ = (⇑order_dual.of_dual ∘ ⇑f ∘ ⇑order_dual.to_dual) ᾰ
source
@[simp]
theorem order_hom.dual_id {α : Type u_2} [preorder α] :
⇑order_hom.dual order_hom.id = order_hom.id
source
@[simp]
theorem order_hom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : β →o γ) (f : α →o β) :
⇑order_hom.dual (g.comp f) = (⇑order_hom.dual g).comp (⇑order_hom.dual f)
source
@[simp]
theorem order_hom.symm_dual_id {α : Type u_2} [preorder α] :
⇑(order_hom.dual.symm) order_hom.id = order_hom.id
source
@[simp]
theorem order_hom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : βᵒᵈ →o γᵒᵈ) (f : αᵒᵈ →o βᵒᵈ) :
⇑(order_hom.dual.symm) (g.comp f) = (⇑(order_hom.dual.symm) g).comp (⇑(order_hom.dual.symm) f)
source
def order_hom.dual_iso (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :
(α →o β) ≃o (αᵒᵈ →o βᵒᵈ)ᵒᵈ

order_hom.dual as an order isomorphism.

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

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

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

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

Equations
source
@[simp]
theorem order_hom.with_top_map_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α →o β) :
⇑(f.with_top_map) = with_top.map ⇑f
source
def rel_embedding.order_embedding_of_lt_embedding {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (f : has_lt.lt ↪r has_lt.lt) :
α ↪o β

Embeddings of partial orders that preserve < also preserve ≤.

Equations
source
@[simp]
theorem rel_embedding.order_embedding_of_lt_embedding_apply {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [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_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) (x : α) :
⇑(f.lt_embedding) x = ⇑f x
source
@[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
source
@[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
source
@[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
source
@[protected]
theorem order_embedding.monotone {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :
monotone ⇑f
source
@[protected]
theorem order_embedding.strict_mono {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :
strict_mono ⇑f
source
@[protected]
theorem order_embedding.acc {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :
well_founded has_lt.lt → well_founded has_lt.lt
source
@[protected]
theorem order_embedding.is_well_order {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) [is_well_order β has_lt.lt] :
is_well_order α has_lt.lt
source
@[protected]
def order_embedding.dual {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :
αᵒᵈ ↪o βᵒᵈ

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

Equations
source
@[protected]
def order_embedding.with_bot_map {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :
with_bot α ↪o with_bot β

A version of with_bot.map for order embeddings.

Equations
source
@[simp]
theorem order_embedding.with_bot_map_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :
⇑(f.with_bot_map) = with_bot.map ⇑f
source
@[simp]
theorem order_embedding.with_top_map_apply {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :
⇑(f.with_top_map) = with_top.map ⇑f
source
@[protected]
def order_embedding.with_top_map {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : α ↪o β) :
with_top α ↪o with_top β

A version of with_top.map for order embeddings.

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_2} [preorder α] (p : α → Prop) :
⇑(order_embedding.subtype p) = coe
source
def order_embedding.subtype {α : Type u_2} [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_2} {β : Type u_3} [partial_order α] [preorder β] (f : has_lt.lt →r has_lt.lt) :
α →o β

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

Equations
source
@[simp]
theorem rel_hom.to_order_hom_coe {α : Type u_2} {β : Type u_3} [partial_order α] [preorder β] (f : has_lt.lt →r has_lt.lt) :
⇑(f.to_order_hom) = ⇑f
source
theorem rel_embedding.to_order_hom_injective {α : Type u_2} {β : Type u_3} [partial_order α] [preorder β] (f : has_lt.lt ↪r has_lt.lt) :
function.injective ⇑(↑f.to_order_hom)
source
@[protected, instance]
def order_iso.order_iso_class {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] :
order_iso_class (α ≃o β) α β
Equations
source
@[simp]
theorem order_iso.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] {f : α ≃o β} :
f.to_equiv.to_fun = ⇑f
source
@[ext]
theorem order_iso.ext {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] {f g : α ≃o β} (h : ⇑f = ⇑g) :
f = g
source
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
source
@[simp]
theorem order_iso.coe_to_order_embedding {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
⇑(e.to_order_embedding) = ⇑e
source
@[protected]
theorem order_iso.bijective {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
function.bijective ⇑e
source
@[protected]
theorem order_iso.injective {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
function.injective ⇑e
source
@[protected]
theorem order_iso.surjective {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
function.surjective ⇑e
source
@[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
source
def order_iso.refl (α : Type u_1) [has_le α] :
α ≃o α

Identity order isomorphism.

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

Inverse of an order isomorphism.

Equations
source
@[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
source
@[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
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_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) (x : α) (y : β) :
⇑e x = y ↔ x = ⇑(e.symm) y
source
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
source
@[simp]
theorem order_iso.symm_symm {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
e.symm.symm = e
source
theorem order_iso.symm_injective {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] :
function.injective order_iso.symm
source
@[simp]
theorem order_iso.to_equiv_symm {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
e.to_equiv.symm = e.symm.to_equiv
source
@[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
source
@[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
source
@[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)
source
@[simp]
theorem order_iso.refl_trans {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
(order_iso.refl α).trans e = e
source
@[simp]
theorem order_iso.trans_refl {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (e : α ≃o β) :
e.trans (order_iso.refl β) = e
source
@[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)
source
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
source
def order_iso.prod_comm {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] :
α × β ≃o β × α

prod.swap as an order_iso.

Equations
source
@[simp]
theorem order_iso.coe_prod_comm {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] :
⇑order_iso.prod_comm = prod.swap
source
@[simp]
theorem order_iso.prod_comm_symm {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] :
order_iso.prod_comm.symm = order_iso.prod_comm
source
def order_iso.dual_dual (α : Type u_2) [has_le α] :
α ≃o αᵒᵈᵒᵈ

The order isomorphism between a type and its double dual.

Equations
source
@[simp]
theorem order_iso.coe_dual_dual (α : Type u_2) [has_le α] :
⇑(order_iso.dual_dual α) = ⇑order_dual.to_dual ∘ ⇑order_dual.to_dual
source
@[simp]
theorem order_iso.coe_dual_dual_symm (α : Type u_2) [has_le α] :
⇑((order_iso.dual_dual α).symm) = ⇑order_dual.of_dual ∘ ⇑order_dual.of_dual
source
@[simp]
theorem order_iso.dual_dual_apply {α : Type u_2} [has_le α] (a : α) :
⇑(order_iso.dual_dual α) a = ⇑order_dual.to_dual (⇑order_dual.to_dual a)
source
@[simp]
theorem order_iso.dual_dual_symm_apply {α : Type u_2} [has_le α] (a : αᵒᵈᵒᵈ) :
⇑((order_iso.dual_dual α).symm) a = ⇑order_dual.of_dual (⇑order_dual.of_dual a)
source
@[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
source
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
source
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
source
@[protected]
theorem order_iso.monotone {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α ≃o β) :
monotone ⇑e
source
@[protected]
theorem order_iso.strict_mono {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α ≃o β) :
strict_mono ⇑e
source
@[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
source
def order_iso.to_rel_iso_lt {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (e : α ≃o β) :
has_lt.lt ≃r has_lt.lt

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

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

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

Equations
source
@[simp]
theorem order_iso.of_rel_iso_lt_apply {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (e : has_lt.lt ≃r has_lt.lt) (x : α) :
⇑(order_iso.of_rel_iso_lt e) x = ⇑e x
source
@[simp]
theorem order_iso.of_rel_iso_lt_symm {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (e : has_lt.lt ≃r has_lt.lt) :
(order_iso.of_rel_iso_lt e).symm = order_iso.of_rel_iso_lt e.symm
source
@[simp]
theorem order_iso.of_rel_iso_lt_to_rel_iso_lt {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (e : α ≃o β) :
order_iso.of_rel_iso_lt e.to_rel_iso_lt = e
source
@[simp]
theorem order_iso.to_rel_iso_lt_of_rel_iso_lt {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (e : has_lt.lt ≃r has_lt.lt) :
(order_iso.of_rel_iso_lt e).to_rel_iso_lt = e
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.of_hom_inv {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {F : Type u_1} {G : Type u_4} [order_hom_class F α β] [order_hom_class G β α] (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
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 : α), (λ (a' : α), (λ (ᾰ : α), β) a') x) :
⇑(order_iso.fun_unique α β) f = f inhabited.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_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
source
@[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
source
@[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
source
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 : function.right_inverse g f) :
α ≃o β

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

Equations
source
@[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 : function.right_inverse g f) :
⇑(rel_iso.symm (strict_mono.order_iso_of_right_inverse f h_mono g hg)) = g
source
@[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 : function.right_inverse g f) :
⇑(strict_mono.order_iso_of_right_inverse f h_mono g hg) = f
source
@[protected]
def order_iso.dual {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] (f : α ≃o β) :
αᵒᵈ ≃o βᵒᵈ

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

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

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

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

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

source
@[simp]
theorem disjoint_map_order_iso_iff {α : Type u_2} {β : Type u_3} [semilattice_inf α] [order_bot α] [semilattice_inf β] [order_bot β] {a b : α} (f : α ≃o β) :
disjoint (⇑f a) (⇑f b) ↔ disjoint a b
source
@[simp]
theorem codisjoint_map_order_iso_iff {α : Type u_2} {β : Type u_3} [semilattice_sup α] [order_top α] [semilattice_sup β] [order_top β] {a b : α} (f : α ≃o β) :
codisjoint (⇑f a) (⇑f b) ↔ codisjoint a b
source
@[protected]
def with_bot.to_dual_top_equiv {α : Type u_2} [has_le α] :
with_bot αᵒᵈ ≃o (with_top α)ᵒᵈ

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
source
@[simp]
theorem with_bot.to_dual_top_equiv_coe {α : Type u_2} [has_le α] (a : α) :
⇑with_bot.to_dual_top_equiv ↑(⇑order_dual.to_dual a) = ⇑order_dual.to_dual ↑a
source
@[simp]
theorem with_bot.to_dual_top_equiv_symm_coe {α : Type u_2} [has_le α] (a : α) :
⇑(with_bot.to_dual_top_equiv.symm) (⇑order_dual.to_dual ↑a) = ↑(⇑order_dual.to_dual a)
source
@[simp]
theorem with_bot.to_dual_top_equiv_bot {α : Type u_2} [has_le α] :
⇑with_bot.to_dual_top_equiv ⊥ = ⊥
source
@[simp]
theorem with_bot.to_dual_top_equiv_symm_bot {α : Type u_2} [has_le α] :
⇑(with_bot.to_dual_top_equiv.symm) ⊥ = ⊥
source
theorem with_bot.coe_to_dual_top_equiv_eq {α : Type u_2} [has_le α] :
⇑with_bot.to_dual_top_equiv = ⇑order_dual.to_dual ∘ ⇑with_bot.of_dual
source
@[protected]
def with_top.to_dual_bot_equiv {α : Type u_2} [has_le α] :
with_top αᵒᵈ ≃o (with_bot α)ᵒᵈ

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
source
@[simp]
theorem with_top.to_dual_bot_equiv_coe {α : Type u_2} [has_le α] (a : α) :
⇑with_top.to_dual_bot_equiv ↑(⇑order_dual.to_dual a) = ⇑order_dual.to_dual ↑a
source
@[simp]
theorem with_top.to_dual_bot_equiv_symm_coe {α : Type u_2} [has_le α] (a : α) :
⇑(with_top.to_dual_bot_equiv.symm) (⇑order_dual.to_dual ↑a) = ↑(⇑order_dual.to_dual a)
source
@[simp]
theorem with_top.to_dual_bot_equiv_top {α : Type u_2} [has_le α] :
⇑with_top.to_dual_bot_equiv ⊤ = ⊤
source
@[simp]
theorem with_top.to_dual_bot_equiv_symm_top {α : Type u_2} [has_le α] :
⇑(with_top.to_dual_bot_equiv.symm) ⊤ = ⊤
source
theorem with_top.coe_to_dual_bot_equiv_eq {α : Type u_2} [has_le α] :
⇑with_top.to_dual_bot_equiv = ⇑order_dual.to_dual ∘ ⇑with_top.of_dual
source
@[simp]
theorem order_iso.with_top_congr_apply {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) (o : option α) :
⇑(e.with_top_congr) o = option.map ⇑e o
source
def order_iso.with_top_congr {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) :
with_top α ≃o with_top β

A version of equiv.option_congr for with_top.

Equations
source
@[simp]
theorem order_iso.with_top_congr_refl {α : Type u_2} [partial_order α] :
(order_iso.refl α).with_top_congr = order_iso.refl (with_top α)
source
@[simp]
theorem order_iso.with_top_congr_symm {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) :
e.with_top_congr.symm = e.symm.with_top_congr
source
@[simp]
theorem order_iso.with_top_congr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [partial_order α] [partial_order β] [partial_order γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
e₁.with_top_congr.trans e₂.with_top_congr = (e₁.trans e₂).with_top_congr
source
def order_iso.with_bot_congr {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) :
with_bot α ≃o with_bot β

A version of equiv.option_congr for with_bot.

Equations
source
@[simp]
theorem order_iso.with_bot_congr_apply {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) (o : option α) :
⇑(e.with_bot_congr) o = option.map ⇑e o
source
@[simp]
theorem order_iso.with_bot_congr_refl {α : Type u_2} [partial_order α] :
(order_iso.refl α).with_bot_congr = order_iso.refl (with_bot α)
source
@[simp]
theorem order_iso.with_bot_congr_symm {α : Type u_2} {β : Type u_3} [partial_order α] [partial_order β] (e : α ≃o β) :
e.with_bot_congr.symm = e.symm.with_bot_congr
source
@[simp]
theorem order_iso.with_bot_congr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [partial_order α] [partial_order β] [partial_order γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) :
e₁.with_bot_congr.trans e₂.with_bot_congr = (e₁.trans e₂).with_bot_congr
source
theorem order_iso.is_compl {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) {x y : α} (h : is_compl x y) :
is_compl (⇑f x) (⇑f y)
source
theorem order_iso.is_compl_iff {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) {x y : α} :
is_compl x y ↔ is_compl (⇑f x) (⇑f y)
source
theorem order_iso.complemented_lattice {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) [complemented_lattice α] :
complemented_lattice β
source
theorem order_iso.complemented_lattice_iff {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β) :
complemented_lattice α ↔ complemented_lattice β