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

@[inline, reducible]

abbrev OrderEmbedding (α : Type u_6) (β : Type u_7) [LE α] [LE β] : Type (max u_6 u_7)

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

Equations

• (α ↪o β) = ((fun (x x_1 : α) => x ≤ x_1) ↪r fun (x x_1 : β) => x ≤ x_1)

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

@[inline, reducible]

abbrev OrderIso (α : Type u_6) (β : Type u_7) [LE α] [LE β] : Type (max u_6 u_7)

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

Equations

• (α ≃o β) = ((fun (x x_1 : α) => x ≤ x_1) ≃r fun (x x_1 : β) => x ≤ x_1)

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

@[inline, reducible]

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 (x x_1 : α) => x ≤ x_1) fun (x x_1 : β) => x ≤ x_1

class OrderIsoClass (F : Type u_6) (α : Type u_7) (β : 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 = let __src := ↑f; { toEquiv := __src, map_rel_iff' := ⋯ }

instance instCoeTCOrderIso {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

• instCoeTCOrderIso = { coe := OrderIsoClass.toOrderIso }

instance OrderIsoClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] : OrderHomClass F α β

Equations

• ⋯ = ⋯

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

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

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

@[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.instFunLikeOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : FunLike (α →o β) α β

Equations

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

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

Equations

• ⋯ = ⋯

@[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 : α →o β) (g : α →o β) (h : ⇑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.

Equations

• ⋯ = ⋯

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

• OrderHom.copy f f' h = { toFun := f', monotone' := ⋯ }

@[simp]

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

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

@[simp]

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

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

The identity function as bundled monotone function.

Equations

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

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

Equations

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

instance OrderHom.instPreorderOrderHom {α : 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.instPreorderOrderHom = Preorder.lift OrderHom.toFun

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

Equations

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

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

@[simp]

theorem OrderHom.coe_le_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f : α →o β} {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 : α →o β} {g : α →o β} {x : α} {y : α} (h₁ : f ≤ g) (h₂ : x ≤ y) : f x ≤ g y

def OrderHom.curry {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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 : β) : ((OrderHom.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 OrderHom.curry) f) x = (f x.1) x.2

@[simp]

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

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

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

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

@[simp]

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

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 β)) => OrderHom.comp f.1 f.2, monotone' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (f : α →o β) (c : γ) : OrderHom.comp ((OrderHom.const β) c) f = (OrderHom.const α) c

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

def OrderHom.prodₘ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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 γ)) => OrderHom.prod f.1 f.2, monotone' := ⋯ }

@[simp]

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

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

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

Equations

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

@[simp]

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

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

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

Equations

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

