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) [Preorder α] [Preorder β] : 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.

def «term_→o_» : Lean.TrailingParserDescr

Notation for an OrderHom.

Equations

• «term_→o_» = Lean.ParserDescr.trailingNode `«term_→o_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →o ") (Lean.ParserDescr.cat `term 25))

@[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 (x1 x2 : α) => x1 ≤ x2) ↪r fun (x1 x2 : β) => x1 ≤ x2)

def «term_↪o_» : Lean.TrailingParserDescr

Notation for an OrderEmbedding.

Equations

• «term_↪o_» = Lean.ParserDescr.trailingNode `«term_↪o_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↪o ") (Lean.ParserDescr.cat `term 26))

@[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 (x1 x2 : α) => x1 ≤ x2) ≃r fun (x1 x2 : β) => x1 ≤ x2)

def «term_≃o_» : Lean.TrailingParserDescr

Notation for an OrderIso.

Equations

• «term_≃o_» = Lean.ParserDescr.trailingNode `«term_≃o_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃o ") (Lean.ParserDescr.cat `term 26))

@[reducible, inline]

abbrev OrderHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [LE α] [LE β] [FunLike F α β] : Prop

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

Equations

• OrderHomClass F α β = RelHomClass F (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : β) => x1 ≤ x2

class OrderIsoClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [LE α] [LE β] [EquivLike F α β] : Prop

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 ≤.

def OrderIsoClass.toOrderIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass 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 = { toEquiv := ↑f, map_rel_iff' := ⋯ }

instance instCoeTCOrderIsoOfOrderIsoClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass 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 α β] [OrderIsoClass F α β] : OrderHomClass F α β

theorem OrderHomClass.monotone {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass F α β] (f : F) : Monotone ⇑f

theorem OrderHomClass.mono {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass F α β] (f : F) : Monotone ⇑f

theorem OrderHomClass.GCongr.mono {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass F α β] (f : F) {a b : α} (hab : a ≤ b) : f a ≤ f b

def OrderHomClass.toOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass 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' := ⋯ }

instance OrderHomClass.instCoeTCOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [FunLike F α β] [OrderHomClass 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 α β] [OrderIsoClass F α β] (f : F) {a : α} {b : β} : EquivLike.inv f b ≤ a ↔ b ≤ f a

theorem map_inv_le_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a b : β} : EquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a

@[simp]

theorem le_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a : α} {b : β} : a ≤ EquivLike.inv f b ↔ f a ≤ b

theorem map_lt_map_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a b : α} : f a < f b ↔ a < b

@[simp]

theorem map_inv_lt_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a : α} {b : β} : EquivLike.inv f b < a ↔ b < f a

theorem map_inv_lt_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a b : β} : EquivLike.inv f b < EquivLike.inv f a ↔ b < a

@[simp]

theorem lt_map_inv_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) {a : α} {b : β} : a < EquivLike.inv f b ↔ f a < b

instance OrderHom.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : FunLike (α →o β) α β

Equations

• OrderHom.instFunLike = { coe := OrderHom.toFun, coe_injective' := ⋯ }

instance OrderHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : OrderHomClass (α →o β) α β

@[simp]

theorem OrderHom.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α → β) (hf : Monotone f) : ⇑{ toFun := f, monotone' := hf } = f

theorem OrderHom.monotone {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : Monotone ⇑f

theorem OrderHom.mono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : Monotone ⇑f

def OrderHom.Simps.coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : α → β

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

Equations

• OrderHom.Simps.coe f = ⇑f

@[simp]

theorem OrderHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : f.toFun = ⇑f

theorem OrderHom.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f g : α →o β) (h : ⇑f = ⇑g) : f = g

theorem OrderHom.ext_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f g : α →o β} : f = g ↔ ⇑f = ⇑g

@[simp]

theorem OrderHom.coe_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : ↑f = f

@[simp]

theorem OrderHomClass.coe_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {F : Type u_6} [FunLike F α β] [OrderHomClass F α β] (f : F) : ⇑↑f = ⇑f

