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)

• toFun : α → β

  The underlying function of an OrderHom.

• monotone' : Monotone s.toFun

  The underlying function of an OrderHom is monotone.

Bundled monotone (aka, increasing) function

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 β] : Type (max (max u_6 u_7) u_8)

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) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [LE α] [LE β] extends EquivLike : Type (max (max u_6 u_7) u_8)

• coe : F → α → β
• inv : F → β → α
• left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
• right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
• coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
• map_le_map_iff : ∀ (f : F) {a b : α}, ↑f a ≤ ↑f b ↔ a ≤ b

  An order isomorphism respects ≤.

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

You should extend this class when you extend OrderIso.

def OrderIsoClass.toOrderIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [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

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

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

Equations

• OrderIsoClass.toOrderHomClass = let src := EquivLike.toEmbeddingLike; RelHomClass.mk (_ : ∀ (f : F) (x x_1 : α), x ≤ x_1 → ↑f x ≤ ↑f x_1)

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

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

def OrderHomClass.toOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [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' := (_ : Monotone ↑f) }

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

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

Equations

• OrderHom.instOrderHomClassOrderHomToLEToLE = RelHomClass.mk (_ : ∀ (f : α →o β) (x x_1 : α), x ≤ x_1 → OrderHom.toFun f x ≤ OrderHom.toFun f x_1)

instance OrderHom.instCoeFunOrderHomForAll {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : CoeFun (α →o β) fun x => α → β

Helper instance for when there's too many metavariables to apply the coercion via FunLike directly.

Equations

• OrderHom.instCoeFunOrderHomForAll = { coe := FunLike.coe }

@[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} [OrderHomClass F α β] (f : F) : ↑↑f = ↑f

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

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

Equations

• @OrderHom.canLift = @OrderHom.canLift.proof_1

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' := (_ : Monotone f') }

@[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' := (_ : Monotone id) }

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 (_ : ∀ (f g : α →o β), ↑f = ↑g → f = g)

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.fst) x.snd

@[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' := (_ : Monotone (↑g ∘ ↑f)) }

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

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

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

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

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

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

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 : α), ↑(↑(↑OrderHom.prodₘ x) a) x = (↑x x, ↑a x)

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

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

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

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

Prod.fst as an OrderHom.

Equations

• OrderHom.fst = { toFun := Prod.fst, monotone' := (_ : ∀ (x x_1 : α × β), x ≤ x_1 → x.fst ≤ x_1.fst) }

@[simp]

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

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

Prod.snd as an OrderHom.

Equations

• OrderHom.snd = { toFun := Prod.snd, monotone' := (_ : ∀ (x x_1 : α × β), x ≤ x_1 → x.snd ≤ x_1.snd) }

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

@[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.fst f.snd

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

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

@[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' := (_ : Monotone (Function.eval i)) }

@[simp]

theorem OrderHom.coeFnHom_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : ↑OrderHom.coeFnHom = fun f => ↑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 => ↑f, monotone' := (_ : ∀ (x x_1 : α →o β), x ≤ x_1 → x ≤ x_1) }

@[simp]

theorem OrderHom.apply_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (x : α) : ↑(OrderHom.apply x) = (fun f => f x) ∘ fun f => ↑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' := (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (i : ι), ↑(f i) x ≤ ↑(f i) x_1) }

@[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' := (_ : ∀ (x x_1 : Subtype p), x ≤ x_1 → x ≤ x_1) }

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

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

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 := (_ : ∀ (x : α →o α), x = default) }

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

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

@[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' := (_ : Monotone (WithBot.map ↑f)) }

@[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' := (_ : Monotone (WithTop.map ↑f)) }

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' := (_ : ∀ {a b : α}, ↑f a ≤ ↑f b ↔ a ≤ b) }

@[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' := (_ : ∀ {a b : α}, ↑f a < ↑f b ↔ a < b) }

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

@[simp]

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' := (_ : ∀ {a b : αᵒᵈ}, ↑f b ≤ ↑f a ↔ b ≤ a) }

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

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

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

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

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 (_ : ∀ (x x_1 : α), f x ≤ f x_1 ↔ x ≤ x_1)

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

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

@[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' := (_ : Monotone ↑f) }

@[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' := (_ : Monotone ↑f) }

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.instOrderIsoClassOrderIso {α : Type u_2} {β : Type u_3} [LE α] [LE β] : OrderIsoClass (α ≃o β) α β

Equations

• OrderIso.instOrderIsoClassOrderIso = OrderIsoClass.mk (_ : ∀ (f : α ≃o β) (x x_1 : α), ↑f.toEquiv x ≤ ↑f.toEquiv x_1 ↔ x ≤ x_1)

@[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_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' := (_ : ∀ {a b : α × β}, Prod.swap a ≤ Prod.swap b ↔ a ≤ b) }

@[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' := (_ : ∀ {a b : α}, ↑e a < ↑e b ↔ a < b) }

@[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' := (_ : ∀ (a a_1 : α), ↑e a ≤ ↑e a_1 ↔ a ≤ a_1) }

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

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

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

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

@[simp]

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

@[simp]

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

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' := (_ : ∀ (a a_1 : α → β), a default ≤ a_1 default ↔ a ≤ a_1) }

@[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' := (_ : ∀ {a b : α}, ↑e a ≤ ↑e b ↔ a ≤ b) }

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

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

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' := (_ : ∀ {a b : αᵒᵈ}, ↑f b ≤ ↑f a ↔ b ≤ a) }

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

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

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

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

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