@[simp]

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

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.snd_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (self : α × β) : OrderHom.snd self = self.2

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.fst_prod_snd {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : OrderHom.prod OrderHom.fst OrderHom.snd = OrderHom.id

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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.prodMap_coe {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (f : α →o β) (g : γ →o δ) : ∀ (a : α × γ), (OrderHom.prodMap f g) a = Prod.map (⇑f) (⇑g) a

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

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

@[simp]

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

def Pi.evalOrderHom {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → Preorder (π i)] (i : ι) : ((j : ι) → π j) →o π i

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

Equations

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

@[simp]

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

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.apply_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (x : α) : ⇑(OrderHom.apply x) = Function.eval x ∘ 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 = OrderHom.comp (Pi.evalOrderHom x) OrderHom.coeFnHom

@[simp]

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

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.piIso_apply {α : Type u_2} [Preorder α] {ι : Type u_6} {π : ι → Type u_7} [(i : ι) → Preorder (π i)] (f : α →o (i : ι) → π i) (i : ι) : OrderHom.piIso f i = OrderHom.comp (Pi.evalOrderHom i) 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 OrderHom.piIso) f = OrderHom.pi f

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

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

@[simp]

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

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 Subtype.orderEmbedding_apply_coe {α : Type u_2} [Preorder α] {p : α → Prop} {q : α → Prop} (h : ∀ (a : α), p a → q a) (x : { x : α // (fun (x : α) => p x) x }) : ↑((Subtype.orderEmbedding h) x) = ↑x

def Subtype.orderEmbedding {α : Type u_2} [Preorder α] {p : α → Prop} {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 = let __src := Subtype.impEmbedding (fun (x : α) => p x) (fun (x : α) => q x) h; { toEmbedding := __src, map_rel_iff' := ⋯ }

instance OrderHom.unique {α : Type u_2} [Preorder α] [Subsingleton α] : Unique (α →o α)

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

Equations

• OrderHom.unique = { toInhabited := { default := OrderHom.id }, uniq := ⋯ }

theorem OrderHom.orderHom_eq_id {α : Type u_2} [Preorder α] [Subsingleton α] (g : α →o α) : g = OrderHom.id

@[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_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

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_id {α : Type u_2} [Preorder α] : OrderHom.dual OrderHom.id = OrderHom.id

@[simp]

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

@[simp]

theorem OrderHom.symm_dual_id {α : Type u_2} [Preorder α] : OrderHom.dual.symm OrderHom.id = OrderHom.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 (OrderHom.comp g f) = OrderHom.comp (OrderHom.dual.symm g) (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' := ⋯ }

@[simp]

theorem OrderHom.withBotMap_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : ⇑(OrderHom.withBotMap f) = WithBot.map ⇑f

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

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

Equations

• OrderHom.withBotMap f = { toFun := WithBot.map ⇑f, monotone' := ⋯ }

@[simp]

theorem OrderHom.withTopMap_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : ⇑(OrderHom.withTopMap f) = WithTop.map ⇑f

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

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

Equations

• OrderHom.withTopMap f = { toFun := WithTop.map ⇑f, monotone' := ⋯ }

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

Embeddings of partial orders that preserve < also preserve ≤.

Equations

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

@[simp]

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

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

< is preserved by order embeddings of preorders.

Equations

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

@[simp]

theorem OrderEmbedding.ltEmbedding_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) (x : α) : (OrderEmbedding.ltEmbedding f) 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 (x x_1 : β) => x < x_1) (f a) → Acc (fun (x x_1 : α) => x < x_1) a

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

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

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

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

Equations

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

theorem OrderEmbedding.wellFoundedLT {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) [WellFoundedLT β] : 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 β] (f : α ↪o β) [WellFoundedGT β] : WellFoundedGT α

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

@[simp]

theorem OrderEmbedding.withBotMap_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) : ⇑(OrderEmbedding.withBotMap f) = WithBot.map ⇑f

def OrderEmbedding.withBotMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) : WithBot α ↪o WithBot β

A version of WithBot.map for order embeddings.

Equations

• OrderEmbedding.withBotMap f = let __src := Function.Embedding.optionMap f.toEmbedding; { toEmbedding := { toFun := WithBot.map ⇑f, inj' := ⋯ }, map_rel_iff' := ⋯ }

@[simp]

theorem OrderEmbedding.withTopMap_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) : ⇑(OrderEmbedding.withTopMap f) = WithTop.map ⇑f

def OrderEmbedding.withTopMap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ↪o β) : WithTop α ↪o WithTop β

A version of WithTop.map for order embeddings.

Equations

• OrderEmbedding.withTopMap f = let __src := OrderEmbedding.dual (OrderEmbedding.withBotMap (OrderEmbedding.dual f)); { toEmbedding := { toFun := WithTop.map ⇑f, inj' := ⋯ }, map_rel_iff' := ⋯ }

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) : ⇑(OrderEmbedding.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) : ⇑(OrderEmbedding.ofStrictMono f h) = f

@[simp]

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

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.toOrderHom_coe {X : Type u_6} {Y : Type u_7} [Preorder X] [Preorder Y] (f : X ↪o Y) : ⇑(OrderEmbedding.toOrderHom f) = ⇑f

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

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

@[simp]

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

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 = { toEmbedding := { toFun := fun (a : α) => isEmptyElim a, inj' := ⋯ }, map_rel_iff' := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

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

theorem RelEmbedding.toOrderHom_injective {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] (f : (fun (x x_1 : α) => x < x_1) ↪r fun (x x_1 : β) => x < x_1) : Function.Injective ⇑(RelHom.toOrderHom (RelEmbedding.toRelHom f))

instance OrderIso.instEquivLikeOrderIso {α : Type u_2} {β : Type u_3} [LE α] [LE β] : EquivLike (α ≃o β) α β

Equations

• OrderIso.instEquivLikeOrderIso = { coe := fun (f : α ≃o β) => f.toFun, inv := fun (f : α ≃o β) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance OrderIso.instOrderIsoClassOrderIsoInstEquivLikeOrderIso {α : Type u_2} {β : Type u_3} [LE α] [LE β] : OrderIsoClass (α ≃o β) α β

Equations

• ⋯ = ⋯

@[simp]

theorem OrderIso.toFun_eq_coe {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f : α ≃o β} : f.toFun = ⇑f

theorem OrderIso.ext {α : Type u_2} {β : Type u_3} [LE α] [LE β] {f : α ≃o β} {g : α ≃o β} (h : ⇑f = ⇑g) : f = g

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

Reinterpret an order isomorphism as an order embedding.

Equations

• OrderIso.toOrderEmbedding e = RelIso.toRelEmbedding e

@[simp]

theorem OrderIso.coe_toOrderEmbedding {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) : ⇑(OrderIso.toOrderEmbedding e) = ⇑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 (x x_1 : α) => x ≤ x_1

@[simp]

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

@[simp]

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

@[simp]

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

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

Inverse of an order isomorphism.

Equations

• OrderIso.symm e = RelIso.symm e

@[simp]

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

@[simp]

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

@[simp]

theorem OrderIso.symm_refl (α : Type u_6) [LE α] : OrderIso.symm (OrderIso.refl α) = OrderIso.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 = (OrderIso.symm e) y

theorem OrderIso.symm_apply_eq {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} : (OrderIso.symm e) y = x ↔ y = e x

@[simp]

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

theorem OrderIso.symm_bijective {α : Type u_2} {β : Type u_3} [LE α] [LE β] : Function.Bijective OrderIso.symm

theorem OrderIso.symm_injective {α : Type u_2} {β : Type u_3} [LE α] [LE β] : Function.Injective OrderIso.symm

@[simp]

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

• OrderIso.trans e 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 γ) : ⇑(OrderIso.trans e 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 : α) : (OrderIso.trans e e') x = e' (e x)

@[simp]

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

@[simp]

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

theorem OrderIso.symm_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [LE β] [LE γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) : OrderIso.symm (OrderIso.trans e₁ e₂) = OrderIso.trans (OrderIso.symm e₂) (OrderIso.symm e₁)

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 β] : ⇑OrderIso.prodComm = Prod.swap

@[simp]

theorem OrderIso.prodComm_symm {α : Type u_2} {β : Type u_3} [LE α] [LE β] : OrderIso.symm OrderIso.prodComm = OrderIso.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 α] : ⇑(OrderIso.dualDual α) = ⇑OrderDual.toDual ∘ ⇑OrderDual.toDual

@[simp]

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

@[simp]

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

@[simp]

theorem OrderIso.dualDual_symm_apply {α : Type u_2} [LE α] (a : αᵒᵈᵒᵈ) : (OrderIso.symm (OrderIso.dualDual α)) a = OrderDual.ofDual (OrderDual.ofDual a)

theorem OrderIso.le_iff_le {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : α} : e x ≤ e y ↔ x ≤ y

theorem OrderIso.le_symm_apply {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} : x ≤ (OrderIso.symm e) y ↔ e x ≤ y

theorem OrderIso.symm_apply_le {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) {x : α} {y : β} : (OrderIso.symm e) 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

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

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

Equations

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

@[simp]

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

@[simp]

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

def OrderIso.ofRelIsoLT {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1) : α ≃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 (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1) (x : α) : (OrderIso.ofRelIsoLT e) x = e x

@[simp]

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

@[simp]

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

@[simp]

theorem OrderIso.toRelIsoLT_ofRelIsoLT {α : Type u_6} {β : Type u_7} [PartialOrder α] [PartialOrder β] (e : (fun (x x_1 : α) => x < x_1) ≃r fun (x x_1 : β) => x < x_1) : OrderIso.toRelIsoLT (OrderIso.ofRelIsoLT e) = 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 = let_fun gf := ⋯; { toEquiv := { 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₁ : OrderHom.comp ↑f ↑g = OrderHom.id) (h₂ : OrderHom.comp ↑g ↑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₂ = { toEquiv := { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }, map_rel_iff' := ⋯ }

@[simp]

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

@[simp]

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

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_symm_apply {α : Type u_6} {β : Type u_7} [Unique α] [Preorder β] : ⇑(OrderIso.symm (OrderIso.funUnique α β)) = Function.const α

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

• Equiv.toOrderIso e 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) : ⇑(Equiv.toOrderIso e h₁ h₂) = ⇑e

@[simp]

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

@[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 (StrictMono.orderIsoOfRightInverse f h_mono g hg)) = g

@[simp]

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

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 = let __src := OrderEmbedding.ofStrictMono f h_mono; { toEquiv := { toFun := f, invFun := g, left_inv := ⋯, right_inv := hg }, map_rel_iff' := ⋯ }

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

• OrderIso.dual f = { 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 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

def WithBot.toDualTopEquiv {α : Type u_2} [LE α] : WithBot αᵒᵈ ≃o (WithTop α)ᵒᵈ

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

Equations

• WithBot.toDualTopEquiv = OrderIso.refl (WithBot αᵒᵈ)

@[simp]

theorem WithBot.toDualTopEquiv_coe {α : Type u_2} [LE α] (a : α) : WithBot.toDualTopEquiv ↑(OrderDual.toDual a) = OrderDual.toDual ↑a

@[simp]

theorem WithBot.toDualTopEquiv_symm_coe {α : Type u_2} [LE α] (a : α) : (OrderIso.symm WithBot.toDualTopEquiv) (OrderDual.toDual ↑a) = ↑(OrderDual.toDual a)

@[simp]

theorem WithBot.toDualTopEquiv_bot {α : Type u_2} [LE α] : WithBot.toDualTopEquiv ⊥ = ⊥

@[simp]

theorem WithBot.toDualTopEquiv_symm_bot {α : Type u_2} [LE α] : (OrderIso.symm WithBot.toDualTopEquiv) ⊥ = ⊥

theorem WithBot.coe_toDualTopEquiv_eq {α : Type u_2} [LE α] : ⇑WithBot.toDualTopEquiv = ⇑OrderDual.toDual ∘ ⇑WithBot.ofDual

def WithTop.toDualBotEquiv {α : Type u_2} [LE α] : WithTop αᵒᵈ ≃o (WithBot α)ᵒᵈ

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

Equations

• WithTop.toDualBotEquiv = OrderIso.refl (WithTop αᵒᵈ)

@[simp]

theorem WithTop.toDualBotEquiv_coe {α : Type u_2} [LE α] (a : α) : WithTop.toDualBotEquiv ↑(OrderDual.toDual a) = OrderDual.toDual ↑a

@[simp]

theorem WithTop.toDualBotEquiv_symm_coe {α : Type u_2} [LE α] (a : α) : (OrderIso.symm WithTop.toDualBotEquiv) (OrderDual.toDual ↑a) = ↑(OrderDual.toDual a)

@[simp]

theorem WithTop.toDualBotEquiv_top {α : Type u_2} [LE α] : WithTop.toDualBotEquiv ⊤ = ⊤

@[simp]

theorem WithTop.toDualBotEquiv_symm_top {α : Type u_2} [LE α] : (OrderIso.symm WithTop.toDualBotEquiv) ⊤ = ⊤

theorem WithTop.coe_toDualBotEquiv {α : Type u_2} [LE α] : ⇑WithTop.toDualBotEquiv = ⇑OrderDual.toDual ∘ ⇑WithTop.ofDual

@[simp]

theorem OrderIso.withTopCongr_apply {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : ∀ (a : Option α), (OrderIso.withTopCongr e) a = Option.map (⇑e) a

def OrderIso.withTopCongr {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : WithTop α ≃o WithTop β

A version of Equiv.optionCongr for WithTop.

Equations

• OrderIso.withTopCongr e = let __src := OrderEmbedding.withTopMap (OrderIso.toOrderEmbedding e); { toEquiv := Equiv.optionCongr e.toEquiv, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.withTopCongr_refl {α : Type u_2} [PartialOrder α] : OrderIso.withTopCongr (OrderIso.refl α) = OrderIso.refl (WithTop α)

@[simp]

theorem OrderIso.withTopCongr_symm {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : OrderIso.symm (OrderIso.withTopCongr e) = OrderIso.withTopCongr (OrderIso.symm e)

@[simp]

theorem OrderIso.withTopCongr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [PartialOrder α] [PartialOrder β] [PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) : OrderIso.trans (OrderIso.withTopCongr e₁) (OrderIso.withTopCongr e₂) = OrderIso.withTopCongr (OrderIso.trans e₁ e₂)

@[simp]

theorem OrderIso.withBotCongr_apply {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : ∀ (a : Option α), (OrderIso.withBotCongr e) a = Option.map (⇑e) a

def OrderIso.withBotCongr {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : WithBot α ≃o WithBot β

A version of Equiv.optionCongr for WithBot.

Equations

• OrderIso.withBotCongr e = let __src := OrderEmbedding.withBotMap (OrderIso.toOrderEmbedding e); { toEquiv := Equiv.optionCongr e.toEquiv, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.withBotCongr_refl {α : Type u_2} [PartialOrder α] : OrderIso.withBotCongr (OrderIso.refl α) = OrderIso.refl (WithBot α)

@[simp]

theorem OrderIso.withBotCongr_symm {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : OrderIso.symm (OrderIso.withBotCongr e) = OrderIso.withBotCongr (OrderIso.symm e)

@[simp]

theorem OrderIso.withBotCongr_trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [PartialOrder α] [PartialOrder β] [PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) : OrderIso.trans (OrderIso.withBotCongr e₁) (OrderIso.withBotCongr e₂) = OrderIso.withBotCongr (OrderIso.trans e₁ e₂)

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 β] (f : α ≃o β) [ComplementedLattice α] : ComplementedLattice β

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