instance OrderHom.canLift {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : CanLift (α → β) (α →o β) DFunLike.coe Monotone

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

def OrderHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (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' := ⋯ }

@[simp]

theorem OrderHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem OrderHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

def OrderHom.id {α : Type u_2} [Preorder α] : α →o α

The identity function as bundled monotone function.

Equations

• OrderHom.id = { toFun := id, monotone' := ⋯ }

@[simp]

theorem OrderHom.id_coe {α : Type u_2} [Preorder α] : ⇑id = _root_.id

instance OrderHom.instInhabited {α : Type u_2} [Preorder α] : Inhabited (α →o α)

Equations

• OrderHom.instInhabited = { default := OrderHom.id }

instance OrderHom.instPreorder {α : 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

• OrderHom.instPreorder = Preorder.lift OrderHom.toFun

instance OrderHom.instPartialOrder {α : Type u_2} [Preorder α] {β : Type u_6} [PartialOrder β] : PartialOrder (α →o β)

Equations

• OrderHom.instPartialOrder = PartialOrder.lift OrderHom.toFun ⋯

theorem OrderHom.le_def {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f g : α →o β} : f ≤ g ↔ ∀ (x : α), f x ≤ g x

@[simp]

theorem OrderHom.coe_le_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f g : α →o β} : ⇑f ≤ ⇑g ↔ f ≤ g

@[simp]

theorem OrderHom.mk_le_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f g : α → β} {hf : Monotone f} {hg : Monotone g} : { toFun := f, monotone' := hf } ≤ { toFun := g, monotone' := hg } ↔ f ≤ g

theorem OrderHom.apply_mono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f g : α →o β} {x y : α} (h₁ : f ≤ g) (h₂ : x ≤ y) : f x ≤ g y

def OrderHom.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

• One or more equations did not get rendered due to their size.

@[simp]

theorem OrderHom.curry_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α × β →o γ) (x : α) (y : β) : ((curry f) x) y = f (x, y)

@[simp]

theorem OrderHom.curry_symm_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β →o γ) (x : α × β) : ((RelIso.symm curry) f) x = (f x.1) x.2

def OrderHom.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

• g.comp f = { toFun := ⇑g ∘ ⇑f, monotone' := ⋯ }

@[simp]

theorem OrderHom.comp_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (g : β →o γ) (f : α →o β) : ⇑(g.comp f) = ⇑g ∘ ⇑f

theorem OrderHom.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₂

@[simp]

theorem OrderHom.mk_comp_mk {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (g : β → γ) (f : α → β) (hg : Monotone g) (hf : Monotone f) : { toFun := g, monotone' := hg }.comp { toFun := f, monotone' := hf } = { toFun := g ∘ f, monotone' := ⋯ }

def OrderHom.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

• OrderHom.compₘ = OrderHom.curry { toFun := fun (f : (β →o γ) × (α →o β)) => f.1.comp f.2, monotone' := ⋯ }

@[simp]

theorem OrderHom.compₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (x : β →o γ) (a✝ : α →o β) : ⇑((compₘ x) a✝) = ⇑x ∘ ⇑a✝

@[simp]

theorem OrderHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : f.comp id = f

@[simp]

theorem OrderHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : id.comp f = f

def OrderHom.const (α : Type u_6) [Preorder α] {β : Type u_7} [Preorder β] : β →o α →o β

Constant function bundled as an OrderHom.

Equations

• OrderHom.const α = { toFun := fun (b : β) => { toFun := Function.const α b, monotone' := ⋯ }, monotone' := ⋯ }

@[simp]

theorem OrderHom.const_coe_coe (α : Type u_6) [Preorder α] {β : Type u_7} [Preorder β] (b : β) : ⇑((const α) b) = Function.const α b

@[simp]

theorem OrderHom.const_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (c : γ) : ((const β) c).comp f = (const α) c

@[simp]

theorem OrderHom.comp_const {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (γ : Type u_6) [Preorder γ] (f : α →o β) (c : α) : f.comp ((const γ) c) = (const γ) (f c)

def OrderHom.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 OrderHom.

Equations

• f.prod g = { toFun := fun (x : α) => (f x, g x), monotone' := ⋯ }

@[simp]

theorem OrderHom.prod_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (g : α →o γ) (x : α) : (f.prod g) x = (f x, g x)

theorem OrderHom.prod_mono {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] {f₁ f₂ : α →o β} (hf : f₁ ≤ f₂) {g₁ g₂ : α →o γ} (hg : g₁ ≤ g₂) : f₁.prod g₁ ≤ f₂.prod g₂

theorem OrderHom.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

def OrderHom.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 OrderHom. This is a fully bundled version.

Equations

• OrderHom.prodₘ = OrderHom.curry { toFun := fun (f : (α →o β) × (α →o γ)) => f.1.prod f.2, monotone' := ⋯ }

@[simp]

theorem OrderHom.prodₘ_coe_coe_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (x : α →o β) (a✝ : α →o γ) (x✝ : α) : ((prodₘ x) a✝) x✝ = (x x✝, a✝ x✝)

def OrderHom.diag {α : Type u_2} [Preorder α] : α →o α × α

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

Equations

• OrderHom.diag = OrderHom.id.prod OrderHom.id

@[simp]

theorem OrderHom.diag_coe {α : Type u_2} [Preorder α] (x : α) : diag x = (x, x)

def OrderHom.onDiag {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o α →o β) : α →o β

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

Equations

• f.onDiag = ((RelIso.symm OrderHom.curry) f).comp OrderHom.diag

@[simp]

theorem OrderHom.onDiag_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o α →o β) (a✝ : α) : f.onDiag a✝ = (f a✝) a✝

def OrderHom.fst {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : α × β →o α

Prod.fst as an OrderHom.

Equations

• OrderHom.fst = { toFun := Prod.fst, monotone' := ⋯ }

@[simp]

theorem OrderHom.fst_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (self : α × β) : fst self = self.1

def OrderHom.snd {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : α × β →o β

Prod.snd as an OrderHom.

Equations

• OrderHom.snd = { toFun := Prod.snd, monotone' := ⋯ }

@[simp]

theorem OrderHom.snd_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (self : α × β) : snd self = self.2

@[simp]

theorem OrderHom.fst_prod_snd {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : fst.prod snd = id

@[simp]

theorem OrderHom.fst_comp_prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (g : α →o γ) : fst.comp (f.prod g) = f

@[simp]

theorem OrderHom.snd_comp_prod {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (g : α →o γ) : snd.comp (f.prod g) = g

def OrderHom.prodIso {α : 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem OrderHom.prodIso_symm_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : (α →o β) × (α →o γ)) : (RelIso.symm prodIso) f = f.1.prod f.2

@[simp]

theorem OrderHom.prodIso_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β × γ) : prodIso f = (fst.comp f, snd.comp f)

def OrderHom.prodMap {α : 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 OrderHoms as an OrderHom

Equations

• f.prodMap g = { toFun := Prod.map ⇑f ⇑g, monotone' := ⋯ }

@[simp]

theorem OrderHom.prodMap_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (f : α →o β) (g : γ →o δ) (a✝ : α × γ) : (f.prodMap g) a✝ = Prod.map (⇑f) (⇑g) a✝

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

• Pi.evalOrderHom i = { toFun := Function.eval i, monotone' := ⋯ }

@[simp]

theorem Pi.evalOrderHom_coe {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → Preorder (π i)] (i : ι) : ⇑(evalOrderHom i) = Function.eval i

def OrderHom.coeFnHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : (α →o β) →o α → β

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

Equations

• OrderHom.coeFnHom = { toFun := fun (f : α →o β) => ⇑f, monotone' := ⋯ }

@[simp]

theorem OrderHom.coeFnHom_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : ⇑coeFnHom = fun (f : α →o β) => ⇑f

def OrderHom.apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (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

• OrderHom.apply x = (Pi.evalOrderHom x).comp OrderHom.coeFnHom

@[simp]

theorem OrderHom.apply_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (x : α) : ⇑(apply x) = Function.eval x ∘ fun (f : α →o β) => ⇑f

def OrderHom.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

• OrderHom.pi f = { toFun := fun (x : α) (i : ι) => (f i) x, monotone' := ⋯ }

@[simp]

theorem OrderHom.pi_coe {α : Type u_2} [Preorder α] {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → Preorder (π i)] (f : (i : ι) → α →o π i) (x : α) (i : ι) : (pi f) x i = (f i) x

def OrderHom.piIso {α : 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

• OrderHom.piIso = { toFun := fun (f : α →o (i : ι) → π i) (i : ι) => (Pi.evalOrderHom i).comp f, invFun := OrderHom.pi, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem OrderHom.piIso_apply {α : Type u_2} [Preorder α] {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → Preorder (π i)] (f : α →o (i : ι) → π i) (i : ι) : piIso f i = (Pi.evalOrderHom i).comp f

@[simp]

theorem OrderHom.piIso_symm_apply {α : Type u_2} [Preorder α] {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → Preorder (π i)] (f : (i : ι) → α →o π i) : (RelIso.symm piIso) f = pi f

def OrderHom.Subtype.val {α : Type u_2} [Preorder α] (p : α → Prop) : Subtype p →o α

Subtype.val as a bundled monotone function.

Equations

• OrderHom.Subtype.val p = { toFun := Subtype.val, monotone' := ⋯ }

@[simp]

theorem OrderHom.Subtype.val_coe {α : Type u_2} [Preorder α] (p : α → Prop) : ⇑(val p) = _root_.Subtype.val

def Subtype.orderEmbedding {α : Type u_2} [Preorder α] {p q : α → Prop} (h : ∀ (a : α), p a → q a) : { x : α // p x } ↪o { x : α // q x }

Subtype.impEmbedding as an order embedding.

Equations

• Subtype.orderEmbedding h = { toEmbedding := Subtype.impEmbedding p q h, map_rel_iff' := ⋯ }

@[simp]

theorem Subtype.orderEmbedding_apply_coe {α : Type u_2} [Preorder α] {p q : α → Prop} (h : ∀ (a : α), p a → q a) (x : { x : α // p x }) : ↑((orderEmbedding h) x) = ↑x

instance OrderHom.unique {α : Type u_2} [Preorder α] [Subsingleton α] : 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} [Preorder α] [Subsingleton α] (g : α →o α) : g = id

def OrderHom.dual {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : (α →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.

@[simp]

theorem OrderHom.dual_symm_apply_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : αᵒᵈ →o βᵒᵈ) (a✝ : α) : (OrderHom.dual.symm f) a✝ = (⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual) a✝

@[simp]

theorem OrderHom.dual_apply_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (a✝ : αᵒᵈ) : (OrderHom.dual f) a✝ = (⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual) a✝

@[simp]

theorem OrderHom.dual_id {α : Type u_2} [Preorder α] : OrderHom.dual id = id

@[simp]

theorem OrderHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (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} [Preorder α] : OrderHom.dual.symm id = id

@[simp]

theorem OrderHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (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) [Preorder α] [Preorder β] : (α →o β) ≃o (αᵒᵈ →o βᵒᵈ)ᵒᵈ

OrderHom.dual as an order isomorphism.

Equations

• OrderHom.dualIso α β = { toEquiv := OrderHom.dual.trans OrderDual.toDual, map_rel_iff' := ⋯ }

def OrderHom.uliftMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : ULift.{u_8, u_2} α →o ULift.{u_9, u_3} β

Lift an order homomorphism f : α →o β to an order homomorphism ULift α →o ULift β in a higher universe.

Equations

• f.uliftMap = { toFun := fun (i : ULift.{?u.25, ?u.27} α) => { down := f i.down }, monotone' := ⋯ }

@[simp]

theorem OrderHom.uliftMap_coe_down {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (i : ULift.{u_8, u_2} α) : (f.uliftMap i).down = f i.down

@[instance 90]

instance OrderHomClass.toOrderHomClassOrderDual {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [FunLike F α β] [OrderHomClass F α β] : OrderHomClass F αᵒᵈ βᵒᵈ

def RelEmbedding.orderEmbeddingOfLTEmbedding {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ↪r fun (x1 x2 : β) => x1 < x2) : α ↪o β

Embeddings of partial orders that preserve < also preserve ≤.

Equations

• f.orderEmbeddingOfLTEmbedding = { toEmbedding := f.toEmbedding, map_rel_iff' := ⋯ }

@[simp]

theorem RelEmbedding.orderEmbeddingOfLTEmbedding_apply {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] {f : (fun (x1 x2 : α) => x1 < x2) ↪r fun (x1 x2 : β) => x1 < x2} {x : α} : f.orderEmbeddingOfLTEmbedding x = f x

def OrderEmbedding.ltEmbedding {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) : (fun (x1 x2 : α) => x1 < x2) ↪r fun (x1 x2 : β) => x1 < x2

< is preserved by order embeddings of preorders.

Equations

• f.ltEmbedding = { toEmbedding := f.toEmbedding, map_rel_iff' := ⋯ }

@[simp]

theorem OrderEmbedding.ltEmbedding_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) (x : α) : f.ltEmbedding x = f x

@[simp]

theorem OrderEmbedding.le_iff_le {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) {a b : α} : f a ≤ f b ↔ a ≤ b

@[simp]

theorem OrderEmbedding.lt_iff_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) {a b : α} : f a < f b ↔ a < b

theorem OrderEmbedding.eq_iff_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) {a b : α} : f a = f b ↔ a = b

theorem OrderEmbedding.monotone {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) : Monotone ⇑f

theorem OrderEmbedding.strictMono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) : StrictMono ⇑f

theorem OrderEmbedding.acc {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) (a : α) : Acc (fun (x1 x2 : β) => x1 < x2) (f a) → Acc (fun (x1 x2 : α) => x1 < x2) a

theorem OrderEmbedding.wellFounded {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) : (WellFounded fun (x1 x2 : β) => x1 < x2) → WellFounded fun (x1 x2 : α) => x1 < x2

theorem OrderEmbedding.isWellOrder {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [IsWellOrder β fun (x1 x2 : β) => x1 < x2] (f : α ↪o β) : IsWellOrder α fun (x1 x2 : α) => x1 < x2

def OrderEmbedding.dual {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) : αᵒᵈ ↪o βᵒᵈ

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

Equations

• f.dual = { toEmbedding := f.toEmbedding, map_rel_iff' := ⋯ }

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

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

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

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

def OrderEmbedding.ofMapLEIff {α : Type u_6} {β : Type u_7} [PartialOrder α] [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

• OrderEmbedding.ofMapLEIff f hf = RelEmbedding.ofMapRelIff f hf

@[simp]

theorem OrderEmbedding.coe_ofMapLEIff {α : Type u_6} {β : Type u_7} [PartialOrder α] [Preorder β] {f : α → β} (h : ∀ (a b : α), f a ≤ f b ↔ a ≤ b) : ⇑(ofMapLEIff f h) = f

def OrderEmbedding.ofStrictMono {α : Type u_6} {β : Type u_7} [LinearOrder α] [Preorder β] (f : α → β) (h : StrictMono f) : α ↪o β

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

Equations

• OrderEmbedding.ofStrictMono f h = OrderEmbedding.ofMapLEIff f ⋯

@[simp]

theorem OrderEmbedding.coe_ofStrictMono {α : Type u_6} {β : Type u_7} [LinearOrder α] [Preorder β] {f : α → β} (h : StrictMono f) : ⇑(ofStrictMono f h) = f

def OrderEmbedding.subtype {α : Type u_2} [Preorder α] (p : α → Prop) : Subtype p ↪o α

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

Equations

• OrderEmbedding.subtype p = { toEmbedding := Function.Embedding.subtype p, map_rel_iff' := ⋯ }

@[simp]

theorem OrderEmbedding.subtype_apply {α : Type u_2} [Preorder α] {p : α → Prop} (x : Subtype p) : (subtype p) x = ↑x

theorem OrderEmbedding.subtype_injective {α : Type u_2} [Preorder α] (p : α → Prop) : Function.Injective ⇑(subtype p)

@[simp]

theorem OrderEmbedding.coe_subtype {α : Type u_2} [Preorder α] (p : α → Prop) : ⇑(subtype p) = Subtype.val

def OrderEmbedding.toOrderHom {X : Type u_6} {Y : Type u_7} [Preorder X] [Preorder Y] (f : X ↪o Y) : X →o Y

Convert an OrderEmbedding to an OrderHom.

Equations

• f.toOrderHom = { toFun := ⇑f, monotone' := ⋯ }

@[simp]

theorem OrderEmbedding.toOrderHom_coe {X : Type u_6} {Y : Type u_7} [Preorder X] [Preorder Y] (f : X ↪o Y) : ⇑f.toOrderHom = ⇑f

def OrderEmbedding.ofIsEmpty {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [IsEmpty α] : α ↪o β

The trivial embedding from an empty preorder to another preorder

Equations

• OrderEmbedding.ofIsEmpty = { toFun := fun (a : α) => isEmptyElim a, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem OrderEmbedding.ofIsEmpty_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [IsEmpty α] (a : α) : ofIsEmpty a = isEmptyElim a

@[simp]

theorem OrderEmbedding.coe_ofIsEmpty {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [IsEmpty α] : ⇑ofIsEmpty = fun (a : α) => isEmptyElim a

theorem Disjoint.of_orderEmbedding {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (f : α ↪o β) [OrderBot α] [OrderBot β] {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} [PartialOrder α] [PartialOrder β] (f : α ↪o β) [OrderTop α] [OrderTop β] {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} [PartialOrder α] [PartialOrder β] (f : α ↪o β) [BoundedOrder α] [BoundedOrder β] {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.

def RelHom.toOrderHom {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] (f : (fun (x1 x2 : α) => x1 < x2) →r fun (x1 x2 : β) => x1 < x2) : α →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' := ⋯ }

@[simp]

theorem RelHom.toOrderHom_coe {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] (f : (fun (x1 x2 : α) => x1 < x2) →r fun (x1 x2 : β) => x1 < x2) : ⇑f.toOrderHom = ⇑f

theorem RelEmbedding.toOrderHom_injective {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] (f : (fun (x1 x2 : α) => x1 < x2) ↪r fun (x1 x2 : β) => x1 < x2) : 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 β) α β

@[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 g : α ≃o β} (h : ⇑f = ⇑g) : f = g

theorem OrderIso.ext_iff {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f g : α ≃o β} : 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 = RelIso.toRelEmbedding e

@[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 β) : Function.Bijective ⇑e

theorem OrderIso.injective {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) : Function.Injective ⇑e

theorem OrderIso.surjective {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) : Function.Surjective ⇑e

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

• OrderIso.refl α = RelIso.refl fun (x1 x2 : α) => x1 ≤ x2

@[simp]

theorem OrderIso.coe_refl {α : Type u_2} [LE α] : ⇑(refl α) = id

@[simp]

theorem OrderIso.refl_apply {α : Type u_2} [LE α] (x : α) : (refl α) x = x

@[simp]

theorem OrderIso.refl_toEquiv {α : Type u_2} [LE α] : (refl α).toEquiv = Equiv.refl α

def OrderIso.symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) : β ≃o α

Inverse of an order isomorphism.

Equations

• e.symm = RelIso.symm e

@[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 α] : (refl α).symm = refl α

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 symm

theorem OrderIso.symm_injective {α : Type u_2} {β : Type u_3} [LE α] [LE β] : Function.Injective 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

• e.trans e' = RelIso.trans e e'

@[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 β) : (refl α).trans e = e

@[simp]

theorem OrderIso.trans_refl {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) : e.trans (refl β) = 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 = refl α

@[simp]

theorem OrderIso.symm_trans_self {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) : e.symm.trans e = refl β

def OrderIso.arrowCongr {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (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' := ⋯ }

@[simp]

theorem OrderIso.arrowCongr_apply {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (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} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (f : α ≃o γ) (g : β ≃o δ) (p : γ →o δ) : (RelIso.symm (f.arrowCongr g)) p = (↑g.symm).comp (p.comp ↑f)

def OrderIso.conj {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (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)

@[simp]

theorem OrderIso.conj_apply {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (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} [Preorder α] [Preorder β] (f : α ≃o β) (a✝ : β →o β) : f.conj.symm a✝ = EquivLike.inv (f.arrowCongr f) a✝

def OrderIso.prodComm {α : Type u_2} {β : Type u_3} [LE α] [LE β] : α × β ≃o β × α

Prod.swap as an OrderIso.

Equations

• OrderIso.prodComm = { toEquiv := Equiv.prodComm α β, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.coe_prodComm {α : Type u_2} {β : Type u_3} [LE α] [LE β] : ⇑prodComm = Prod.swap

@[simp]

theorem OrderIso.prodComm_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] : prodComm.symm = prodComm

def OrderIso.dualDual (α : Type u_2) [LE α] : α ≃o αᵒᵈᵒᵈ

The order isomorphism between a type and its double dual.

Equations

• OrderIso.dualDual α = OrderIso.refl α

@[simp]

theorem OrderIso.coe_dualDual (α : Type u_2) [LE α] : ⇑(dualDual α) = ⇑OrderDual.toDual ∘ ⇑OrderDual.toDual

@[simp]

theorem OrderIso.coe_dualDual_symm (α : Type u_2) [LE α] : ⇑(dualDual α).symm = ⇑OrderDual.ofDual ∘ ⇑OrderDual.ofDual

@[simp]

theorem OrderIso.dualDual_apply {α : Type u_2} [LE α] (a : α) : (dualDual α) a = OrderDual.toDual (OrderDual.toDual a)

@[simp]

theorem OrderIso.dualDual_symm_apply {α : Type u_2} [LE α] (a : αᵒᵈᵒᵈ) : (dualDual α).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.GCongr.orderIso_apply_le_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x y : α} : x ≤ y → e x ≤ e y

Alias of the reverse direction of OrderIso.le_iff_le.

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} [Preorder α] [Preorder β] (e : α ≃o β) : Monotone ⇑e

theorem OrderIso.strictMono {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) : StrictMono ⇑e

@[simp]

theorem OrderIso.lt_iff_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {x y : α} : e x < e y ↔ x < y

theorem OrderIso.GCongr.orderIso_apply_lt_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {x y : α} : x < y → e x < e y

Alias of the reverse direction of OrderIso.lt_iff_lt.

theorem OrderIso.lt_symm_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {x : α} {y : β} : x < e.symm y ↔ e x < y

theorem OrderIso.symm_apply_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {x : α} {y : β} : e.symm y < x ↔ y < e x

def OrderIso.toRelIsoLT {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) : (fun (x1 x2 : α) => x1 < x2) ≃r fun (x1 x2 : β) => x1 < x2

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

Equations

• e.toRelIsoLT = { toEquiv := e.toEquiv, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.toRelIsoLT_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) (x : α) : e.toRelIsoLT x = e x

@[simp]

theorem OrderIso.toRelIsoLT_symm {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) : e.toRelIsoLT.symm = e.symm.toRelIsoLT

def OrderIso.ofRelIsoLT {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x1 x2 : α) => x1 < x2) ≃r fun (x1 x2 : β) => x1 < x2) : α ≃o β

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

Equations

• OrderIso.ofRelIsoLT e = { toEquiv := e.toEquiv, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.ofRelIsoLT_apply {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x1 x2 : α) => x1 < x2) ≃r fun (x1 x2 : β) => x1 < x2) (x : α) : (ofRelIsoLT e) x = e x

@[simp]

theorem OrderIso.ofRelIsoLT_symm {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x1 x2 : α) => x1 < x2) ≃r fun (x1 x2 : β) => x1 < x2) : (ofRelIsoLT e).symm = ofRelIsoLT e.symm

@[simp]

theorem OrderIso.ofRelIsoLT_toRelIsoLT {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : ofRelIsoLT e.toRelIsoLT = e

@[simp]

theorem OrderIso.toRelIsoLT_ofRelIsoLT {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x1 x2 : α) => x1 < x2) ≃r fun (x1 x2 : β) => x1 < x2) : (ofRelIsoLT e).toRelIsoLT = e

def OrderIso.ofCmpEqCmp {α : Type u_6} {β : Type u_7} [LinearOrder α] [LinearOrder β] (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

• OrderIso.ofCmpEqCmp f g h = { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

def OrderIso.ofHomInv {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {F : Type u_6} {G : Type u_7} [FunLike F α β] [OrderHomClass F α β] [FunLike G β α] [OrderHomClass 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' := ⋯ }

def OrderIso.funUnique (α : Type u_6) (β : Type u_7) [Unique α] [Preorder β] : (α → β) ≃o β

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

Equations

• OrderIso.funUnique α β = { toEquiv := Equiv.funUnique α β, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.funUnique_toEquiv (α : Type u_6) (β : Type u_7) [Unique α] [Preorder β] : (funUnique α β).toEquiv = Equiv.funUnique α β

@[simp]

theorem OrderIso.funUnique_apply (α : Type u_6) (β : Type u_7) [Unique α] [Preorder β] (f : (i : α) → (fun (a : α) => β) i) : (funUnique α β) f = f default

@[simp]

theorem OrderIso.funUnique_symm_apply {α : Type u_6} {β : Type u_7} [Unique α] [Preorder β] : ⇑(funUnique α β).symm = Function.const α

noncomputable def OrderIso.ofUnique (α : Type u_6) (β : Type u_7) [Unique α] [Unique β] [Preorder α] [Preorder β] : α ≃o β

The order isomorphism α ≃o β when α and β are preordered types containing unique elements.

Equations

• OrderIso.ofUnique α β = { toEquiv := Equiv.ofUnique α β, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.ofUnique_symm_apply (α : Type u_6) (β : Type u_7) [Unique α] [Unique β] [Preorder α] [Preorder β] (a✝ : β) : (RelIso.symm (ofUnique α β)) a✝ = default

@[simp]

theorem OrderIso.ofUnique_apply (α : Type u_6) (β : Type u_7) [Unique α] [Unique β] [Preorder α] [Preorder β] (a✝ : α) : (ofUnique α β) a✝ = default

def Equiv.toOrderIso {α : 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

• e.toOrderIso h₁ h₂ = { toEquiv := e, map_rel_iff' := ⋯ }

@[simp]

theorem Equiv.coe_toOrderIso {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃ β) (h₁ : Monotone ⇑e) (h₂ : Monotone ⇑e.symm) : ⇑(e.toOrderIso h₁ h₂) = ⇑e

@[simp]

theorem Equiv.toOrderIso_toEquiv {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (e : α ≃ β) (h₁ : Monotone ⇑e) (h₂ : Monotone ⇑e.symm) : (e.toOrderIso h₁ h₂).toEquiv = e

def StrictMono.orderIsoOfRightInverse {α : Type u_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (g : β → α) (hg : Function.RightInverse g f) : α ≃o β

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

Equations

• StrictMono.orderIsoOfRightInverse f h_mono g hg = { toFun := f, invFun := g, left_inv := ⋯, right_inv := hg, map_rel_iff' := ⋯ }

@[simp]

theorem StrictMono.orderIsoOfRightInverse_apply {α : Type u_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (g : β → α) (hg : Function.RightInverse g f) : ⇑(orderIsoOfRightInverse f h_mono g hg) = f

@[simp]

theorem StrictMono.orderIsoOfRightInverse_symm_apply {α : Type u_2} {β : Type u_3} [LinearOrder α] [Preorder β] (f : α → β) (h_mono : StrictMono f) (g : β → α) (hg : Function.RightInverse g f) : ⇑(RelIso.symm (orderIsoOfRightInverse f h_mono g hg)) = g

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

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

Equations

• f.dual = { toEquiv := f.toEquiv, map_rel_iff' := ⋯ }

theorem OrderIso.map_bot' {α : Type u_2} {β : Type u_3} [LE α] [PartialOrder β] (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 α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) : f ⊥ = ⊥

theorem OrderIso.map_top' {α : Type u_2} {β : Type u_3} [LE α] [PartialOrder β] (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 α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) : f ⊤ = ⊤

theorem OrderEmbedding.map_inf_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] (f : α ↪o β) (x y : α) : f (x ⊓ y) ≤ f x ⊓ f y

theorem OrderEmbedding.le_map_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] (f : α ↪o β) (x y : α) : f x ⊔ f y ≤ f (x ⊔ y)

theorem OrderIso.map_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] (f : α ≃o β) (x y : α) : f (x ⊓ y) = f x ⊓ f y

theorem OrderIso.map_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] (f : α ≃o β) (x y : α) : f (x ⊔ y) = f x ⊔ f y

theorem OrderIso.isMax_apply {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} : IsMax (f x) ↔ IsMax x

theorem OrderIso.isMin_apply {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} : IsMin (f x) ↔ IsMin x

theorem Disjoint.map_orderIso {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β] {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} [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β] {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

@[simp]

theorem disjoint_map_orderIso_iff {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β] {a b : α} (f : α ≃o β) : Disjoint (f a) (f b) ↔ Disjoint a b

@[simp]

theorem codisjoint_map_orderIso_iff {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β] {a b : α} (f : α ≃o β) : Codisjoint (f a) (f b) ↔ Codisjoint a b

theorem OrderIso.isCompl {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : α ≃o β) {x y : α} (h : IsCompl x y) : IsCompl (f x) (f y)

theorem OrderIso.isCompl_iff {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : α ≃o β) {x y : α} : IsCompl x y ↔ IsCompl (f x) (f y)

theorem OrderIso.complementedLattice {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [ComplementedLattice α] (f : α ≃o β) : ComplementedLattice β

theorem OrderIso.complementedLattice_iff {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : α ≃o β) : ComplementedLattice α ↔ ComplementedLattice β

@[instance 90]

instance OrderIsoClass.toOrderIsoClassOrderDual {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] : OrderIsoClass F αᵒᵈ βᵒᵈ

theorem denselyOrdered_iff_of_orderIsoClass {X : Type u_6} {Y : Type u_7} {F : Type u_8} [Preorder X] [Preorder Y] [EquivLike F X Y] [OrderIsoClass F X Y] (f : F) : DenselyOrdered X ↔ DenselyOrdered Y