Mathlib.Order.Hom.Basic

OrderHom structure

(α β : Type*) [Preorder α] [Preorder β]

Full source

/-- Bundled monotone (aka, increasing) function -/
structure OrderHom (α β : Type*) [Preorder α] [Preorder β] where
  /-- The underlying function of an `OrderHom`. -/
  toFun : α → β
  /-- The underlying function of an `OrderHom` is monotone. -/
  monotone' : Monotone toFun

Order Homomorphism

Informal description

The structure representing a bundled monotone (increasing) function between preorders. An order homomorphism `f : α →o β` is a function `f : α → β` together with a proof that it preserves the order relation, i.e., for any `x, y ∈ α`, if `x ≤ y` then `f x ≤ f y`.

term_→o_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for an `OrderHom`. -/
infixr:25 " →o " => OrderHom

Order homomorphism notation

Informal description

The notation `→o` denotes an order homomorphism between two preorders. Specifically, for preorders `α` and `β`, the notation `α →o β` represents the type of order homomorphisms from `α` to `β`, which are functions `f : α → β` that preserve the order relation (i.e., if `x ≤ y` in `α`, then `f x ≤ f y` in `β`).

OrderEmbedding abbrev

(α β : Type*) [LE α] [LE β]

Full source

/-- An order embedding is an embedding `f : α ↪ β` such that `a ≤ b ↔ (f a) ≤ (f b)`.
This definition is an abbreviation of `RelEmbedding (≤) (≤)`. -/
abbrev OrderEmbedding (α β : Type*) [LE α] [LE β] :=
  @RelEmbedding α β (· ≤ ·) (· ≤ ·)

Order Embedding Between Preordered Types

Informal description

An order embedding between two preordered types $\alpha$ and $\beta$ is an injective function $f : \alpha \hookrightarrow \beta$ that preserves and reflects the order relation, meaning for any $x, y \in \alpha$, we have $x \leq y$ if and only if $f(x) \leq f(y)$ in $\beta$.

term_↪o_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for an `OrderEmbedding`. -/
infixl:25 " ↪o " => OrderEmbedding

Order Embedding Notation

Informal description

The notation `α ↪o β` represents an order embedding between types `α` and `β` with preorder structures. An order embedding is an injective function that preserves and reflects the order relation, meaning for any elements `x, y` in `α`, `x ≤ y` if and only if `f x ≤ f y` in `β`.

OrderIso abbrev

(α β : Type*) [LE α] [LE β]

Full source

/-- An order isomorphism is an equivalence such that `a ≤ b ↔ (f a) ≤ (f b)`.
This definition is an abbreviation of `RelIso (≤) (≤)`. -/
abbrev OrderIso (α β : Type*) [LE α] [LE β] :=
  @RelIso α β (· ≤ ·) (· ≤ ·)

Order-Preserving Isomorphism ($\alpha \simeq_o \beta$)

Informal description

An *order isomorphism* between two preordered types $\alpha$ and $\beta$ is a bijective function $f : \alpha \to \beta$ that preserves the order relation in both directions, i.e., for any $x, y \in \alpha$, we have $x \leq y$ if and only if $f(x) \leq f(y)$.

term_≃o_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for an `OrderIso`. -/
infixl:25 " ≃o " => OrderIso

Order isomorphism notation

Informal description

The notation `≃o` is used to denote an order isomorphism between two types `α` and `β` equipped with a preorder relation `≤`. An order isomorphism is a bijective function `f : α → β` that preserves the order relation in both directions, i.e., for any `x, y ∈ α`, we have `x ≤ y` if and only if `f(x) ≤ f(y)`.

OrderHomClass abbrev

(F : Type*) (α β : outParam Type*) [LE α] [LE β] [FunLike F α β]

Full source

/-- `OrderHomClass F α b` asserts that `F` is a type of `≤`-preserving morphisms. -/
abbrev OrderHomClass (F : Type*) (α β : outParam Type*) [LE α] [LE β] [FunLike F α β] :=
  RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop)

Class of Order-Preserving Morphisms

Informal description

The class `OrderHomClass F α β` asserts that `F` is a type of order-preserving morphisms between types `α$ and $\beta$ equipped with partial order relations $\leq$. Specifically, for any $f \in F$ and any $x, y \in \alpha$, if $x \leq y$ then $f(x) \leq f(y)$.

OrderIsoClass structure

(F : Type*) (α β : outParam Type*) [LE α] [LE β] [EquivLike F α β]

Full source

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

You should extend this class when you extend `OrderIso`. -/
class OrderIsoClass (F : Type*) (α β : outParam Type*) [LE α] [LE β] [EquivLike F α β] :
    Prop where
  /-- An order isomorphism respects `≤`. -/
  map_le_map_iff (f : F) {a b : α} : f a ≤ f b ↔ a ≤ b

Order Isomorphism Class

Informal description

The class `OrderIsoClass F α β` indicates that `F` is a type of order isomorphisms between types `α` and `β` equipped with a partial order relation `≤`. An order isomorphism is a bijective function that preserves and reflects the order relation, meaning that for any elements `x` and `y` in `α`, `x ≤ y` if and only if `f x ≤ f y` for any `f : F`.

OrderIsoClass.toOrderIso definition

[LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) : α ≃o β

Full source

/-- 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 β`. -/
@[coe]
def OrderIsoClass.toOrderIso [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] (f : F) :
    α ≃o β :=
  { EquivLike.toEquiv f with map_rel_iff' := map_le_map_iff f }

Conversion from order isomorphism class to explicit order isomorphism

Informal description

Given a type `F` that satisfies `OrderIsoClass F α β` (i.e., elements of `F` are order-preserving bijections between partially ordered types `α` and `β`), the function `OrderIsoClass.toOrderIso` converts an element `f : F` into an explicit order isomorphism `α ≃o β`. This isomorphism consists of: - A bijection `f : α → β` that preserves the order relation in both directions (i.e., for any `x, y ∈ α`, `x ≤ y` if and only if `f(x) ≤ f(y)`).

instCoeTCOrderIsoOfOrderIsoClass instance

[LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] : CoeTC F (α ≃o β)

Full source

/-- Any type satisfying `OrderIsoClass` can be cast into `OrderIso` via
`OrderIsoClass.toOrderIso`. -/
instance [LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] : CoeTC F (α ≃o β) :=
  ⟨OrderIsoClass.toOrderIso⟩

Coercion from Order Isomorphism Class to Order Isomorphism

Informal description

For any types $\alpha$ and $\beta$ equipped with partial orders $\leq$, and any type $F$ that satisfies `OrderIsoClass F α β`, there is a canonical coercion from $F$ to the type of order isomorphisms $\alpha \simeq_o \beta$. This means that any element $f : F$ can be treated as an explicit order isomorphism between $\alpha$ and $\beta$, preserving the order relation in both directions.

OrderIsoClass.toOrderHomClass instance

[LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] : OrderHomClass F α β

Full source

instance (priority := 100) OrderIsoClass.toOrderHomClass [LE α] [LE β]
    [EquivLike F α β] [OrderIsoClass F α β] : OrderHomClass F α β :=
  { EquivLike.toEmbeddingLike (E := F) with
    map_rel := fun f _ _ => (map_le_map_iff f).2 }

Order Isomorphisms are Order Homomorphisms

Informal description

For any types $\alpha$ and $\beta$ equipped with partial orders $\leq$, every order isomorphism class $F$ between $\alpha$ and $\beta$ is also an order homomorphism class. That is, every order isomorphism (a bijective order-preserving map) is automatically an order homomorphism (a monotone map).

OrderHomClass.monotone theorem

(f : F) : Monotone f

Full source

protected theorem monotone (f : F) : Monotone f := fun _ _ => map_rel f

Monotonicity of Order-Preserving Morphisms

Informal description

For any order-preserving morphism $f \colon F$ between partially ordered types $\alpha$ and $\beta$, the function $f$ is monotone. That is, for any $x, y \in \alpha$, if $x \leq y$, then $f(x) \leq f(y)$.

OrderHomClass.mono theorem

(f : F) : Monotone f

Full source

protected theorem mono (f : F) : Monotone f := fun _ _ => map_rel f

Monotonicity of Order-Preserving Morphisms

Informal description

For any order-preserving morphism $f \colon F$ between partially ordered types $\alpha$ and $\beta$, the function $f$ is monotone. That is, for any $x, y \in \alpha$, if $x \leq y$, then $f(x) \leq f(y)$.

OrderHomClass.GCongr.mono theorem

(f : F) {a b : α} (hab : a ≤ b) : f a ≤ f b

Full source

@[gcongr] protected lemma GCongr.mono (f : F) {a b : α} (hab : a ≤ b) : f a ≤ f b :=
  OrderHomClass.mono f hab

Monotonicity of Order-Preserving Morphisms under Generalized Congruence

Informal description

For any order-preserving morphism $f \colon F$ between partially ordered types $\alpha$ and $\beta$, and for any elements $a, b \in \alpha$ such that $a \leq b$, it follows that $f(a) \leq f(b)$.

OrderHomClass.toOrderHom definition

(f : F) : α →o β

Full source

/-- 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 β`. -/
@[coe]
def toOrderHom (f : F) : α →o β where
  toFun := f
  monotone' := OrderHomClass.monotone f

Conversion from OrderHomClass to OrderHom

Informal description

Given a type `F` that satisfies `OrderHomClass F α β`, this function converts an element `f : F` into an order homomorphism `α →o β`. The resulting homomorphism has the same underlying function as `f` and is equipped with a proof that it is monotone (i.e., preserves the order relation).

OrderHomClass.instCoeTCOrderHom instance

: CoeTC F (α →o β)

Full source

/-- Any type satisfying `OrderHomClass` can be cast into `OrderHom` via
`OrderHomClass.toOrderHom`. -/
instance : CoeTC F (α →o β) :=
  ⟨toOrderHom⟩

Coercion from OrderHomClass to Order Homomorphisms

Informal description

For any type $F$ that satisfies `OrderHomClass F α β`, there is a canonical coercion from $F$ to the type of order homomorphisms $\alpha \to_o \beta$. This means any element $f : F$ can be treated as an order-preserving function between the preorders $\alpha$ and $\beta$.

map_inv_le_iff theorem

(f : F) {a : α} {b : β} : EquivLike.inv f b ≤ a ↔ b ≤ f a

Full source

@[simp]
theorem map_inv_le_iff (f : F) {a : α} {b : β} : EquivLike.invEquivLike.inv f b ≤ a ↔ b ≤ f a := by
  convert (map_le_map_iff f).symm
  exact (EquivLike.right_inv f _).symm

Order isomorphism preserves order via inverse comparison: $f^{-1}(b) \leq a \leftrightarrow b \leq f(a)$

Informal description

For any order isomorphism $f \colon \alpha \to \beta$ and elements $a \in \alpha$, $b \in \beta$, the inequality $f^{-1}(b) \leq a$ holds if and only if $b \leq f(a)$.

map_inv_le_map_inv_iff theorem

(f : F) {a b : β} : EquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a

Full source

theorem map_inv_le_map_inv_iff (f : F) {a b : β} :
    EquivLike.invEquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a := by
  simp

Order isomorphism preserves order via inverse comparison: $f^{-1}(b) \leq f^{-1}(a) \leftrightarrow b \leq a$

Informal description

For any order isomorphism $f \colon \alpha \to \beta$ and elements $a, b \in \beta$, the inequality $f^{-1}(b) \leq f^{-1}(a)$ holds if and only if $b \leq a$.

le_map_inv_iff theorem

(f : F) {a : α} {b : β} : a ≤ EquivLike.inv f b ↔ f a ≤ b

Full source

@[simp]
theorem le_map_inv_iff (f : F) {a : α} {b : β} : a ≤ EquivLike.inv f b ↔ f a ≤ b := by
  convert (map_le_map_iff f).symm
  exact (EquivLike.right_inv _ _).symm

Order isomorphism preserves order via inverse

Informal description

For any order isomorphism $f \colon \alpha \to \beta$ and elements $a \in \alpha$, $b \in \beta$, we have $a \leq f^{-1}(b)$ if and only if $f(a) \leq b$.

map_lt_map_iff theorem

(f : F) {a b : α} : f a < f b ↔ a < b

Full source

theorem map_lt_map_iff (f : F) {a b : α} : f a < f b ↔ a < b :=
  lt_iff_lt_of_le_iff_le' (map_le_map_iff f) (map_le_map_iff f)

Order isomorphism preserves strict order

Informal description

For any order isomorphism $f \colon \alpha \to \beta$ and elements $a, b \in \alpha$, we have $f(a) < f(b)$ if and only if $a < b$.

map_inv_lt_iff theorem

(f : F) {a : α} {b : β} : EquivLike.inv f b < a ↔ b < f a

Full source

@[simp]
theorem map_inv_lt_iff (f : F) {a : α} {b : β} : EquivLike.invEquivLike.inv f b < a ↔ b < f a := by
  rw [← map_lt_map_iff f]
  simp only [EquivLike.apply_inv_apply]

Order isomorphism preserves strict order under inverse mapping: $f^{-1}(b) < a \leftrightarrow b < f(a)$

Informal description

For any order isomorphism $f \colon \alpha \to \beta$ between partially ordered sets, and for any elements $a \in \alpha$ and $b \in \beta$, the inequality $f^{-1}(b) < a$ holds if and only if $b < f(a)$.

map_inv_lt_map_inv_iff theorem

(f : F) {a b : β} : EquivLike.inv f b < EquivLike.inv f a ↔ b < a

Full source

theorem map_inv_lt_map_inv_iff (f : F) {a b : β} :
    EquivLike.invEquivLike.inv f b < EquivLike.inv f a ↔ b < a := by
  simp

Order isomorphism preserves strict order under inverse mapping: $f^{-1}(b) < f^{-1}(a) \leftrightarrow b < a$

Informal description

For any order isomorphism $f \colon \alpha \to \beta$ and elements $a, b \in \beta$, the inequality $f^{-1}(b) < f^{-1}(a)$ holds if and only if $b < a$.

lt_map_inv_iff theorem

(f : F) {a : α} {b : β} : a < EquivLike.inv f b ↔ f a < b

Full source

@[simp]
theorem lt_map_inv_iff (f : F) {a : α} {b : β} : a < EquivLike.inv f b ↔ f a < b := by
  rw [← map_lt_map_iff f]
  simp only [EquivLike.apply_inv_apply]

Order isomorphism preserves strict order under inverse mapping: $a < f^{-1}(b) \leftrightarrow f(a) < b$

Informal description

For any order isomorphism $f \colon \alpha \to \beta$ between partially ordered types $\alpha$ and $\beta$, and for any elements $a \in \alpha$ and $b \in \beta$, we have $a < f^{-1}(b)$ if and only if $f(a) < b$.

OrderHom.instFunLike instance

: FunLike (α →o β) α β

Full source

instance : FunLike (α →o β) α β where
  coe := toFun
  coe_injective' f g h := by cases f; cases g; congr

Function-Like Structure on Order Homomorphisms

Informal description

For any two preorders $\alpha$ and $\beta$, the type of order homomorphisms $\alpha \to_o \beta$ can be treated as a function-like type, where each order homomorphism can be coerced to a function from $\alpha$ to $\beta$.

OrderHom.instOrderHomClass instance

: OrderHomClass (α →o β) α β

Full source

instance : OrderHomClass (α →o β) α β where
  map_rel f _ _ h := f.monotone' h

Order Homomorphisms as Order-Preserving Maps

Informal description

For any two preorders $\alpha$ and $\beta$, the type of order homomorphisms $\alpha \to_o \beta$ forms an instance of `OrderHomClass`, meaning that every order homomorphism preserves the order relation: if $x \leq y$ in $\alpha$, then $f(x) \leq f(y)$ in $\beta$ for any $f \in \alpha \to_o \beta$.

OrderHom.coe_mk theorem

(f : α → β) (hf : Monotone f) : ⇑(mk f hf) = f

Full source

@[simp] theorem coe_mk (f : α → β) (hf : Monotone f) : ⇑(mk f hf) = f := rfl

Coefficient Extraction from Order Homomorphism Construction

Informal description

For any function $f : \alpha \to \beta$ between preorders and a proof $hf$ that $f$ is monotone, the underlying function of the bundled order homomorphism $\text{mk}(f, hf) : \alpha \to_o \beta$ is equal to $f$.

OrderHom.monotone theorem

(f : α →o β) : Monotone f

Full source

protected theorem monotone (f : α →o β) : Monotone f :=
  f.monotone'

Monotonicity of Order Homomorphisms

Informal description

For any order homomorphism $f \colon \alpha \to_o \beta$ between preorders, the function $f$ is monotone, meaning that for all $x, y \in \alpha$, if $x \leq y$ then $f(x) \leq f(y)$.

OrderHom.mono theorem

(f : α →o β) : Monotone f

Full source

protected theorem mono (f : α →o β) : Monotone f :=
  f.monotone

Monotonicity of Order Homomorphisms

Informal description

For any order homomorphism $f \colon \alpha \to_o \beta$ between preorders, the function $f$ is monotone, i.e., for all $x, y \in \alpha$, if $x \leq y$ then $f(x) \leq f(y)$.

OrderHom.Simps.coe definition

(f : α →o β) : α → β

Full source

/-- See Note [custom simps projection]. We give this manually so that we use `toFun` as the
projection directly instead. -/
def Simps.coe (f : α →o β) : α → β := f

Coercion from order homomorphism to function

Informal description

The coercion function that maps an order homomorphism `f : α →o β` to its underlying function `f : α → β`.

OrderHom.toFun_eq_coe theorem

(f : α →o β) : f.toFun = f

Full source

@[simp] theorem toFun_eq_coe (f : α →o β) : f.toFun = f := rfl

Equality of Underlying Function and Coercion for Order Homomorphisms

Informal description

For any order homomorphism $f \colon \alpha \to_o \beta$, the underlying function $f.\text{toFun}$ is equal to the coercion of $f$ to a function, i.e., $f.\text{toFun} = f$.

OrderHom.ext theorem

(f g : α →o β) (h : (f : α → β) = g) : f = g

Full source

@[ext]
theorem ext (f g : α →o β) (h : (f : α → β) = g) : f = g :=
  DFunLike.coe_injective h

Extensionality of Order Homomorphisms

Informal description

For any two order homomorphisms $f, g \colon \alpha \to_o \beta$ between preorders, if the underlying functions $f$ and $g$ are equal (i.e., $f(x) = g(x)$ for all $x \in \alpha$), then $f = g$ as order homomorphisms.

OrderHom.coe_eq theorem

(f : α →o β) : OrderHomClass.toOrderHom f = f

Full source

@[simp] theorem coe_eq (f : α →o β) : OrderHomClass.toOrderHom f = f := rfl

Identity of Order Homomorphism Conversion

Informal description

For any order homomorphism $f \colon \alpha \to_o \beta$ between preorders, the conversion of $f$ to an order homomorphism via `OrderHomClass.toOrderHom` yields $f$ itself, i.e., $\text{OrderHomClass.toOrderHom}(f) = f$.

OrderHomClass.coe_coe theorem

{F} [FunLike F α β] [OrderHomClass F α β] (f : F) : ⇑(f : α →o β) = f

Full source

@[simp] theorem _root_.OrderHomClass.coe_coe {F} [FunLike F α β] [OrderHomClass F α β] (f : F) :
    ⇑(f : α →o β) = f :=
  rfl

Equality of Underlying Functions in Order Homomorphisms

Informal description

For any type `F` with a function-like structure `FunLike F α β` and an order-preserving structure `OrderHomClass F α β`, and for any element `f : F`, the underlying function of the order homomorphism `f : α →o β` is equal to `f` itself.

OrderHom.canLift instance

: CanLift (α → β) (α →o β) (↑) Monotone

Full source

/-- One can lift an unbundled monotone function to a bundled one. -/
protected instance canLift : CanLift (α → β) (α →o β) (↑) Monotone where
  prf f h := ⟨⟨f, h⟩, rfl⟩

Lifting Monotone Functions to Order Homomorphisms

Informal description

For any preorders $\alpha$ and $\beta$, there is a canonical way to lift a monotone function $f : \alpha \to \beta$ to an order homomorphism $f : \alpha \to_o \beta$.

OrderHom.copy definition

(f : α →o β) (f' : α → β) (h : f' = f) : α →o β

Full source

/-- Copy of an `OrderHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : α →o β) (f' : α → β) (h : f' = f) : α →o β :=
  ⟨f', h.symm.subst f.monotone'⟩

Copy of an order homomorphism with a new function

Informal description

Given an order homomorphism $f \colon \alpha \to_o \beta$ and a function $f' \colon \alpha \to \beta$ such that $f' = f$, the function `OrderHom.copy` constructs a new order homomorphism with the underlying function $f'$ and the same monotonicity proof as $f$. This is useful for fixing definitional equalities.

OrderHom.coe_copy theorem

(f : α →o β) (f' : α → β) (h : f' = f) : (f.copy f' h) = f'

Full source

@[simp]
theorem coe_copy (f : α →o β) (f' : α → β) (h : f' = f) : (f.copy f' h) = f' :=
  rfl

Coefficient of Copied Order Homomorphism Equals Given Function

Informal description

Given an order homomorphism $f \colon \alpha \to_o \beta$ and a function $f' \colon \alpha \to \beta$ such that $f' = f$, the underlying function of the copied order homomorphism $f.\text{copy}\, f'\, h$ is equal to $f'$.

OrderHom.copy_eq theorem

(f : α →o β) (f' : α → β) (h : f' = f) : f.copy f' h = f

Full source

theorem copy_eq (f : α →o β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

Equality of Copied Order Homomorphism with Original

Informal description

Given an order homomorphism $f \colon \alpha \to_o \beta$ and a function $f' \colon \alpha \to \beta$ such that $f' = f$, the copied order homomorphism $f.\text{copy}\, f'\, h$ is equal to $f$.

OrderHom.id definition

: α →o α

Full source

/-- The identity function as bundled monotone function. -/
@[simps -fullyApplied]
def id : α →o α :=
  ⟨_root_.id, monotone_id⟩

Identity order homomorphism

Informal description

The identity function on a preorder $\alpha$, viewed as a bundled monotone function from $\alpha$ to itself. That is, the function $\operatorname{id} : \alpha \to \alpha$ together with the proof that it is monotone (i.e., $x \leq y$ implies $\operatorname{id}(x) \leq \operatorname{id}(y)$ for all $x, y \in \alpha$).

OrderHom.instInhabited instance

: Inhabited (α →o α)

Full source

instance : Inhabited (α →o α) :=
  ⟨id⟩

Inhabitedness of Order Homomorphisms

Informal description

For any preorder $\alpha$, the type of order homomorphisms from $\alpha$ to itself is inhabited, with the identity function serving as a canonical element.

OrderHom.instPreorder instance

: Preorder (α →o β)

Full source

/-- The preorder structure of `α →o β` is pointwise inequality: `f ≤ g ↔ ∀ a, f a ≤ g a`. -/
instance : Preorder (α →o β) :=
  @Preorder.lift (α →o β) (α → β) _ toFun

Pointwise Preorder on Order Homomorphisms

Informal description

The type of order homomorphisms $\alpha \to_o \beta$ (monotone functions from a preorder $\alpha$ to a preorder $\beta$) forms a preorder under the pointwise ordering: $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x \in \alpha$.

OrderHom.instPartialOrder instance

{β : Type*} [PartialOrder β] : PartialOrder (α →o β)

Full source

instance {β : Type*} [PartialOrder β] : PartialOrder (α →o β) :=
  @PartialOrder.lift (α →o β) (α → β) _ toFun ext

Partial Order on Order Homomorphisms

Informal description

For any type $\beta$ with a partial order, the type of order homomorphisms $\alpha \to_o \beta$ (monotone functions from $\alpha$ to $\beta$) forms a partial order under the pointwise ordering: $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x \in \alpha$.

OrderHom.le_def theorem

{f g : α →o β} : f ≤ g ↔ ∀ x, f x ≤ g x

Full source

theorem le_def {f g : α →o β} : f ≤ g ↔ ∀ x, f x ≤ g x :=
  Iff.rfl

Pointwise Order Characterization for Order Homomorphisms

Informal description

For any two order homomorphisms $f, g : \alpha \to_o \beta$ between preorders $\alpha$ and $\beta$, the inequality $f \leq g$ holds if and only if $f(x) \leq g(x)$ for all $x \in \alpha$.

OrderHom.coe_le_coe theorem

{f g : α →o β} : (f : α → β) ≤ g ↔ f ≤ g

Full source

@[simp, norm_cast]
theorem coe_le_coe {f g : α →o β} : (f : α → β) ≤ g ↔ f ≤ g :=
  Iff.rfl

Pointwise Inequality of Order Homomorphisms via Underlying Functions

Informal description

For any two order homomorphisms $f, g : \alpha \to_o \beta$ between preorders $\alpha$ and $\beta$, the pointwise inequality of the underlying functions $(f : \alpha \to \beta) \leq g$ holds if and only if $f \leq g$ in the pointwise order on order homomorphisms.

OrderHom.mk_le_mk theorem

{f g : α → β} {hf hg} : mk f hf ≤ mk g hg ↔ f ≤ g

Full source

@[simp]
theorem mk_le_mk {f g : α → β} {hf hg} : mkmk f hf ≤ mk g hg ↔ f ≤ g :=
  Iff.rfl

Pointwise Order Characterization for Constructed Order Homomorphisms

Informal description

For any two functions $f, g : \alpha \to \beta$ between preorders $\alpha$ and $\beta$, with respective proofs $hf$ and $hg$ that they are monotone, the order homomorphism $\text{mk}\,f\,hf$ is less than or equal to $\text{mk}\,g\,hg$ if and only if $f \leq g$ pointwise (i.e., $f(x) \leq g(x)$ for all $x \in \alpha$).

OrderHom.apply_mono theorem

{f g : α →o β} {x y : α} (h₁ : f ≤ g) (h₂ : x ≤ y) : f x ≤ g y

Full source

@[mono]
theorem apply_mono {f g : α →o β} {x y : α} (h₁ : f ≤ g) (h₂ : x ≤ y) : f x ≤ g y :=
  (h₁ x).trans <| g.mono h₂

Monotonicity of Order Homomorphism Application

Informal description

For any two order homomorphisms $f, g \colon \alpha \to_o \beta$ between preorders $\alpha$ and $\beta$, if $f \leq g$ in the pointwise order and $x \leq y$ in $\alpha$, then $f(x) \leq g(y)$ in $\beta$.

OrderHom.curry definition

: (α × β →o γ) ≃o (α →o β →o γ)

Full source

/-- Curry/uncurry as an order isomorphism between `α × β →o γ` and `α →o β →o γ`. -/
def curry : (α × β →o γ) ≃o (α →o β →o γ) where
  toFun f := ⟨fun x ↦ ⟨Function.curry f x, fun _ _ h ↦ f.mono ⟨le_rfl, h⟩⟩, fun _ _ h _ =>
    f.mono ⟨h, le_rfl⟩⟩
  invFun f := ⟨Function.uncurry fun x ↦ f x, fun x y h ↦ (f.mono h.1 x.2).trans ((f y.1).mono h.2)⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' := by simp [le_def]

Currying isomorphism for order homomorphisms

Informal description

The order isomorphism $\text{curry} : (\alpha \times \beta \to_o \gamma) \simeq_o (\alpha \to_o \beta \to_o \gamma)$ converts between a monotone function of two variables (from $\alpha \times \beta$ to $\gamma$) and its curried version (a monotone function from $\alpha$ to monotone functions from $\beta$ to $\gamma$). Specifically: - For $f : \alpha \times \beta \to_o \gamma$, the curried version $\text{curry}(f) : \alpha \to_o \beta \to_o \gamma$ satisfies $\text{curry}(f)(x)(y) = f(x, y)$ for all $x \in \alpha$, $y \in \beta$. - The inverse operation $\text{curry}^{-1}$ uncurries a function $g : \alpha \to_o \beta \to_o \gamma$ to $\text{curry}^{-1}(g)(x, y) = g(x)(y)$. This isomorphism preserves the order structure in both directions.

OrderHom.curry_apply theorem

(f : α × β →o γ) (x : α) (y : β) : curry f x y = f (x, y)

Full source

@[simp]
theorem curry_apply (f : α × βα × β →o γ) (x : α) (y : β) : curry f x y = f (x, y) :=
  rfl

Currying preserves evaluation for order homomorphisms

Informal description

For any order homomorphism $f : \alpha \times \beta \to_o \gamma$ and elements $x \in \alpha$, $y \in \beta$, the curried version of $f$ satisfies $(\text{curry}\,f)(x)(y) = f(x, y)$.

OrderHom.curry_symm_apply theorem

(f : α →o β →o γ) (x : α × β) : curry.symm f x = f x.1 x.2

Full source

@[simp]
theorem curry_symm_apply (f : α →o β →o γ) (x : α × β) : curry.symm f x = f x.1 x.2 :=
  rfl

Uncurrying preserves evaluation for order homomorphisms

Informal description

For any order homomorphism $f : \alpha \to_o \beta \to_o \gamma$ and any pair $(x_1, x_2) \in \alpha \times \beta$, the uncurried version of $f$ satisfies $\text{curry}^{-1}(f)(x_1, x_2) = f(x_1)(x_2)$.

OrderHom.comp definition

(g : β →o γ) (f : α →o β) : α →o γ

Full source

/-- The composition of two bundled monotone functions. -/
@[simps -fullyApplied]
def comp (g : β →o γ) (f : α →o β) : α →o γ :=
  ⟨g ∘ f, g.mono.comp f.mono⟩

Composition of order homomorphisms

Informal description

The composition of two order homomorphisms $ g : \beta \to_o \gamma $ and $ f : \alpha \to_o \beta $ is the order homomorphism $ g \circ f : \alpha \to_o \gamma $ defined by $ (g \circ f)(x) = g(f(x)) $, which preserves the order relation.

OrderHom.comp_mono theorem

 ⦃g₁ g₂ : β →o γ⦄ (hg : g₁ ≤ g₂) ⦃f₁ f₂ : α →o β⦄ (hf : f₁ ≤ f₂) : g₁.comp f₁ ≤ g₂.comp f₂

Full source

@[mono]
theorem comp_mono ⦃g₁ g₂ : β →o γ⦄ (hg : g₁ ≤ g₂) ⦃f₁ f₂ : α →o β⦄ (hf : f₁ ≤ f₂) :
    g₁.comp f₁ ≤ g₂.comp f₂ := fun _ => (hg _).trans (g₂.mono <| hf _)

Monotonicity of Order Homomorphism Composition

Informal description

For any order homomorphisms $g_1, g_2 : \beta \to_o \gamma$ and $f_1, f_2 : \alpha \to_o \beta$, if $g_1 \leq g_2$ and $f_1 \leq f_2$ in the pointwise order, then the composition $g_1 \circ f_1 \leq g_2 \circ f_2$ as order homomorphisms from $\alpha$ to $\gamma$.

OrderHom.mk_comp_mk theorem

(g : β → γ) (f : α → β) (hg hf) : comp ⟨g, hg⟩ ⟨f, hf⟩ = ⟨g ∘ f, hg.comp hf⟩

Full source

@[simp] lemma mk_comp_mk (g : β → γ) (f : α → β) (hg hf) :
    comp ⟨g, hg⟩ ⟨f, hf⟩ = ⟨g ∘ f, hg.comp hf⟩ := rfl

Composition of Constructed Order Homomorphisms Equals Constructed Composition

Informal description

Given functions $g : \beta \to \gamma$ and $f : \alpha \to \beta$ with proofs $hg$ and $hf$ that they are order-preserving, the composition of the order homomorphisms $\langle g, hg \rangle$ and $\langle f, hf \rangle$ is equal to the order homomorphism $\langle g \circ f, hg \circ hf \rangle$.

OrderHom.compₘ definition

: (β →o γ) →o (α →o β) →o α →o γ

Full source

/-- The composition of two bundled monotone functions, a fully bundled version. -/
@[simps! -fullyApplied]
def compₘ : (β →o γ) →o (α →o β) →o α →o γ :=
  curry ⟨fun f : (β →o γ) × (α →o β) => f.1.comp f.2, fun _ _ h => comp_mono h.1 h.2⟩

Fully bundled composition of order homomorphisms

Informal description

The fully bundled composition of order homomorphisms, which takes two order homomorphisms $ g : \beta \to_o \gamma $ and $ f : \alpha \to_o \beta $ and returns their composition $ g \circ f : \alpha \to_o \gamma $. This version is fully bundled as a monotone map from $ \beta \to_o \gamma $ to $ (\alpha \to_o \beta) \to_o (\alpha \to_o \gamma) $.

OrderHom.comp_id theorem

(f : α →o β) : comp f id = f

Full source

@[simp]
theorem comp_id (f : α →o β) : comp f id = f := by
  ext
  rfl

Right Identity Law for Order Homomorphism Composition

Informal description

For any order homomorphism $f \colon \alpha \to_o \beta$, the composition of $f$ with the identity order homomorphism on $\alpha$ is equal to $f$ itself, i.e., $f \circ \operatorname{id} = f$.

OrderHom.id_comp theorem

(f : α →o β) : comp id f = f

Full source

@[simp]
theorem id_comp (f : α →o β) : comp id f = f := by
  ext
  rfl

Left identity law for order homomorphism composition

Informal description

For any order homomorphism $f \colon \alpha \to_o \beta$ between preorders, the composition of the identity order homomorphism $\mathrm{id} \colon \alpha \to_o \alpha$ with $f$ equals $f$ itself. That is, $\mathrm{id} \circ f = f$.

OrderHom.const definition

(α : Type*) [Preorder α] {β : Type*} [Preorder β] : β →o α →o β

Full source

/-- Constant function bundled as an `OrderHom`. -/
@[simps -fullyApplied]
def const (α : Type*) [Preorder α] {β : Type*} [Preorder β] : β →o α →o β where
  toFun b := ⟨Function.const α b, fun _ _ _ => le_rfl⟩
  monotone' _ _ h _ := h

Constant order homomorphism

Informal description

The constant function bundled as an order homomorphism. For a fixed element $b$ in a preorder $\beta$, this defines a monotone function from any preorder $\alpha$ to $\beta$ that maps every element of $\alpha$ to $b$. The function is monotone since for any $x, y \in \alpha$, the implication $x \leq y \rightarrow b \leq b$ holds trivially.

OrderHom.const_comp theorem

(f : α →o β) (c : γ) : (const β c).comp f = const α c

Full source

@[simp]
theorem const_comp (f : α →o β) (c : γ) : (const β c).comp f = const α c :=
  rfl

Composition of Constant Order Homomorphism with Any Order Homomorphism Yields Constant Function

Informal description

For any order homomorphism $f : \alpha \to_o \beta$ and any element $c \in \gamma$, the composition of the constant order homomorphism $\text{const}_\beta(c)$ with $f$ equals the constant order homomorphism $\text{const}_\alpha(c)$. That is, $(\text{const}_\beta(c)) \circ f = \text{const}_\alpha(c)$.

OrderHom.comp_const theorem

(γ : Type*) [Preorder γ] (f : α →o β) (c : α) : f.comp (const γ c) = const γ (f c)

Full source

@[simp]
theorem comp_const (γ : Type*) [Preorder γ] (f : α →o β) (c : α) :
    f.comp (const γ c) = const γ (f c) :=
  rfl

Composition of Order Homomorphism with Constant Function Yields Constant Function

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preorders. For any order homomorphism $f : \alpha \to_o \beta$ and any element $c \in \alpha$, the composition of $f$ with the constant order homomorphism $\text{const}_\gamma(c)$ equals the constant order homomorphism $\text{const}_\gamma(f(c))$. That is, $f \circ \text{const}_\gamma(c) = \text{const}_\gamma(f(c))$.

OrderHom.prod definition

(f : α →o β) (g : α →o γ) : α →o β × γ

Full source

/-- Given two bundled monotone maps `f`, `g`, `f.prod g` is the map `x ↦ (f x, g x)` bundled as a
`OrderHom`. -/
@[simps]
protected def prod (f : α →o β) (g : α →o γ) : α →o β × γ :=
  ⟨fun x => (f x, g x), fun _ _ h => ⟨f.mono h, g.mono h⟩⟩

Product of Order Homomorphisms

Informal description

Given two order homomorphisms $ f : \alpha \to_o \beta $ and $ g : \alpha \to_o \gamma $, the function $ \text{OrderHom.prod} \, f \, g $ maps each element $ x \in \alpha $ to the pair $ (f x, g x) $, forming an order homomorphism from $ \alpha $ to the product order $ \beta \times \gamma $. This means that if $ x \leq y $ in $ \alpha $, then both $ f x \leq f y $ and $ g x \leq g y $ hold, ensuring the pair $ (f x, g x) \leq (f y, g y) $ in the product order.

OrderHom.prod_mono theorem

 {f₁ f₂ : α →o β} (hf : f₁ ≤ f₂) {g₁ g₂ : α →o γ} (hg : g₁ ≤ g₂) : f₁.prod g₁ ≤ f₂.prod g₂

Full source

@[mono]
theorem prod_mono {f₁ f₂ : α →o β} (hf : f₁ ≤ f₂) {g₁ g₂ : α →o γ} (hg : g₁ ≤ g₂) :
    f₁.prod g₁ ≤ f₂.prod g₂ := fun _ => Prod.le_def.2 ⟨hf _, hg _⟩

Monotonicity of Product Order Homomorphism Construction

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preorders. For any order homomorphisms $f_1, f_2 : \alpha \to_o \beta$ and $g_1, g_2 : \alpha \to_o \gamma$, if $f_1 \leq f_2$ and $g_1 \leq g_2$, then the product homomorphism $f_1 \times g_1 \leq f_2 \times g_2$ in the pointwise order on $\alpha \to_o \beta \times \gamma$.

OrderHom.comp_prod_comp_same theorem

(f₁ f₂ : β →o γ) (g : α →o β) : (f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g

Full source

theorem comp_prod_comp_same (f₁ f₂ : β →o γ) (g : α →o β) :
    (f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g :=
  rfl

Composition Distributes Over Product of Order Homomorphisms

Informal description

For any order homomorphisms $f_1, f_2 : \beta \to_o \gamma$ and $g : \alpha \to_o \beta$, the composition of $g$ with the product homomorphism $(f_1 \times f_2)$ is equal to the product of the compositions $(f_1 \circ g) \times (f_2 \circ g)$. In other words, $(f_1 \circ g, f_2 \circ g) = (f_1 \times f_2) \circ g$ as order homomorphisms from $\alpha$ to $\gamma \times \gamma$.

OrderHom.prodₘ definition

: (α →o β) →o (α →o γ) →o α →o β × γ

Full source

/-- 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. -/
@[simps!]
def prodₘ : (α →o β) →o (α →o γ) →o α →o β × γ :=
  curry ⟨fun f : (α →o β) × (α →o γ) => f.1.prod f.2, fun _ _ h => prod_mono h.1 h.2⟩

Fully bundled product of order homomorphisms

Informal description

The fully bundled version of the product construction for order homomorphisms. Given two order homomorphisms $f : \alpha \to_o \beta$ and $g : \alpha \to_o \gamma$, the function $\text{OrderHom.prodₘ}$ maps the pair $(f, g)$ to the order homomorphism $x \mapsto (f x, g x)$. This operation is itself an order homomorphism from $(\alpha \to_o \beta) \times (\alpha \to_o \gamma)$ to $\alpha \to_o \beta \times \gamma$, meaning it preserves the pointwise order structure.

OrderHom.diag definition

: α →o α × α

Full source

/-- Diagonal embedding of `α` into `α × α` as an `OrderHom`. -/
@[simps!]
def diag : α →o α × α :=
  id.prod id

Diagonal order homomorphism

Informal description

The diagonal embedding of a preorder $\alpha$ into $\alpha \times \alpha$ as an order homomorphism. Specifically, it maps each element $x \in \alpha$ to the pair $(x, x)$, and is monotone with respect to the order: if $x \leq y$, then $(x, x) \leq (y, y)$ in the product order.

OrderHom.onDiag definition

(f : α →o α →o β) : α →o β

Full source

/-- Restriction of `f : α →o α →o β` to the diagonal. -/
@[simps! +simpRhs]
def onDiag (f : α →o α →o β) : α →o β :=
  (curry.symm f).comp diag

Diagonal restriction of a monotone function

Informal description

Given a monotone function $ f : \alpha \to_o \alpha \to_o \beta $ (a function that is monotone in both arguments), the restriction of $ f $ to the diagonal is the monotone function $ \alpha \to_o \beta $ defined by $ x \mapsto f(x, x) $.

OrderHom.fst definition

: α × β →o α

Full source

/-- `Prod.fst` as an `OrderHom`. -/
@[simps]
def fst : α × βα × β →o α :=
  ⟨Prod.fst, fun _ _ h => h.1⟩

First projection as an order homomorphism

Informal description

The function that projects the first component of a pair in the product order $\alpha \times \beta$ to $\alpha$, bundled as an order homomorphism. Specifically, for any pair $(x, y) \in \alpha \times \beta$, the function returns $x$, and it is monotone with respect to the product order: if $(x_1, y_1) \leq (x_2, y_2)$, then $x_1 \leq x_2$.

OrderHom.snd definition

: α × β →o β

Full source

/-- `Prod.snd` as an `OrderHom`. -/
@[simps]
def snd : α × βα × β →o β :=
  ⟨Prod.snd, fun _ _ h => h.2⟩

Second projection as an order homomorphism

Informal description

The function that projects the second component of a pair in the product order $\alpha \times \beta$ to $\beta$, bundled as an order homomorphism. Specifically, for any pair $(x, y) \in \alpha \times \beta$, the function returns $y$, and it is monotone with respect to the product order: if $(x_1, y_1) \leq (x_2, y_2)$, then $y_1 \leq y_2$.

OrderHom.fst_prod_snd theorem

: (fst : α × β →o α).prod snd = id

Full source

@[simp]
theorem fst_prod_snd : (fst : α × βα × β →o α).prod snd = id := by
  ext ⟨x, y⟩ : 2
  rfl

Product of Projections is Identity: $(fst, snd) = id$

Informal description

The product of the first and second projection order homomorphisms on $\alpha \times \beta$ equals the identity order homomorphism on $\alpha \times \beta$. That is, for any pair $(x, y) \in \alpha \times \beta$, we have $(fst(x, y), snd(x, y)) = (x, y)$.

OrderHom.fst_comp_prod theorem

(f : α →o β) (g : α →o γ) : fst.comp (f.prod g) = f

Full source

@[simp]
theorem fst_comp_prod (f : α →o β) (g : α →o γ) : fst.comp (f.prod g) = f :=
  ext _ _ rfl

First projection composed with product equals first factor

Informal description

For any two order homomorphisms $f \colon \alpha \to_o \beta$ and $g \colon \alpha \to_o \gamma$, the composition of the first projection homomorphism $\mathrm{fst} \colon \alpha \times \beta \to_o \alpha$ with the product homomorphism $f \times g \colon \alpha \to_o \beta \times \gamma$ equals $f$. That is, $\mathrm{fst} \circ (f \times g) = f$.

OrderHom.snd_comp_prod theorem

(f : α →o β) (g : α →o γ) : snd.comp (f.prod g) = g

Full source

@[simp]
theorem snd_comp_prod (f : α →o β) (g : α →o γ) : snd.comp (f.prod g) = g :=
  ext _ _ rfl

Composition of Second Projection with Product Homomorphism Equals Second Factor

Informal description

For any two order homomorphisms $f \colon \alpha \to_o \beta$ and $g \colon \alpha \to_o \gamma$, the composition of the second projection homomorphism $\mathrm{snd} \colon \alpha \times \beta \to_o \beta$ with the product homomorphism $f \times g \colon \alpha \to_o \beta \times \gamma$ equals $g$. In other words, $\mathrm{snd} \circ (f \times g) = g$.

OrderHom.prodIso definition

: (α →o β × γ) ≃o (α →o β) × (α →o γ)

Full source

/-- Order isomorphism between the space of monotone maps to `β × γ` and the product of the spaces
of monotone maps to `β` and `γ`. -/
@[simps]
def prodIso : (α →o β × γ) ≃o (α →o β) × (α →o γ) where
  toFun f := (fst.comp f, snd.comp f)
  invFun f := f.1.prod f.2
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' := forall_and.symm

Order isomorphism between monotone maps to a product and pairs of monotone maps

Informal description

The order isomorphism between the space of monotone maps from $\alpha$ to $\beta \times \gamma$ and the product of the spaces of monotone maps from $\alpha$ to $\beta$ and from $\alpha$ to $\gamma$. Specifically, it maps a monotone function $f : \alpha \to \beta \times \gamma$ to the pair $(f_1, f_2)$, where $f_1$ and $f_2$ are the compositions of $f$ with the first and second projections, respectively. Conversely, it maps a pair of monotone functions $(g, h)$ to the monotone function $x \mapsto (g x, h x)$.

OrderHom.prodMap definition

(f : α →o β) (g : γ →o δ) : α × γ →o β × δ

Full source

/-- `Prod.map` of two `OrderHom`s as an `OrderHom` -/
@[simps]
def prodMap (f : α →o β) (g : γ →o δ) : α × γα × γ →o β × δ :=
  ⟨Prod.map f g, fun _ _ h => ⟨f.mono h.1, g.mono h.2⟩⟩

Product of order homomorphisms

Informal description

Given two order homomorphisms $ f : \alpha \to_o \beta $ and $ g : \gamma \to_o \delta $, the function $ \text{prodMap} $ constructs an order homomorphism $ \alpha \times \gamma \to_o \beta \times \delta $ by applying $ f $ to the first component and $ g $ to the second component. This homomorphism is monotone, meaning that if $ (x_1, y_1) \leq (x_2, y_2) $ in $ \alpha \times \gamma $, then $ (f x_1, g y_1) \leq (f x_2, g y_2) $ in $ \beta \times \delta $.

Pi.evalOrderHom definition

(i : ι) : (∀ j, π j) →o π i

Full source

/-- Evaluation of an unbundled function at a point (`Function.eval`) as an `OrderHom`. -/
@[simps -fullyApplied]
def _root_.Pi.evalOrderHom (i : ι) : (∀ j, π j) →o π i :=
  ⟨Function.eval i, Function.monotone_eval i⟩

Monotone evaluation map at an index

Informal description

For a given index $i$ in some index set $\iota$, the evaluation function $\operatorname{eval}_i$ maps a family of elements $(f_j)_{j \in \iota}$ in the product space $\prod_{j \in \iota} \pi_j$ (where each $\pi_j$ is a preorder) to its $i$-th component $f_i \in \pi_i$. This function is bundled with a proof that it is monotone, meaning that if $f \leq g$ in the product order (i.e., $f_j \leq g_j$ for all $j$), then $\operatorname{eval}_i(f) \leq \operatorname{eval}_i(g)$.

OrderHom.coeFnHom definition

: (α →o β) →o α → β

Full source

/-- The "forgetful functor" from `α →o β` to `α → β` that takes the underlying function,
is monotone. -/
@[simps -fullyApplied]
def coeFnHom : (α →o β) →o α → β where
  toFun f := f
  monotone' _ _ h := h

Coefficient function as an order homomorphism

Informal description

The function that maps an order homomorphism $ f : \alpha \to_o \beta $ to its underlying function $ f : \alpha \to \beta $, is itself a monotone function between the preorder of order homomorphisms $ \alpha \to_o \beta $ and the preorder of functions $ \alpha \to \beta $ (ordered pointwise).

OrderHom.apply definition

(x : α) : (α →o β) →o β

Full source

/-- Function application `fun f => f a` (for fixed `a`) is a monotone function from the
monotone function space `α →o β` to `β`. See also `Pi.evalOrderHom`. -/
@[simps! -fullyApplied]
def apply (x : α) : (α →o β) →o β :=
  (Pi.evalOrderHom x).comp coeFnHom

Evaluation of order homomorphism at a point

Informal description

For a fixed element $ x $ in a preorder $ \alpha $, the function that evaluates an order homomorphism $ f : \alpha \to_o \beta $ at $ x $ (i.e., maps $ f $ to $ f(x) $) is itself a monotone function from the preorder of order homomorphisms $ \alpha \to_o \beta $ (ordered pointwise) to the codomain preorder $ \beta $.

OrderHom.pi definition

(f : ∀ i, α →o π i) : α →o ∀ i, π i

Full source

/-- Construct a bundled monotone map `α →o Π i, π i` from a family of monotone maps
`f i : α →o π i`. -/
@[simps]
def pi (f : ∀ i, α →o π i) : α →o ∀ i, π i :=
  ⟨fun x i => f i x, fun _ _ h i => (f i).mono h⟩

Pointwise order homomorphism family

Informal description

Given a family of order homomorphisms $f_i : \alpha \to_o \pi_i$ for each index $i$, the function `OrderHom.pi` constructs a bundled monotone map $\alpha \to_o \Pi i, \pi_i$ by pointwise application. Specifically, for any $x \in \alpha$, the resulting function maps $x$ to the tuple $(f_i(x))_{i}$ and preserves the order relation: if $x \leq y$ in $\alpha$, then $f_i(x) \leq f_i(y)$ for all $i$.

OrderHom.piIso definition

: (α →o ∀ i, π i) ≃o ∀ i, α →o π i

Full source

/-- Order isomorphism between bundled monotone maps `α →o Π i, π i` and families of bundled monotone
maps `Π i, α →o π i`. -/
@[simps]
def piIso : (α →o ∀ i, π i) ≃o ∀ i, α →o π i where
  toFun f i := (Pi.evalOrderHom i).comp f
  invFun := pi
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' := forall_swap

Order isomorphism between families of order homomorphisms and product-valued order homomorphisms

Informal description

The order isomorphism between the space of bundled monotone maps $\alpha \to_o \prod_i \pi_i$ and the product space $\prod_i (\alpha \to_o \pi_i)$ of bundled monotone maps. Specifically, it establishes a bijection that preserves the order relation in both directions, where a family of order homomorphisms $(f_i : \alpha \to_o \pi_i)_i$ corresponds to the single order homomorphism $\alpha \to_o \prod_i \pi_i$ defined by $x \mapsto (f_i(x))_i$.

OrderHom.Subtype.val definition

(p : α → Prop) : Subtype p →o α

Full source

/-- `Subtype.val` as a bundled monotone function. -/
@[simps -fullyApplied]
def Subtype.val (p : α → Prop) : SubtypeSubtype p →o α :=
  ⟨_root_.Subtype.val, fun _ _ h => h⟩

Subtype embedding as an order homomorphism

Informal description

The function that embeds a subtype `{x // p x}` into its base type `α` as a bundled monotone function. Specifically, it maps each element `x` of the subtype to its underlying value in `α`, and preserves the order relation: if `x ≤ y` in the subtype, then `x ≤ y` in `α`.

Subtype.orderEmbedding definition

{p q : α → Prop} (h : ∀ a, p a → q a) : { x // p x } ↪o { x // q x }

Full source

/-- `Subtype.impEmbedding` as an order embedding. -/
@[simps!]
def _root_.Subtype.orderEmbedding {p q : α → Prop} (h : ∀ a, p a → q a) :
    {x // p x}{x // p x} ↪o {x // q x} :=
  { Subtype.impEmbedding _ _ h with
    map_rel_iff' := by aesop }

Order embedding between subtypes under implication of predicates

Informal description

Given two predicates $ p $ and $ q $ on a type $ \alpha $ such that $ p(a) $ implies $ q(a) $ for all $ a \in \alpha $, the order embedding from the subtype $ \{x \mid p(x)\} $ to the subtype $ \{x \mid q(x)\} $ maps each element $ x $ to itself and preserves the order relation: for any $ x, y $ in $ \{x \mid p(x)\} $, $ x \leq y $ if and only if $ x \leq y $ in $ \{x \mid q(x)\} $.

OrderHom.unique instance

[Subsingleton α] : Unique (α →o α)

Full source

/-- There is a unique monotone map from a subsingleton to itself. -/
instance unique [Subsingleton α] : Unique (α →o α) where
  default := OrderHom.id
  uniq _ := ext _ _ (Subsingleton.elim _ _)

Uniqueness of Order Homomorphisms on Subsingleton Preorders

Informal description

For any preorder $\alpha$ that is a subsingleton (i.e., all elements are equal), there is exactly one order homomorphism from $\alpha$ to itself, which is the identity function.

OrderHom.orderHom_eq_id theorem

[Subsingleton α] (g : α →o α) : g = OrderHom.id

Full source

theorem orderHom_eq_id [Subsingleton α] (g : α →o α) : g = OrderHom.id :=
  Subsingleton.elim _ _

Uniqueness of Order Homomorphisms on Subsingleton Preorders

Informal description

For any preorder $\alpha$ that is a subsingleton (i.e., all elements are equal), every order homomorphism $g : \alpha \to \alpha$ is equal to the identity order homomorphism.

OrderHom.dual definition

: (α →o β) ≃ (αᵒᵈ →o βᵒᵈ)

Full source

/-- Reinterpret a bundled monotone function as a monotone function between dual orders. -/
@[simps]
protected def dual : (α →o β) ≃ (αᵒᵈ →o βᵒᵈ) where
  toFun f := ⟨(OrderDual.toDual : β → βᵒᵈ) ∘ (f : α → β) ∘
    (OrderDual.ofDual : αᵒᵈ → α), f.mono.dual⟩
  invFun f := ⟨OrderDual.ofDual ∘ f ∘ OrderDual.toDual, f.mono.dual⟩
  left_inv _ := rfl
  right_inv _ := rfl

Dual of an order homomorphism

Informal description

The equivalence between the type of order homomorphisms from $\alpha$ to $\beta$ and the type of order homomorphisms from the order dual of $\alpha$ to the order dual of $\beta$. Specifically, given an order homomorphism $f : \alpha \to_o \beta$, its dual version is the composition of the order dual isomorphisms with $f$, i.e., $\text{toDual} \circ f \circ \text{ofDual} : \alpha^\text{op} \to_o \beta^\text{op}$.

OrderHom.dual_id theorem

: (OrderHom.id : α →o α).dual = OrderHom.id

Full source

@[simp]
theorem dual_id : (OrderHom.id : α →o α).dual = OrderHom.id :=
  rfl

Dual of Identity Order Homomorphism is Identity

Informal description

The dual of the identity order homomorphism on a preorder $\alpha$ is equal to the identity order homomorphism on the order dual $\alpha^\text{op}$. That is, $(\operatorname{id} : \alpha \to_o \alpha)^\text{op} = \operatorname{id} : \alpha^\text{op} \to_o \alpha^\text{op}$.

OrderHom.dual_comp theorem

(g : β →o γ) (f : α →o β) : (g.comp f).dual = g.dual.comp f.dual

Full source

@[simp]
theorem dual_comp (g : β →o γ) (f : α →o β) :
    (g.comp f).dual = g.dual.comp f.dual :=
  rfl

Dual of Composition of Order Homomorphisms Equals Composition of Duals

Informal description

For any order homomorphisms $f \colon \alpha \to_o \beta$ and $g \colon \beta \to_o \gamma$ between preorders, the dual of their composition $(g \circ f)^\text{op}$ is equal to the composition of their duals $g^\text{op} \circ f^\text{op}$ as order homomorphisms between the order duals $\alpha^\text{op} \to_o \beta^\text{op} \to_o \gamma^\text{op}$.

OrderHom.symm_dual_id theorem

: OrderHom.dual.symm OrderHom.id = (OrderHom.id : α →o α)

Full source

@[simp]
theorem symm_dual_id : OrderHom.dual.symm OrderHom.id = (OrderHom.id : α →o α) :=
  rfl

Inverse of Dual Identity Order Homomorphism is Identity

Informal description

The inverse of the dual of the identity order homomorphism is equal to the identity order homomorphism itself. That is, for any preorder $\alpha$, we have $\text{OrderHom.dual.symm}(\text{OrderHom.id}) = \text{OrderHom.id} : \alpha \to_o \alpha$.

OrderHom.symm_dual_comp theorem

 (g : βᵒᵈ →o γᵒᵈ) (f : αᵒᵈ →o βᵒᵈ) : OrderHom.dual.symm (g.comp f) = (OrderHom.dual.symm g).comp (OrderHom.dual.symm f)

Full source

@[simp]
theorem symm_dual_comp (g : βᵒᵈβᵒᵈ →o γᵒᵈ) (f : αᵒᵈαᵒᵈ →o βᵒᵈ) :
    OrderHom.dual.symm (g.comp f) = (OrderHom.dual.symm g).comp (OrderHom.dual.symm f) :=
  rfl

Inverse of Dual Composition Equals Composition of Inverses for Order Homomorphisms

Informal description

For any order homomorphisms $f \colon \alpha^\text{op} \to_o \beta^\text{op}$ and $g \colon \beta^\text{op} \to_o \gamma^\text{op}$ between order duals of preorders, the inverse of the dual of their composition $(g \circ f)$ is equal to the composition of the inverses of their duals $(g^\text{op})^{-1} \circ (f^\text{op})^{-1}$ as order homomorphisms $\alpha \to_o \beta \to_o \gamma$.

OrderHom.dualIso definition

(α β : Type*) [Preorder α] [Preorder β] : (α →o β) ≃o (αᵒᵈ →o βᵒᵈ)ᵒᵈ

Full source

/-- `OrderHom.dual` as an order isomorphism. -/
def dualIso (α β : Type*) [Preorder α] [Preorder β] : (α →o β) ≃o (αᵒᵈ →o βᵒᵈ)ᵒᵈ where
  toEquiv := OrderHom.dual.trans OrderDual.toDual
  map_rel_iff' := Iff.rfl

Order isomorphism between order homomorphisms and their duals

Informal description

The order isomorphism $\text{OrderHom.dualIso}$ between the type of order homomorphisms $\alpha \to_o \beta$ and the type of order homomorphisms $(\alpha^\text{op} \to_o \beta^\text{op})^\text{op}$, where $\alpha^\text{op}$ and $\beta^\text{op}$ denote the order duals of $\alpha$ and $\beta$ respectively. This isomorphism is constructed by composing the equivalence $\text{OrderHom.dual}$ with the order dual isomorphism $\text{OrderDual.toDual}$, and it preserves the order relation in both directions.

OrderHom.uliftMap definition

(f : α →o β) : ULift α →o ULift β

Full source

/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `ULift α →o ULift β` in a
higher universe. -/
@[simps!]
def uliftMap (f : α →o β) : ULiftULift α →o ULift β :=
  ⟨fun i => ⟨f i.down⟩, fun _ _ h ↦ f.monotone h⟩

Lifting of an order homomorphism to a higher universe via ULift

Informal description

Given an order homomorphism $ f : \alpha \to_o \beta $ between preorders, the function lifts $ f $ to an order homomorphism $ \text{ULift} \alpha \to_o \text{ULift} \beta $ in a higher universe. Specifically, for any $ i : \text{ULift} \alpha $, the lifted function maps $ i $ to $ \langle f \, i.\text{down} \rangle $, and it preserves the order relation: if $ x \leq y $ in $ \text{ULift} \alpha $, then $ f \, x.\text{down} \leq f \, y.\text{down} $ in $ \beta $, ensuring the lifted function is monotone.

OrderHomClass.toOrderHomClassOrderDual instance

[LE α] [LE β] [FunLike F α β] [OrderHomClass F α β] : OrderHomClass F αᵒᵈ βᵒᵈ

Full source

instance (priority := 90) OrderHomClass.toOrderHomClassOrderDual [LE α] [LE β]
    [FunLike F α β] [OrderHomClass F α β] : OrderHomClass F αᵒᵈ βᵒᵈ where
  map_rel f := map_rel f

Order-Preserving Morphisms on Dual Preorders

Informal description

For any type $F$ of order-preserving morphisms between preorders $\alpha$ and $\beta$, the same morphisms also preserve the order when viewed as maps between the dual preorders $\alpha^\text{op}$ and $\beta^\text{op}$.

RelEmbedding.orderEmbeddingOfLTEmbedding definition

 [PartialOrder α] [PartialOrder β] (f : ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop)) : α ↪o β

Full source

/-- Embeddings of partial orders that preserve `<` also preserve `≤`. -/
def RelEmbedding.orderEmbeddingOfLTEmbedding [PartialOrder α] [PartialOrder β]
    (f : ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop)) : α ↪o β :=
  { f with
    map_rel_iff' := by
      intros
      simp [le_iff_lt_or_eq, f.map_rel_iff, f.injective.eq_iff] }

Order embedding induced by a strict order embedding

Informal description

Given a relation embedding $f$ between the strict order relations $<$ on two partially ordered sets $\alpha$ and $\beta$, the function constructs an order embedding between $\alpha$ and $\beta$ with respect to the non-strict order relations $\leq$. Specifically, for any $x, y \in \alpha$, we have $x \leq y$ if and only if $f(x) \leq f(y)$ in $\beta$.

RelEmbedding.orderEmbeddingOfLTEmbedding_apply theorem

 [PartialOrder α] [PartialOrder β] {f : ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop)} {x : α} :
  RelEmbedding.orderEmbeddingOfLTEmbedding f x = f x

Full source

@[simp]
theorem RelEmbedding.orderEmbeddingOfLTEmbedding_apply [PartialOrder α] [PartialOrder β]
    {f : ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop)} {x : α} :
    RelEmbedding.orderEmbeddingOfLTEmbedding f x = f x :=
  rfl

Application of Order Embedding Induced by Strict Order Embedding

Informal description

For any partially ordered sets $\alpha$ and $\beta$, given a strict order embedding $f \colon (\alpha, <) \hookrightarrow (\beta, <)$, the application of the induced order embedding $\text{orderEmbeddingOfLTEmbedding}(f)$ to an element $x \in \alpha$ is equal to $f(x)$.

OrderEmbedding.ltEmbedding definition

: ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop)

Full source

/-- `<` is preserved by order embeddings of preorders. -/
def ltEmbedding : ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop) :=
  { f with map_rel_iff' := by intros; simp [lt_iff_le_not_le, f.map_rel_iff] }

Strict order embedding induced by an order embedding

Informal description

Given an order embedding $f : \alpha \hookrightarrow \beta$ between two partially ordered sets, the function `OrderEmbedding.ltEmbedding` constructs a relation embedding between the strict orders on $\alpha$ and $\beta$. Specifically, it maps the strict order relation $<$ on $\alpha$ to the strict order relation $<$ on $\beta$, preserving and reflecting the relation such that for any $x, y \in \alpha$, $x < y$ if and only if $f(x) < f(y)$.

OrderEmbedding.ltEmbedding_apply theorem

(x : α) : f.ltEmbedding x = f x

Full source

@[simp]
theorem ltEmbedding_apply (x : α) : f.ltEmbedding x = f x :=
  rfl

Application of Induced Strict Order Embedding

Informal description

For any order embedding $f \colon \alpha \hookrightarrow \beta$ between partially ordered sets and any element $x \in \alpha$, the application of the induced strict order embedding to $x$ equals $f(x)$, i.e., $f_{\text{lt}}(x) = f(x)$.

OrderEmbedding.le_iff_le theorem

{a b} : f a ≤ f b ↔ a ≤ b

Full source

@[simp]
theorem le_iff_le {a b} : f a ≤ f b ↔ a ≤ b :=
  f.map_rel_iff

Order Embedding Preserves and Reflects Order Relations

Informal description

For any order embedding $f \colon \alpha \hookrightarrow \beta$ between preordered types and for any elements $a, b \in \alpha$, we have $f(a) \leq f(b)$ in $\beta$ if and only if $a \leq b$ in $\alpha$.

OrderEmbedding.lt_iff_lt theorem

{a b} : f a < f b ↔ a < b

Full source

@[simp]
theorem lt_iff_lt {a b} : f a < f b ↔ a < b :=
  f.ltEmbedding.map_rel_iff

Order Embedding Preserves and Reflects Strict Order Relations

Informal description

For any order embedding $f \colon \alpha \hookrightarrow \beta$ between preordered types and for any elements $a, b \in \alpha$, we have $f(a) < f(b)$ in $\beta$ if and only if $a < b$ in $\alpha$.

OrderEmbedding.monotone theorem

: Monotone f

Full source

protected theorem monotone : Monotone f :=
  OrderHomClass.monotone f

Monotonicity of Order Embeddings

Informal description

For any order embedding $f \colon \alpha \hookrightarrow \beta$ between preordered types, the function $f$ is monotone. That is, for any $x, y \in \alpha$, if $x \leq y$, then $f(x) \leq f(y)$.

OrderEmbedding.strictMono theorem

: StrictMono f

Full source

protected theorem strictMono : StrictMono f := fun _ _ => f.lt_iff_lt.2

Order Embeddings are Strictly Monotone

Informal description

An order embedding $f \colon \alpha \hookrightarrow \beta$ between preordered types is strictly monotone, meaning that for any $x, y \in \alpha$, if $x < y$ then $f(x) < f(y)$.

OrderEmbedding.acc theorem

(a : α) : Acc (· < ·) (f a) → Acc (· < ·) a

Full source

protected theorem acc (a : α) : Acc (· < ·) (f a) → Acc (· < ·) a :=
  f.ltEmbedding.acc a

Accessibility Preservation under Order Embeddings

Informal description

For any order embedding $f \colon \alpha \hookrightarrow \beta$ between partially ordered sets and any element $a \in \alpha$, if the image $f(a)$ is accessible with respect to the strict order relation $<$ on $\beta$, then $a$ is accessible with respect to the strict order relation $<$ on $\alpha$. Here, an element $x$ is called *accessible* with respect to a relation $<$ if every descending $<$-chain starting from $x$ is finite.

OrderEmbedding.wellFounded theorem

(f : α ↪o β) : WellFounded ((· < ·) : β → β → Prop) → WellFounded ((· < ·) : α → α → Prop)

Full source

protected theorem wellFounded (f : α ↪o β) :
    WellFounded ((· < ·) : β → β → Prop) → WellFounded ((· < ·) : α → α → Prop) :=
  f.ltEmbedding.wellFounded

Well-foundedness preservation under order embeddings

Informal description

Given an order embedding $f \colon \alpha \hookrightarrow \beta$ between partially ordered sets, if the strict order relation $<$ on $\beta$ is well-founded, then the strict order relation $<$ on $\alpha$ is also well-founded. Here, a relation $<$ on a type is called *well-founded* if every non-empty subset has a minimal element with respect to $<$.

OrderEmbedding.isWellOrder theorem

[IsWellOrder β (· < ·)] (f : α ↪o β) : IsWellOrder α (· < ·)

Full source

protected theorem isWellOrder [IsWellOrder β (· < ·)] (f : α ↪o β) : IsWellOrder α (· < ·) :=
  f.ltEmbedding.isWellOrder

Well-order preservation under order embeddings

Informal description

Let $\alpha$ and $\beta$ be types equipped with strict order relations $<$, and let $f \colon \alpha \hookrightarrow \beta$ be an order embedding. If $<$ is a well-order on $\beta$, then $<$ is also a well-order on $\alpha$. Here, a *well-order* is a strict total order where every non-empty subset has a minimal element with respect to $<$.

OrderEmbedding.dual definition

: αᵒᵈ ↪o βᵒᵈ

Full source

/-- An order embedding is also an order embedding between dual orders. -/
protected def dual : αᵒᵈαᵒᵈ ↪o βᵒᵈ :=
  ⟨f.toEmbedding, f.map_rel_iff⟩

Dual order embedding

Informal description

Given an order embedding $f : \alpha \hookrightarrow \beta$, the dual order embedding $f^{\mathrm{dual}} : \alpha^{\mathrm{op}} \hookrightarrow \beta^{\mathrm{op}}$ is defined by the same underlying function but between the opposite orders, preserving the order-reversing structure.

OrderEmbedding.wellFoundedLT theorem

[WellFoundedLT β] (f : α ↪o β) : WellFoundedLT α

Full source

/-- A preorder which embeds into a well-founded preorder is itself well-founded. -/
protected theorem wellFoundedLT [WellFoundedLT β] (f : α ↪o β) : WellFoundedLT α where
  wf := f.wellFounded IsWellFounded.wf

Well-foundedness of strict order preserved under order embeddings

Informal description

Let $\alpha$ and $\beta$ be preordered types, and let $f \colon \alpha \hookrightarrow \beta$ be an order embedding. If the strict order relation $<$ on $\beta$ is well-founded, then the strict order relation $<$ on $\alpha$ is also well-founded. Here, a relation $<$ on a type is called *well-founded* if every non-empty subset has a minimal element with respect to $<$.

OrderEmbedding.wellFoundedGT theorem

[WellFoundedGT β] (f : α ↪o β) : WellFoundedGT α

Full source

/-- A preorder which embeds into a preorder in which `(· > ·)` is well-founded
also has `(· > ·)` well-founded. -/
protected theorem wellFoundedGT [WellFoundedGT β] (f : α ↪o β) : WellFoundedGT α :=
  @OrderEmbedding.wellFoundedLT αᵒᵈ _ _ _ _ f.dual

Well-foundedness of strict greater-than relation preserved under order embeddings

Informal description

Let $\alpha$ and $\beta$ be preordered types, and let $f \colon \alpha \hookrightarrow \beta$ be an order embedding. If the strict order relation $>$ on $\beta$ is well-founded, then the strict order relation $>$ on $\alpha$ is also well-founded. Here, a relation $>$ on a type is called *well-founded* if every non-empty subset has a minimal element with respect to $>$.

OrderEmbedding.ofMapLEIff definition

{α β} [PartialOrder α] [Preorder β] (f : α → β) (hf : ∀ a b, f a ≤ f b ↔ a ≤ b) : α ↪o β

Full source

/-- 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`.
-/
def ofMapLEIff {α β} [PartialOrder α] [Preorder β] (f : α → β) (hf : ∀ a b, f a ≤ f b ↔ a ≤ b) :
    α ↪o β :=
  RelEmbedding.ofMapRelIff f hf

Order embedding from a function preserving order iff condition

Informal description

Given a function $f : \alpha \to \beta$ between a partially ordered set $\alpha$ and a preordered set $\beta$, if $f$ satisfies the condition that $f(a) \leq f(b)$ if and only if $a \leq b$ for all $a, b \in \alpha$, then $f$ can be promoted to an order embedding from $\alpha$ to $\beta$.

OrderEmbedding.coe_ofMapLEIff theorem

{α β} [PartialOrder α] [Preorder β] {f : α → β} (h) : ⇑(ofMapLEIff f h) = f

Full source

@[simp]
theorem coe_ofMapLEIff {α β} [PartialOrder α] [Preorder β] {f : α → β} (h) :
    ⇑(ofMapLEIff f h) = f :=
  rfl

Embedding Construction Preserves Function: $\operatorname{ofMapLEIff}(f, h) = f$

Informal description

Given a function $f : \alpha \to \beta$ between a partially ordered set $\alpha$ and a preordered set $\beta$, and a proof $h$ that $f$ satisfies $f(a) \leq f(b) \leftrightarrow a \leq b$ for all $a, b \in \alpha$, the underlying function of the order embedding constructed via `OrderEmbedding.ofMapLEIff` is equal to $f$.

OrderEmbedding.ofStrictMono definition

{α β} [LinearOrder α] [Preorder β] (f : α → β) (h : StrictMono f) : α ↪o β

Full source

/-- A strictly monotone map from a linear order is an order embedding. -/
def ofStrictMono {α β} [LinearOrder α] [Preorder β] (f : α → β) (h : StrictMono f) : α ↪o β :=
  ofMapLEIff f fun _ _ => h.le_iff_le

Order embedding from a strictly monotone function

Informal description

Given a strictly monotone function $f : \alpha \to \beta$ from a linearly ordered type $\alpha$ to a preordered type $\beta$, the function $f$ can be promoted to an order embedding from $\alpha$ to $\beta$. This means that $f$ is injective and preserves the order relation: for any $x, y \in \alpha$, $x \leq y$ if and only if $f(x) \leq f(y)$ in $\beta$.

OrderEmbedding.coe_ofStrictMono theorem

{α β} [LinearOrder α] [Preorder β] {f : α → β} (h : StrictMono f) : ⇑(ofStrictMono f h) = f

Full source

@[simp]
theorem coe_ofStrictMono {α β} [LinearOrder α] [Preorder β] {f : α → β} (h : StrictMono f) :
    ⇑(ofStrictMono f h) = f :=
  rfl

Embedding Construction Preserves Strictly Monotone Function: $\text{ofStrictMono}(f, h) = f$

Informal description

Given a strictly monotone function $f : \alpha \to \beta$ from a linearly ordered type $\alpha$ to a preordered type $\beta$, the underlying function of the order embedding constructed via `OrderEmbedding.ofStrictMono` is equal to $f$ itself. In other words, if $h$ is a proof that $f$ is strictly monotone, then the coercion of $\text{ofStrictMono}(f, h)$ is exactly $f$.

OrderEmbedding.subtype definition

(p : α → Prop) : Subtype p ↪o α

Full source

/-- Embedding of a subtype into the ambient type as an `OrderEmbedding`. -/
def subtype (p : α → Prop) : SubtypeSubtype p ↪o α :=
  ⟨Function.Embedding.subtype p, Iff.rfl⟩

Subtype order embedding

Informal description

The embedding of a subtype $\{x \in \alpha \mid p(x)\}$ into the original type $\alpha$ as an order embedding. This means it is an injective function that preserves and reflects the order relation: for any $x, y$ in the subtype, $x \leq y$ if and only if their images in $\alpha$ satisfy the same inequality.

OrderEmbedding.subtype_apply theorem

{p : α → Prop} (x : Subtype p) : subtype p x = x

Full source

@[simp]
theorem subtype_apply {p : α → Prop} (x : Subtype p) : subtype p x = x :=
  rfl

Identity Property of Subtype Order Embedding

Informal description

For any predicate $p$ on a preordered type $\alpha$ and any element $x$ in the subtype $\{x \in \alpha \mid p(x)\}$, the order embedding $\text{subtype } p$ applied to $x$ equals $x$ itself.

OrderEmbedding.subtype_injective theorem

(p : α → Prop) : Function.Injective (subtype p)

Full source

theorem subtype_injective (p : α → Prop) : Function.Injective (subtype p) :=
  Subtype.coe_injective

Injectivity of Subtype Order Embedding

Informal description

For any predicate $p$ on a preordered type $\alpha$, the order embedding $\text{subtype } p : \{x \in \alpha \mid p(x)\} \hookrightarrow \alpha$ is injective. That is, for any $x, y$ in the subtype, if $\text{subtype } p(x) = \text{subtype } p(y)$, then $x = y$.

OrderEmbedding.coe_subtype theorem

(p : α → Prop) : ⇑(subtype p) = Subtype.val

Full source

@[simp]
theorem coe_subtype (p : α → Prop) : ⇑(subtype p) = Subtype.val :=
  rfl

Subtype Order Embedding Coincides with Subtype Projection

Informal description

For any predicate $p$ on a preordered type $\alpha$, the underlying function of the order embedding $\text{subtype } p : \{x \in \alpha \mid p(x)\} \hookrightarrow \alpha$ is equal to the standard subtype projection function $\text{Subtype.val}$.

OrderEmbedding.toOrderHom definition

{X Y : Type*} [Preorder X] [Preorder Y] (f : X ↪o Y) : X →o Y

Full source

/-- Convert an `OrderEmbedding` to an `OrderHom`. -/
@[simps -fullyApplied]
def toOrderHom {X Y : Type*} [Preorder X] [Preorder Y] (f : X ↪o Y) : X →o Y where
  toFun := f
  monotone' := f.monotone

Conversion from order embedding to order homomorphism

Informal description

Given an order embedding $f \colon X \hookrightarrow Y$ between preordered types $X$ and $Y$, this function converts $f$ into an order homomorphism (monotone function) $X \to Y$ by using the underlying function of $f$ and its monotonicity property.

OrderEmbedding.ofIsEmpty definition

[IsEmpty α] : α ↪o β

Full source

/-- The trivial embedding from an empty preorder to another preorder -/
@[simps] def ofIsEmpty [IsEmpty α] : α ↪o β where
  toFun := isEmptyElim
  inj' := isEmptyElim
  map_rel_iff' {a} := isEmptyElim a

Trivial order embedding from an empty type

Informal description

The trivial order embedding from an empty preordered type $\alpha$ to another preordered type $\beta$, which is well-defined since there are no elements in $\alpha$ to map.

OrderEmbedding.coe_ofIsEmpty theorem

[IsEmpty α] : (ofIsEmpty : α ↪o β) = (isEmptyElim : α → β)

Full source

@[simp, norm_cast]
lemma coe_ofIsEmpty [IsEmpty α] : (ofIsEmpty : α ↪o β) = (isEmptyElim : α → β) := rfl

Trivial Order Embedding from Empty Type Equals Empty Elimination Function

Informal description

For an empty preordered type $\alpha$ and any preordered type $\beta$, the trivial order embedding `ofIsEmpty : α ↪o β` is equal to the function `isEmptyElim : α → β` that eliminates the empty type.

Disjoint.of_orderEmbedding theorem

[OrderBot α] [OrderBot β] {a₁ a₂ : α} : Disjoint (f a₁) (f a₂) → Disjoint a₁ a₂

Full source

/-- If the images by an order embedding of two elements are disjoint,
then they are themselves disjoint. -/
lemma Disjoint.of_orderEmbedding [OrderBot α] [OrderBot β] {a₁ a₂ : α} :
    Disjoint (f a₁) (f a₂) → Disjoint a₁ a₂ := by
  intro h x h₁ h₂
  rw [← f.le_iff_le] at h₁ h₂ ⊢
  calc
    f x ≤ ⊥ := h h₁ h₂
    _ ≤ f ⊥ := bot_le

Order Embedding Preserves Disjointness of Elements

Informal description

Let $\alpha$ and $\beta$ be preordered types with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively. Given an order embedding $f \colon \alpha \hookrightarrow \beta$ and elements $a_1, a_2 \in \alpha$, if the images $f(a_1)$ and $f(a_2)$ are disjoint in $\beta$ (i.e., $f(a_1) \sqcap f(a_2) = \bot_\beta$), then $a_1$ and $a_2$ are disjoint in $\alpha$ (i.e., $a_1 \sqcap a_2 = \bot_\alpha$).

Codisjoint.of_orderEmbedding theorem

[OrderTop α] [OrderTop β] {a₁ a₂ : α} : Codisjoint (f a₁) (f a₂) → Codisjoint a₁ a₂

Full source

/-- If the images by an order embedding of two elements are codisjoint,
then they are themselves codisjoint. -/
lemma Codisjoint.of_orderEmbedding [OrderTop α] [OrderTop β] {a₁ a₂ : α} :
    Codisjoint (f a₁) (f a₂) → Codisjoint a₁ a₂ :=
  Disjoint.of_orderEmbedding (α := αᵒᵈ) (β := βᵒᵈ) f.dual

Order Embedding Preserves Codisjointness of Elements

Informal description

Let $\alpha$ and $\beta$ be preordered types with top elements $\top_\alpha$ and $\top_\beta$ respectively. Given an order embedding $f \colon \alpha \hookrightarrow \beta$ and elements $a_1, a_2 \in \alpha$, if the images $f(a_1)$ and $f(a_2)$ are codisjoint in $\beta$ (i.e., $f(a_1) \sqcup f(a_2) = \top_\beta$), then $a_1$ and $a_2$ are codisjoint in $\alpha$ (i.e., $a_1 \sqcup a_2 = \top_\alpha$).

IsCompl.of_orderEmbedding theorem

[BoundedOrder α] [BoundedOrder β] {a₁ a₂ : α} : IsCompl (f a₁) (f a₂) → IsCompl a₁ a₂

Full source

/-- If the images by an order embedding of two elements are complements,
then they are themselves complements. -/
lemma IsCompl.of_orderEmbedding [BoundedOrder α] [BoundedOrder β] {a₁ a₂ : α} :
    IsCompl (f a₁) (f a₂) → IsCompl a₁ a₂ := fun ⟨hd, hcd⟩ ↦
  ⟨Disjoint.of_orderEmbedding f hd, Codisjoint.of_orderEmbedding f hcd⟩

Order Embedding Preserves Complementarity of Elements

Informal description

Let $\alpha$ and $\beta$ be bounded orders with top and bottom elements. Given an order embedding $f \colon \alpha \hookrightarrow \beta$ and elements $a_1, a_2 \in \alpha$, if the images $f(a_1)$ and $f(a_2)$ are complements in $\beta$ (i.e., they are disjoint and codisjoint), then $a_1$ and $a_2$ are complements in $\alpha$.

RelHom.toOrderHom definition

: α →o β

Full source

/-- A bundled expression of the fact that a map between partial orders that is strictly monotone
is weakly monotone. -/
@[simps -fullyApplied]
def toOrderHom : α →o β where
  toFun := f
  monotone' := StrictMono.monotone fun _ _ => f.map_rel

Conversion from relation homomorphism to order homomorphism

Informal description

Given a relation homomorphism $ f $ between strict orders $ (<) $ on $ \alpha $ and $ \beta $, this definition converts $ f $ into an order homomorphism (monotone function) between the corresponding preorders. Specifically, the function $ f $ is used as the underlying map, and the proof that $ f $ is monotone follows from the fact that $ f $ preserves the strict order relation.

RelEmbedding.toOrderHom_injective theorem

 (f : ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop)) :
  Function.Injective (f : ((· < ·) : α → α → Prop) →r ((· < ·) : β → β → Prop)).toOrderHom

Full source

theorem RelEmbedding.toOrderHom_injective
    (f : ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop)) :
    Function.Injective (f : ((· < ·) : α → α → Prop) →r ((· < ·) : β → β → Prop)).toOrderHom :=
  fun _ _ h => f.injective h

Injectivity of the Induced Order Homomorphism from a Relation Embedding

Informal description

Let $\alpha$ and $\beta$ be types equipped with strict order relations $<$ and $<$ respectively. Given a relation embedding $f : (\alpha, <) \hookrightarrow (\beta, <)$, the induced order homomorphism obtained by converting $f$ to a relation homomorphism and then to an order homomorphism is injective. In other words, the function $(f : (\alpha, <) \to_r (\beta, <)).toOrderHom$ is injective.

OrderIso.instEquivLike instance

: EquivLike (α ≃o β) α β

Full source

instance : EquivLike (α ≃o β) α β where
  coe f := f.toFun
  inv f := f.invFun
  left_inv f := f.left_inv
  right_inv f := f.right_inv
  coe_injective' f g h₁ h₂ := by
    obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

Equivalence-like Structure for Order Isomorphisms

Informal description

The type of order isomorphisms $\alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$ forms an equivalence-like class, where each isomorphism can be injectively coerced to a bijection between $\alpha$ and $\beta$.

OrderIso.instOrderIsoClass instance

: OrderIsoClass (α ≃o β) α β

Full source

instance : OrderIsoClass (α ≃o β) α β where
  map_le_map_iff f _ _ := f.map_rel_iff'

Order Isomorphism Class for Order Isomorphisms

Informal description

The type of order isomorphisms $\alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$ forms an order isomorphism class, meaning it satisfies the properties of an order isomorphism: each element is a bijective function that preserves and reflects the order relation.

OrderIso.toFun_eq_coe theorem

{f : α ≃o β} : f.toFun = f

Full source

@[simp]
theorem toFun_eq_coe {f : α ≃o β} : f.toFun = f :=
  rfl

Underlying Function of Order Isomorphism Equals Coercion

Informal description

For any order isomorphism $f : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the underlying function $f.\text{toFun}$ is equal to $f$ itself when viewed as a function.

OrderIso.ext theorem

{f g : α ≃o β} (h : (f : α → β) = g) : f = g

Full source

@[ext]
theorem ext {f g : α ≃o β} (h : (f : α → β) = g) : f = g :=
  DFunLike.coe_injective h

Extensionality of Order Isomorphisms

Informal description

For any two order isomorphisms $f, g : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, if the underlying functions $f$ and $g$ are equal (i.e., $f(x) = g(x)$ for all $x \in \alpha$), then $f = g$ as order isomorphisms.

OrderIso.toOrderEmbedding definition

(e : α ≃o β) : α ↪o β

Full source

/-- Reinterpret an order isomorphism as an order embedding. -/
def toOrderEmbedding (e : α ≃o β) : α ↪o β :=
  e.toRelEmbedding

Conversion from order isomorphism to order embedding

Informal description

Given an order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the function converts $e$ into an order embedding $e : \alpha \hookrightarrow_o \beta$ by extracting the underlying embedding from the isomorphism, preserving the order relation in both directions.

OrderIso.coe_toOrderEmbedding theorem

(e : α ≃o β) : ⇑e.toOrderEmbedding = e

Full source

@[simp]
theorem coe_toOrderEmbedding (e : α ≃o β) : ⇑e.toOrderEmbedding = e :=
  rfl

Equality of Order Isomorphism and its Embedding's Function

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the underlying function of the order embedding obtained from $e$ is equal to $e$ itself. That is, if we convert $e$ to an order embedding and then consider it as a function, we recover the original function $e$.

OrderIso.bijective theorem

(e : α ≃o β) : Function.Bijective e

Full source

protected theorem bijective (e : α ≃o β) : Function.Bijective e :=
  e.toEquiv.bijective

Bijectivity of Order Isomorphisms

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the function $e : \alpha \to \beta$ is bijective. That is, $e$ is both injective (for any $x, y \in \alpha$, $e(x) = e(y)$ implies $x = y$) and surjective (for every $y \in \beta$, there exists an $x \in \alpha$ such that $e(x) = y$).

OrderIso.injective theorem

(e : α ≃o β) : Function.Injective e

Full source

protected theorem injective (e : α ≃o β) : Function.Injective e :=
  e.toEquiv.injective

Injectivity of Order Isomorphisms

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the function $e : \alpha \to \beta$ is injective. That is, for any $x, y \in \alpha$, if $e(x) = e(y)$, then $x = y$.

OrderIso.surjective theorem

(e : α ≃o β) : Function.Surjective e

Full source

protected theorem surjective (e : α ≃o β) : Function.Surjective e :=
  e.toEquiv.surjective

Surjectivity of Order Isomorphisms

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the function $e : \alpha \to \beta$ is surjective.

OrderIso.apply_eq_iff_eq theorem

(e : α ≃o β) {x y : α} : e x = e y ↔ x = y

Full source

theorem apply_eq_iff_eq (e : α ≃o β) {x y : α} : e x = e y ↔ x = y :=
  e.toEquiv.apply_eq_iff_eq

Order Isomorphism Preserves Equality: $e(x) = e(y) \leftrightarrow x = y$

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any elements $x, y \in \alpha$, we have $e(x) = e(y)$ if and only if $x = y$.

OrderIso.refl definition

(α : Type*) [LE α] : α ≃o α

Full source

/-- Identity order isomorphism. -/
def refl (α : Type*) [LE α] : α ≃o α :=
  RelIso.refl (· ≤ ·)

Identity order isomorphism

Informal description

The identity order isomorphism on a preordered type $\alpha$ is the bijective function $\text{id} : \alpha \to \alpha$ that preserves the order relation in both directions, i.e., for any $x, y \in \alpha$, we have $x \leq y$ if and only if $\text{id}(x) \leq \text{id}(y)$.

OrderIso.coe_refl theorem

: ⇑(refl α) = id

Full source

@[simp]
theorem coe_refl : ⇑(refl α) = id :=
  rfl

Identity Order Isomorphism as Identity Function

Informal description

The underlying function of the identity order isomorphism $\text{refl}(\alpha)$ is equal to the identity function $\text{id}$ on $\alpha$.

OrderIso.refl_apply theorem

(x : α) : refl α x = x

Full source

@[simp]
theorem refl_apply (x : α) : refl α x = x :=
  rfl

Identity Order Isomorphism Evaluation: $\text{refl}(\alpha)(x) = x$

Informal description

For any element $x$ in a preordered type $\alpha$, the identity order isomorphism $\text{refl}(\alpha)$ evaluated at $x$ equals $x$, i.e., $\text{refl}(\alpha)(x) = x$.

OrderIso.refl_toEquiv theorem

: (refl α).toEquiv = Equiv.refl α

Full source

@[simp]
theorem refl_toEquiv : (refl α).toEquiv = Equiv.refl α :=
  rfl

Identity Order Isomorphism's Underlying Equivalence is Identity

Informal description

For any preordered type $\alpha$, the underlying equivalence of the identity order isomorphism $\text{refl}(\alpha)$ is equal to the identity equivalence $\text{Equiv.refl}(\alpha)$.

OrderIso.symm definition

(e : α ≃o β) : β ≃o α

Full source

/-- Inverse of an order isomorphism. -/
def symm (e : α ≃o β) : β ≃o α := RelIso.symm e

Inverse of an order isomorphism

Informal description

Given an order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the inverse function $e^{-1} : \beta \to \alpha$ is also an order isomorphism from $\beta$ to $\alpha$, preserving the order relation in both directions.

OrderIso.apply_symm_apply theorem

(e : α ≃o β) (x : β) : e (e.symm x) = x

Full source

@[simp]
theorem apply_symm_apply (e : α ≃o β) (x : β) : e (e.symm x) = x :=
  e.toEquiv.apply_symm_apply x

Order Isomorphism Recovery: $e(e^{-1}(x)) = x$

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ and any element $x \in \beta$, applying $e$ to the inverse image $e^{-1}(x)$ recovers the original element $x$, i.e., $e(e^{-1}(x)) = x$.

OrderIso.symm_apply_apply theorem

(e : α ≃o β) (x : α) : e.symm (e x) = x

Full source

@[simp]
theorem symm_apply_apply (e : α ≃o β) (x : α) : e.symm (e x) = x :=
  e.toEquiv.symm_apply_apply x

Inverse Order Isomorphism Recovers Original Element: $e^{-1}(e(x)) = x$

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any element $x \in \alpha$, applying the inverse isomorphism $e^{-1}$ to the image $e(x)$ recovers the original element $x$, i.e., $e^{-1}(e(x)) = x$.

OrderIso.symm_refl theorem

(α : Type*) [LE α] : (refl α).symm = refl α

Full source

@[simp]
theorem symm_refl (α : Type*) [LE α] : (refl α).symm = refl α :=
  rfl

Inverse of Identity Order Isomorphism is Identity

Informal description

For any preordered type $\alpha$, the inverse of the identity order isomorphism on $\alpha$ is equal to the identity order isomorphism itself, i.e., $(\text{refl}_{\alpha})^{-1} = \text{refl}_{\alpha}$.

OrderIso.apply_eq_iff_eq_symm_apply theorem

(e : α ≃o β) (x : α) (y : β) : e x = y ↔ x = e.symm y

Full source

theorem apply_eq_iff_eq_symm_apply (e : α ≃o β) (x : α) (y : β) : e x = y ↔ x = e.symm y :=
  e.toEquiv.apply_eq_iff_eq_symm_apply

Order Isomorphism Characterization: $e(x) = y \leftrightarrow x = e^{-1}(y)$

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any elements $x \in \alpha$ and $y \in \beta$, the equality $e(x) = y$ holds if and only if $x = e^{-1}(y)$.

OrderIso.symm_apply_eq theorem

(e : α ≃o β) {x : α} {y : β} : e.symm y = x ↔ y = e x

Full source

theorem symm_apply_eq (e : α ≃o β) {x : α} {y : β} : e.symm y = x ↔ y = e x :=
  e.toEquiv.symm_apply_eq

Characterization of Inverse Order Isomorphism: $e^{-1}(y) = x \leftrightarrow y = e(x)$

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any elements $x \in \alpha$ and $y \in \beta$, the equality $e^{-1}(y) = x$ holds if and only if $y = e(x)$.

OrderIso.symm_symm theorem

(e : α ≃o β) : e.symm.symm = e

Full source

@[simp]
theorem symm_symm (e : α ≃o β) : e.symm.symm = e := rfl

Double Inverse of Order Isomorphism Equals Original

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the double inverse of $e$ is equal to $e$ itself, i.e., $(e^{-1})^{-1} = e$.

OrderIso.symm_bijective theorem

: Function.Bijective (OrderIso.symm : (α ≃o β) → β ≃o α)

Full source

theorem symm_bijective : Function.Bijective (OrderIso.symm : (α ≃o β) → β ≃o α) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Operation on Order Isomorphisms

Informal description

The function that maps an order isomorphism $e : \alpha \simeq_o \beta$ to its inverse $e^{-1} : \beta \simeq_o \alpha$ is bijective. That is, the inverse operation on order isomorphisms is both injective and surjective.

OrderIso.symm_injective theorem

: Function.Injective (symm : α ≃o β → β ≃o α)

Full source

theorem symm_injective : Function.Injective (symm : α ≃o β → β ≃o α) :=
  symm_bijective.injective

Injectivity of the Inverse Operation on Order Isomorphisms

Informal description

The function that maps an order isomorphism $e : \alpha \simeq_o \beta$ to its inverse $e^{-1} : \beta \simeq_o \alpha$ is injective. That is, if two order isomorphisms have the same inverse, then they must be equal.

OrderIso.toEquiv_symm theorem

(e : α ≃o β) : e.toEquiv.symm = e.symm.toEquiv

Full source

@[simp]
theorem toEquiv_symm (e : α ≃o β) : e.toEquiv.symm = e.symm.toEquiv :=
  rfl

Equivalence of Inverse Order Isomorphism

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the underlying equivalence's inverse $e^{-1} : \beta \simeq \alpha$ is equal to the equivalence obtained from the inverse order isomorphism $e^{-1} : \beta \simeq_o \alpha$.

OrderIso.trans definition

(e : α ≃o β) (e' : β ≃o γ) : α ≃o γ

Full source

/-- Composition of two order isomorphisms is an order isomorphism. -/
@[trans]
def trans (e : α ≃o β) (e' : β ≃o γ) : α ≃o γ :=
  RelIso.trans e e'

Composition of order isomorphisms

Informal description

Given two order isomorphisms $e : \alpha \simeq_o \beta$ and $e' : \beta \simeq_o \gamma$, their composition $e' \circ e$ forms an order isomorphism between $\alpha$ and $\gamma$. This means that for any $x, y \in \alpha$, we have $x \leq y$ if and only if $(e' \circ e)(x) \leq (e' \circ e)(y)$.

OrderIso.coe_trans theorem

(e : α ≃o β) (e' : β ≃o γ) : ⇑(e.trans e') = e' ∘ e

Full source

@[simp]
theorem coe_trans (e : α ≃o β) (e' : β ≃o γ) : ⇑(e.trans e') = e' ∘ e :=
  rfl

Composition of Order Isomorphisms Preserves Function Composition

Informal description

For any two order isomorphisms $e : \alpha \simeq_o \beta$ and $e' : \beta \simeq_o \gamma$, the underlying function of their composition $e \circ e'$ is equal to the composition of their underlying functions, i.e., $(e \circ e') = e' \circ e$.

OrderIso.trans_apply theorem

(e : α ≃o β) (e' : β ≃o γ) (x : α) : e.trans e' x = e' (e x)

Full source

@[simp]
theorem trans_apply (e : α ≃o β) (e' : β ≃o γ) (x : α) : e.trans e' x = e' (e x) :=
  rfl

Composition of Order Isomorphisms: $(e' \circ e)(x) = e'(e(x))$

Informal description

Given two order isomorphisms $e : \alpha \simeq_o \beta$ and $e' : \beta \simeq_o \gamma$, and an element $x \in \alpha$, the application of the composed isomorphism $e' \circ e$ to $x$ is equal to the application of $e'$ to the application of $e$ to $x$, i.e., $(e' \circ e)(x) = e'(e(x))$.

OrderIso.refl_trans theorem

(e : α ≃o β) : (refl α).trans e = e

Full source

@[simp]
theorem refl_trans (e : α ≃o β) : (refl α).trans e = e := by
  ext x
  rfl

Identity Order Isomorphism is Left Neutral for Composition

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$, the composition of the identity order isomorphism on $\alpha$ with $e$ is equal to $e$ itself, i.e., $(\text{refl } \alpha) \circ e = e$.

OrderIso.trans_refl theorem

(e : α ≃o β) : e.trans (refl β) = e

Full source

@[simp]
theorem trans_refl (e : α ≃o β) : e.trans (refl β) = e := by
  ext x
  rfl

Right Identity Law for Order Isomorphism Composition

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$, the composition of $e$ with the identity order isomorphism on $\beta$ is equal to $e$ itself, i.e., $e \circ \text{id}_\beta = e$.

OrderIso.symm_trans_apply theorem

(e₁ : α ≃o β) (e₂ : β ≃o γ) (c : γ) : (e₁.trans e₂).symm c = e₁.symm (e₂.symm c)

Full source

@[simp]
theorem symm_trans_apply (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : γ) :
    (e₁.trans e₂).symm c = e₁.symm (e₂.symm c) :=
  rfl

Inverse of Composition of Order Isomorphisms

Informal description

Let $e₁ : \alpha \simeq_o \beta$ and $e₂ : \beta \simeq_o \gamma$ be order isomorphisms between preordered types. For any element $c \in \gamma$, the inverse of the composition $e₁ \circ e₂$ evaluated at $c$ equals the composition of the inverses $e₁^{-1} \circ e₂^{-1}$ evaluated at $c$, i.e., $$(e₁ \circ e₂)^{-1}(c) = e₁^{-1}(e₂^{-1}(c)).$$

OrderIso.symm_trans theorem

(e₁ : α ≃o β) (e₂ : β ≃o γ) : (e₁.trans e₂).symm = e₂.symm.trans e₁.symm

Full source

theorem symm_trans (e₁ : α ≃o β) (e₂ : β ≃o γ) : (e₁.trans e₂).symm = e₂.symm.trans e₁.symm :=
  rfl

Inverse of Composition of Order Isomorphisms Equals Reverse Composition of Inverses

Informal description

Given two order isomorphisms $e₁ : α ≃ₒ β$ and $e₂ : β ≃ₒ γ$, the inverse of their composition $(e₁ \circ e₂)^{-1}$ is equal to the composition of their inverses in reverse order, $e₂^{-1} \circ e₁^{-1}$.

OrderIso.self_trans_symm theorem

(e : α ≃o β) : e.trans e.symm = OrderIso.refl α

Full source

@[simp]
theorem self_trans_symm (e : α ≃o β) : e.trans e.symm = OrderIso.refl α :=
  RelIso.self_trans_symm e

Composition of Order Isomorphism with Its Inverse Yields Identity

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity order isomorphism on $\alpha$, i.e., $e \circ e^{-1} = \text{id}_\alpha$.

OrderIso.symm_trans_self theorem

(e : α ≃o β) : e.symm.trans e = OrderIso.refl β

Full source

@[simp]
theorem symm_trans_self (e : α ≃o β) : e.symm.trans e = OrderIso.refl β :=
  RelIso.symm_trans_self e

Inverse Composition Yields Identity Order Isomorphism: $e^{-1} \circ e = \text{id}_\beta$

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the composition of its inverse $e^{-1}$ with $e$ is equal to the identity order isomorphism on $\beta$, i.e., $e^{-1} \circ e = \text{id}_\beta$.

OrderIso.arrowCongr definition

 {α β γ δ} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (f : α ≃o γ) (g : β ≃o δ) : (α →o β) ≃o (γ →o δ)

Full source

/-- An order isomorphism between the domains and codomains of two prosets of
order homomorphisms gives an order isomorphism between the two function prosets. -/
@[simps apply symm_apply]
def arrowCongr {α β γ δ} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ]
    (f : α ≃o γ) (g : β ≃o δ) : (α →o β) ≃o (γ →o δ) where
  toFun  p := .comp g <| .comp p f.symm
  invFun p := .comp g.symm <| .comp p f
  left_inv p := DFunLike.coe_injective <| by
    change (g.symm ∘ g) ∘ p ∘ (f.symm ∘ f) = p
    simp only [← DFunLike.coe_eq_coe_fn, ← OrderIso.coe_trans, Function.id_comp,
               OrderIso.self_trans_symm, OrderIso.coe_refl, Function.comp_id]
  right_inv p := DFunLike.coe_injective <| by
    change (g ∘ g.symm) ∘ p ∘ (f ∘ f.symm) = p
    simp only [← DFunLike.coe_eq_coe_fn, ← OrderIso.coe_trans, Function.id_comp,
               OrderIso.symm_trans_self, OrderIso.coe_refl, Function.comp_id]
  map_rel_iff' {p q} := by
    simp only [Equiv.coe_fn_mk, OrderHom.le_def, OrderHom.comp_coe,
               OrderHomClass.coe_coe, Function.comp_apply, map_le_map_iff]
    exact Iff.symm f.forall_congr_left

Order isomorphism between function spaces induced by domain and codomain isomorphisms

Informal description

Given order isomorphisms $f : \alpha \simeq_o \gamma$ and $g : \beta \simeq_o \delta$ between preordered types, the function `OrderIso.arrowCongr` constructs an order isomorphism $(α →o β) \simeq_o (γ →o δ)$ between the function spaces of order homomorphisms. Specifically, it maps an order homomorphism $p : α →o β$ to the composition $g \circ p \circ f^{-1} : γ →o δ$, and its inverse maps $q : γ →o δ$ to $g^{-1} \circ q \circ f : α →o β$.

OrderIso.conj definition

{α β} [Preorder α] [Preorder β] (f : α ≃o β) : (α →o α) ≃ (β →o β)

Full source

/-- If `α` and `β` are order-isomorphic then the two orders of order-homomorphisms
from `α` and `β` to themselves are order-isomorphic. -/
@[simps! apply symm_apply]
def conj {α β} [Preorder α] [Preorder β] (f : α ≃o β) : (α →o α) ≃ (β →o β) :=
  arrowCongr f f

Conjugation of order homomorphisms by an order isomorphism

Informal description

Given an order isomorphism $f : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the function `OrderIso.conj` constructs a bijection between the spaces of order homomorphisms $\alpha \to_o \alpha$ and $\beta \to_o \beta$. Specifically, it maps an order homomorphism $p : \alpha \to_o \alpha$ to the composition $f \circ p \circ f^{-1} : \beta \to_o \beta$, and its inverse maps $q : \beta \to_o \beta$ to $f^{-1} \circ q \circ f : \alpha \to_o \alpha$.

OrderIso.prodComm definition

: α × β ≃o β × α

Full source

/-- `Prod.swap` as an `OrderIso`. -/
def prodComm : α × βα × β ≃o β × α where
  toEquiv := Equiv.prodComm α β
  map_rel_iff' := Prod.swap_le_swap

Order isomorphism of product commutativity

Informal description

The function `OrderIso.prodComm` is an order isomorphism between the product types $\alpha \times \beta$ and $\beta \times \alpha$, where the order is preserved under swapping the components of the pairs. Specifically, for any $(a, b) \in \alpha \times \beta$ and $(c, d) \in \beta \times \alpha$, we have $(a, b) \leq (c, d)$ if and only if $(b, a) \leq (d, c)$.

OrderIso.coe_prodComm theorem

: ⇑(prodComm : α × β ≃o β × α) = Prod.swap

Full source

@[simp]
theorem coe_prodComm : ⇑(prodComm : α × βα × β ≃o β × α) = Prod.swap :=
  rfl

Underlying Function of Product Commutativity Order Isomorphism is Swap

Informal description

The underlying function of the order isomorphism `prodComm` between $\alpha \times \beta$ and $\beta \times \alpha$ is equal to the product swap function, i.e., for any $(a, b) \in \alpha \times \beta$, we have $\text{prodComm}(a, b) = (b, a)$.

OrderIso.prodComm_symm theorem

: (prodComm : α × β ≃o β × α).symm = prodComm

Full source

@[simp]
theorem prodComm_symm : (prodComm : α × βα × β ≃o β × α).symm = prodComm :=
  rfl

Inverse of Product Commutativity Order Isomorphism is Itself

Informal description

The inverse of the order isomorphism `prodComm` from $\alpha \times \beta$ to $\beta \times \alpha$ is equal to `prodComm` itself, i.e., $(\text{prodComm})^{-1} = \text{prodComm}$.

OrderIso.dualDual definition

: α ≃o αᵒᵈᵒᵈ

Full source

/-- The order isomorphism between a type and its double dual. -/
def dualDual : α ≃o αᵒᵈᵒᵈ :=
  refl α

Order isomorphism between a type and its double dual

Informal description

The order isomorphism between a type $\alpha$ and its double dual $\alpha^{\text{op}\text{op}}$, which is the identity map equipped with the proof that it preserves the order relation in both directions.

OrderIso.coe_dualDual theorem

: ⇑(dualDual α) = toDual ∘ toDual

Full source

@[simp]
theorem coe_dualDual : ⇑(dualDual α) = toDualtoDual ∘ toDual :=
  rfl

Function Representation of Double Dual Order Isomorphism

Informal description

The underlying function of the order isomorphism `dualDual` from a type $\alpha$ to its double dual $\alpha^{\text{op}\text{op}}$ is equal to the composition of the `toDual` function applied twice, i.e., $\text{dualDual} = \text{toDual} \circ \text{toDual}$.

OrderIso.coe_dualDual_symm theorem

: ⇑(dualDual α).symm = ofDual ∘ ofDual

Full source

@[simp]
theorem coe_dualDual_symm : ⇑(dualDual α).symm = ofDualofDual ∘ ofDual :=
  rfl

Inverse of Double Dual Order Isomorphism as Composition of `ofDual` Functions

Informal description

The underlying function of the inverse of the order isomorphism `dualDual α` is equal to the composition of the two `ofDual` functions, i.e., $(\text{dualDual } \alpha)^{-1} = \text{ofDual} \circ \text{ofDual}$.

OrderIso.dualDual_apply theorem

(a : α) : dualDual α a = toDual (toDual a)

Full source

@[simp]
theorem dualDual_apply (a : α) : dualDual α a = toDual (toDual a) :=
  rfl

Double Dual Order Isomorphism Maps Element to Double Dual

Informal description

For any element $a$ of a preordered type $\alpha$, the order isomorphism $\alpha \simeq_o \alpha^{\text{op}\text{op}}$ maps $a$ to the double dual of $a$, i.e., $\text{dualDual}(\alpha)(a) = \text{toDual}(\text{toDual}(a))$.

OrderIso.dualDual_symm_apply theorem

(a : αᵒᵈᵒᵈ) : (dualDual α).symm a = ofDual (ofDual a)

Full source

@[simp]
theorem dualDual_symm_apply (a : αᵒᵈαᵒᵈᵒᵈ) : (dualDual α).symm a = ofDual (ofDual a) :=
  rfl

Inverse of Double Dual Order Isomorphism Applied to Element

Informal description

For any element $a$ in the double dual order $\alpha^{\text{op}\text{op}}$, the inverse of the order isomorphism $\text{dualDual} : \alpha \simeq \alpha^{\text{op}\text{op}}$ evaluated at $a$ is equal to applying the "ofDual" operation twice to $a$, i.e., $(\text{dualDual} \ \alpha)^{-1}(a) = \text{ofDual}(\text{ofDual}(a))$.

OrderIso.le_iff_le theorem

(e : α ≃o β) {x y : α} : e x ≤ e y ↔ x ≤ y

Full source

theorem le_iff_le (e : α ≃o β) {x y : α} : e x ≤ e y ↔ x ≤ y :=
  e.map_rel_iff

Order Isomorphism Preserves Order Relation: $e(x) \leq e(y) \leftrightarrow x \leq y$

Informal description

For any order isomorphism $e : \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any elements $x, y \in \alpha$, we have $e(x) \leq e(y)$ if and only if $x \leq y$.

OrderIso.le_symm_apply theorem

(e : α ≃o β) {x : α} {y : β} : x ≤ e.symm y ↔ e x ≤ y

Full source

theorem le_symm_apply (e : α ≃o β) {x : α} {y : β} : x ≤ e.symm y ↔ e x ≤ y :=
  e.rel_symm_apply

Order Isomorphism Characterization via Inverse: $x \leq e^{-1}(y) \leftrightarrow e(x) \leq y$

Informal description

For any order isomorphism $e \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any $x \in \alpha$ and $y \in \beta$, we have $x \leq e^{-1}(y)$ if and only if $e(x) \leq y$.

OrderIso.symm_apply_le theorem

(e : α ≃o β) {x : α} {y : β} : e.symm y ≤ x ↔ y ≤ e x

Full source

theorem symm_apply_le (e : α ≃o β) {x : α} {y : β} : e.symm y ≤ x ↔ y ≤ e x :=
  e.symm_apply_rel

Order Isomorphism Inverse Inequality: $e^{-1}(y) \leq x \leftrightarrow y \leq e(x)$

Informal description

For any order isomorphism $e \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any elements $x \in \alpha$ and $y \in \beta$, the inequality $e^{-1}(y) \leq x$ holds if and only if $y \leq e(x)$.

OrderIso.monotone theorem

(e : α ≃o β) : Monotone e

Full source

protected theorem monotone (e : α ≃o β) : Monotone e :=
  e.toOrderEmbedding.monotone

Monotonicity of Order Isomorphisms

Informal description

For any order isomorphism $e \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the function $e$ is monotone. That is, for any $x, y \in \alpha$, if $x \leq y$, then $e(x) \leq e(y)$.

OrderIso.strictMono theorem

(e : α ≃o β) : StrictMono e

Full source

protected theorem strictMono (e : α ≃o β) : StrictMono e :=
  e.toOrderEmbedding.strictMono

Order Isomorphisms are Strictly Monotone

Informal description

For any order isomorphism $e \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the function $e$ is strictly monotone, meaning that for any $x, y \in \alpha$, if $x < y$ then $e(x) < e(y)$.

OrderIso.lt_iff_lt theorem

(e : α ≃o β) {x y : α} : e x < e y ↔ x < y

Full source

@[simp]
theorem lt_iff_lt (e : α ≃o β) {x y : α} : e x < e y ↔ x < y :=
  e.toOrderEmbedding.lt_iff_lt

Order Isomorphism Preserves Strict Order Relation ($e(x) < e(y) \leftrightarrow x < y$)

Informal description

For any order isomorphism $e \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any elements $x, y \in \alpha$, we have $e(x) < e(y)$ in $\beta$ if and only if $x < y$ in $\alpha$.

OrderIso.lt_symm_apply theorem

(e : α ≃o β) {x : α} {y : β} : x < e.symm y ↔ e x < y

Full source

theorem lt_symm_apply (e : α ≃o β) {x : α} {y : β} : x < e.symm y ↔ e x < y := by
  rw [← e.lt_iff_lt, e.apply_symm_apply]

Order Isomorphism and Inverse Preserve Strict Order: $x < e^{-1}(y) \leftrightarrow e(x) < y$

Informal description

For any order isomorphism $e \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any elements $x \in \alpha$ and $y \in \beta$, we have $x < e^{-1}(y)$ if and only if $e(x) < y$.

OrderIso.symm_apply_lt theorem

(e : α ≃o β) {x : α} {y : β} : e.symm y < x ↔ y < e x

Full source

theorem symm_apply_lt (e : α ≃o β) {x : α} {y : β} : e.symm y < x ↔ y < e x := by
  rw [← e.lt_iff_lt, e.apply_symm_apply]

Order Isomorphism Preserves Strict Order Under Inverse ($e^{-1}(y) < x \leftrightarrow y < e(x)$)

Informal description

For any order isomorphism $e \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any elements $x \in \alpha$ and $y \in \beta$, the inverse image $e^{-1}(y)$ is less than $x$ in $\alpha$ if and only if $y$ is less than $e(x)$ in $\beta$. In other words, $e^{-1}(y) < x \leftrightarrow y < e(x)$.

OrderIso.toRelIsoLT definition

(e : α ≃o β) : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)

Full source

/-- Converts an `OrderIso` into a `RelIso (<) (<)`. -/
def toRelIsoLT (e : α ≃o β) : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop) :=
  ⟨e.toEquiv, lt_iff_lt e⟩

Conversion of Order Isomorphism to Strict Order Relation Isomorphism

Informal description

Given an order isomorphism $e \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the function converts $e$ into a relation isomorphism between the strict order relations $(<)$ on $\alpha$ and $(<)$ on $\beta$. Specifically, for any $x, y \in \alpha$, we have $x < y$ if and only if $e(x) < e(y)$.

OrderIso.toRelIsoLT_apply theorem

(e : α ≃o β) (x : α) : e.toRelIsoLT x = e x

Full source

@[simp]
theorem toRelIsoLT_apply (e : α ≃o β) (x : α) : e.toRelIsoLT x = e x :=
  rfl

Application of Order Isomorphism to Strict Order Relation Isomorphism ($e.\text{toRelIsoLT}(x) = e(x)$)

Informal description

For any order isomorphism $e \colon \alpha \simeq_o \beta$ and any element $x \in \alpha$, the application of the converted strict order relation isomorphism $e.\text{toRelIsoLT}$ at $x$ equals $e(x)$.

OrderIso.toRelIsoLT_symm theorem

(e : α ≃o β) : e.toRelIsoLT.symm = e.symm.toRelIsoLT

Full source

@[simp]
theorem toRelIsoLT_symm (e : α ≃o β) : e.toRelIsoLT.symm = e.symm.toRelIsoLT :=
  rfl

Inverse of Strict Order Relation Isomorphism Induced by Order Isomorphism

Informal description

For any order isomorphism $e \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the inverse of the strict order relation isomorphism induced by $e$ is equal to the strict order relation isomorphism induced by the inverse of $e$. That is, $(e.\text{toRelIsoLT}).\text{symm} = e.\text{symm}.\text{toRelIsoLT}$.

OrderIso.ofRelIsoLT definition

 {α β} [PartialOrder α] [PartialOrder β] (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) : α ≃o β

Full source

/-- Converts a `RelIso (<) (<)` into an `OrderIso`. -/
def ofRelIsoLT {α β} [PartialOrder α] [PartialOrder β]
    (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) : α ≃o β :=
  ⟨e.toEquiv, by simp [le_iff_eq_or_lt, e.map_rel_iff, e.injective.eq_iff]⟩

Order isomorphism from strict order relation isomorphism

Informal description

Given two partially ordered sets $\alpha$ and $\beta$, and a relation isomorphism $e$ between their strict orders $(<)$, the function constructs an order isomorphism $\alpha \simeq_o \beta$ by extending $e$ to an equivalence that preserves the order relation in both directions. Specifically, for any $x, y \in \alpha$, we have $x \leq y$ if and only if $e(x) \leq e(y)$.

OrderIso.ofRelIsoLT_apply theorem

 {α β} [PartialOrder α] [PartialOrder β] (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) (x : α) :
  ofRelIsoLT e x = e x

Full source

@[simp]
theorem ofRelIsoLT_apply {α β} [PartialOrder α] [PartialOrder β]
    (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) (x : α) : ofRelIsoLT e x = e x :=
  rfl

Evaluation of Order Isomorphism from Strict Order Relation Isomorphism

Informal description

Let $\alpha$ and $\beta$ be partially ordered sets, and let $e : (\alpha, <) \simeqr (\beta, <)$ be a relation isomorphism between their strict orders. For any element $x \in \alpha$, the order isomorphism $\text{ofRelIsoLT}\ e$ evaluated at $x$ equals $e(x)$.

OrderIso.ofRelIsoLT_symm theorem

 {α β} [PartialOrder α] [PartialOrder β] (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) :
  (ofRelIsoLT e).symm = ofRelIsoLT e.symm

Full source

@[simp]
theorem ofRelIsoLT_symm {α β} [PartialOrder α] [PartialOrder β]
    (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) :
    (ofRelIsoLT e).symm = ofRelIsoLT e.symm :=
  rfl

Inverse of Order Isomorphism from Strict Order Relation Isomorphism

Informal description

Given two partially ordered sets $\alpha$ and $\beta$, and a relation isomorphism $e$ between their strict orders $(<)$, the inverse of the order isomorphism constructed from $e$ is equal to the order isomorphism constructed from the inverse of $e$. In other words, $(\text{ofRelIsoLT}~e)^{-1} = \text{ofRelIsoLT}~(e^{-1})$.

OrderIso.ofRelIsoLT_toRelIsoLT theorem

{α β} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : ofRelIsoLT (toRelIsoLT e) = e

Full source

@[simp]
theorem ofRelIsoLT_toRelIsoLT {α β} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
    ofRelIsoLT (toRelIsoLT e) = e := by
  ext
  simp

Identity of Order Isomorphism Construction via Strict Order Relations

Informal description

Let $\alpha$ and $\beta$ be partially ordered sets, and let $e : \alpha \simeq_o \beta$ be an order isomorphism. Then the composition of the operations `toRelIsoLT` (converting $e$ to a strict order relation isomorphism) and `ofRelIsoLT` (converting back to an order isomorphism) yields the original isomorphism $e$.

OrderIso.toRelIsoLT_ofRelIsoLT theorem

 {α β} [PartialOrder α] [PartialOrder β] (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) :
  toRelIsoLT (ofRelIsoLT e) = e

Full source

@[simp]
theorem toRelIsoLT_ofRelIsoLT {α β} [PartialOrder α] [PartialOrder β]
    (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) : toRelIsoLT (ofRelIsoLT e) = e := by
  ext
  simp

Round-trip Equivalence of Order Isomorphism and Strict Order Relation Isomorphism

Informal description

For any two partially ordered sets $\alpha$ and $\beta$, and a relation isomorphism $e$ between their strict orders $(<)$, the composition of converting $e$ to an order isomorphism and then back to a relation isomorphism yields $e$ itself. That is, $\text{toRelIsoLT}(\text{ofRelIsoLT}(e)) = e$.

OrderIso.ofCmpEqCmp definition

 {α β} [LinearOrder α] [LinearOrder β] (f : α → β) (g : β → α) (h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b) :
  α ≃o β

Full source

/-- 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`. -/
def ofCmpEqCmp {α β} [LinearOrder α] [LinearOrder β] (f : α → β) (g : β → α)
    (h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b) : α ≃o β :=
  have gf : ∀ a : α, a = g (f a) := by
    intro
    rw [← cmp_eq_eq_iff, h, cmp_self_eq_eq]
  { toFun := f, invFun := g, left_inv := fun a => (gf a).symm,
    right_inv := by
      intro
      rw [← cmp_eq_eq_iff, ← h, cmp_self_eq_eq],
    map_rel_iff' := by
      intros a b
      apply le_iff_le_of_cmp_eq_cmp
      convert (h a (f b)).symm
      apply gf }

Order isomorphism from comparison equality

Informal description

Given two linearly ordered types $\alpha$ and $\beta$, and functions $f : \alpha \to \beta$ and $g : \beta \to \alpha$, if for all $a \in \alpha$ and $b \in \beta$ the comparison $\text{cmp}(a, g(b))$ equals $\text{cmp}(f(a), b)$, then $f$ and $g$ form an order isomorphism between $\alpha$ and $\beta$.

OrderIso.ofHomInv definition

 {F G : Type*} [FunLike F α β] [OrderHomClass F α β] [FunLike G β α] [OrderHomClass G β α] (f : F) (g : G)
  (h₁ : (f : α →o β).comp (g : β →o α) = OrderHom.id) (h₂ : (g : β →o α).comp (f : α →o β) = OrderHom.id) : α ≃o β

Full source

/-- 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`. -/
def ofHomInv {F G : Type*} [FunLike F α β] [OrderHomClass F α β] [FunLike G β α]
    [OrderHomClass G β α] (f : F) (g : G)
    (h₁ : (f : α →o β).comp (g : β →o α) = OrderHom.id)
    (h₂ : (g : β →o α).comp (f : α →o β) = OrderHom.id) :
    α ≃o β where
  toFun := f
  invFun := g
  left_inv := DFunLike.congr_fun h₂
  right_inv := DFunLike.congr_fun h₁
  map_rel_iff' := @fun a b =>
    ⟨fun h => by
      replace h := map_rel g h
      rwa [Equiv.coe_fn_mk, show g (f a) = (g : β →o α).comp (f : α →o β) a from rfl,
        show g (f b) = (g : β →o α).comp (f : α →o β) b from rfl, h₂] at h,
      fun h => (f : α →o β).monotone h⟩

Order isomorphism from homomorphism-inverse pairs

Informal description

Given two types $\alpha$ and $\beta$ with preorders, and two function-like types $F$ and $G$ where $F$ consists of order-preserving maps from $\alpha$ to $\beta$ and $G$ consists of order-preserving maps from $\beta$ to $\alpha$, if $f \in F$ and $g \in G$ satisfy the conditions that their compositions in both directions yield the identity order homomorphism, then $f$ and $g$ form an order isomorphism between $\alpha$ and $\beta$. Specifically, $f$ is the forward map and $g$ is its inverse, both preserving the order relation.

OrderIso.funUnique definition

(α β : Type*) [Unique α] [Preorder β] : (α → β) ≃o β

Full source

/-- Order isomorphism between `α → β` and `β`, where `α` has a unique element. -/
@[simps! toEquiv apply]
def funUnique (α β : Type*) [Unique α] [Preorder β] : (α → β) ≃o β where
  toEquiv := Equiv.funUnique α β
  map_rel_iff' := by simp [Pi.le_def, Unique.forall_iff]

Order isomorphism between functions from a singleton type and their codomain

Informal description

Given a type $\alpha$ with a unique element and a preordered type $\beta$, the type of order-preserving functions from $\alpha$ to $\beta$ is order-isomorphic to $\beta$ itself. The isomorphism maps a function $f \colon \alpha \to \beta$ to its value at the unique element of $\alpha$, and conversely, any element $b \in \beta$ corresponds to the constant function with value $b$.

OrderIso.funUnique_symm_apply theorem

{α β : Type*} [Unique α] [Preorder β] : ((funUnique α β).symm : β → α → β) = Function.const α

Full source

@[simp]
theorem funUnique_symm_apply {α β : Type*} [Unique α] [Preorder β] :
    ((funUnique α β).symm : β → α → β) = Function.const α :=
  rfl

Inverse of `funUnique` is the Constant Function Constructor

Informal description

For any type $\alpha$ with a unique element and any preordered type $\beta$, the inverse of the order isomorphism `funUnique` (which maps functions $\alpha \to \beta$ to their evaluation at the unique element of $\alpha$) is equal to the constant function constructor $\text{const} \colon \beta \to (\alpha \to \beta)$.

OrderIso.ofUnique definition

(α β : Type*) [Unique α] [Unique β] [Preorder α] [Preorder β] : α ≃o β

Full source

/-- The order isomorphism `α ≃o β` when `α` and `β` are preordered types
containing unique elements. -/
@[simps!]
noncomputable def ofUnique
    (α β : Type*) [Unique α] [Unique β] [Preorder α] [Preorder β] :
    α ≃o β where
  toEquiv := Equiv.ofUnique α β
  map_rel_iff' := by simp

Order isomorphism between types with unique elements

Informal description

Given two preordered types $\alpha$ and $\beta$ each containing exactly one element, there exists a unique order isomorphism between them. This isomorphism maps the unique element of $\alpha$ to the unique element of $\beta$ and preserves the order relation in both directions.

Equiv.toOrderIso definition

(e : α ≃ β) (h₁ : Monotone e) (h₂ : Monotone e.symm) : α ≃o β

Full source

/-- If `e` is an equivalence with monotone forward and inverse maps, then `e` is an
order isomorphism. -/
def toOrderIso (e : α ≃ β) (h₁ : Monotone e) (h₂ : Monotone e.symm) : α ≃o β :=
  ⟨e, ⟨fun h => by simpa only [e.symm_apply_apply] using h₂ h, fun h => h₁ h⟩⟩

Order isomorphism from a monotone bijection with monotone inverse

Informal description

Given a bijection $ e : \alpha \simeq \beta $ between two preordered types, if both $ e $ and its inverse $ e^{-1} $ are monotone (order-preserving), then $ e $ is an order isomorphism between $ \alpha $ and $ \beta $.

Equiv.coe_toOrderIso theorem

(e : α ≃ β) (h₁ : Monotone e) (h₂ : Monotone e.symm) : ⇑(e.toOrderIso h₁ h₂) = e

Full source

@[simp]
theorem coe_toOrderIso (e : α ≃ β) (h₁ : Monotone e) (h₂ : Monotone e.symm) :
    ⇑(e.toOrderIso h₁ h₂) = e :=
  rfl

Underlying Function of Order Isomorphism from Monotone Bijection

Informal description

Given a bijection $e : \alpha \simeq \beta$ between two preordered types, if both $e$ and its inverse $e^{-1}$ are monotone (order-preserving), then the underlying function of the order isomorphism constructed from $e$ is equal to $e$ itself. That is, $\text{toOrderIso}(e, h₁, h₂) = e$.

Equiv.toOrderIso_toEquiv theorem

(e : α ≃ β) (h₁ : Monotone e) (h₂ : Monotone e.symm) : (e.toOrderIso h₁ h₂).toEquiv = e

Full source

@[simp]
theorem toOrderIso_toEquiv (e : α ≃ β) (h₁ : Monotone e) (h₂ : Monotone e.symm) :
    (e.toOrderIso h₁ h₂).toEquiv = e :=
  rfl

Underlying Equivalence of Order Isomorphism Construction

Informal description

Given a bijection $e : \alpha \simeq \beta$ between two preordered types, if both $e$ and its inverse $e^{-1}$ are monotone (order-preserving), then the underlying equivalence of the resulting order isomorphism $e.\text{toOrderIso}~h_1~h_2$ is equal to $e$.

StrictMono.orderIsoOfRightInverse definition

(g : β → α) (hg : Function.RightInverse g f) : α ≃o β

Full source

/-- A strictly monotone function with a right inverse is an order isomorphism. -/
@[simps -fullyApplied]
def orderIsoOfRightInverse (g : β → α) (hg : Function.RightInverse g f) : α ≃o β :=
  { OrderEmbedding.ofStrictMono f h_mono with
    toFun := f,
    invFun := g,
    left_inv := fun _ => h_mono.injective <| hg _,
    right_inv := hg }

Order isomorphism from strictly monotone function with right inverse

Informal description

Given a strictly monotone function $f : \alpha \to \beta$ between linearly ordered types, and a right inverse $g : \beta \to \alpha$ of $f$ (i.e., $f \circ g = \text{id}_\beta$), the function $f$ can be promoted to an order isomorphism between $\alpha$ and $\beta$. This isomorphism preserves the order structure in both directions, meaning $x \leq y$ if and only if $f(x) \leq f(y)$ for all $x, y \in \alpha$.

OrderIso.dual definition

[LE α] [LE β] (f : α ≃o β) : αᵒᵈ ≃o βᵒᵈ

Full source

/-- An order isomorphism is also an order isomorphism between dual orders. -/
protected def OrderIso.dual [LE α] [LE β] (f : α ≃o β) : αᵒᵈαᵒᵈ ≃o βᵒᵈ :=
  ⟨f.toEquiv, f.map_rel_iff⟩

Dual Order Isomorphism

Informal description

Given an order isomorphism $f : \alpha \simeq_o \beta$ between two preordered types $\alpha$ and $\beta$, the dual order isomorphism $f^{\mathrm{dual}} : \alpha^{\mathrm{op}} \simeq_o \beta^{\mathrm{op}}$ is defined by the same underlying bijection as $f$, but now viewed as a map between the opposite orders $\alpha^{\mathrm{op}}$ and $\beta^{\mathrm{op}}$.

OrderIso.map_bot' theorem

[LE α] [PartialOrder β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ x', x ≤ x') (hy : ∀ y', y ≤ y') : f x = y

Full source

theorem OrderIso.map_bot' [LE α] [PartialOrder β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ x', x ≤ x')
    (hy : ∀ y', y ≤ y') : f x = y := by
  refine le_antisymm ?_ (hy _)
  rw [← f.apply_symm_apply y, f.map_rel_iff]
  apply hx

Order Isomorphism Preserves Universal Lower Bounds: $f(x) = y$

Informal description

Let $\alpha$ be a preorder and $\beta$ be a partial order. Given an order isomorphism $f : \alpha \simeq_o \beta$, an element $x \in \alpha$ that is a lower bound for all elements in $\alpha$ (i.e., $x \leq x'$ for all $x' \in \alpha$), and an element $y \in \beta$ that is a lower bound for all elements in $\beta$ (i.e., $y \leq y'$ for all $y' \in \beta$), then $f(x) = y$.

OrderIso.map_bot theorem

[LE α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) : f ⊥ = ⊥

Full source

theorem OrderIso.map_bot [LE α] [PartialOrder β] [OrderBot α] [OrderBot β] (f : α ≃o β) : f ⊥ = ⊥ :=
  f.map_bot' (fun _ => bot_le) fun _ => bot_le

Order Isomorphism Preserves Bottom Element: $f(\bot) = \bot$

Informal description

Let $\alpha$ be a preorder with a least element $\bot_\alpha$, and $\beta$ be a partial order with a least element $\bot_\beta$. For any order isomorphism $f : \alpha \simeq_o \beta$, we have $f(\bot_\alpha) = \bot_\beta$.

OrderIso.map_top' theorem

[LE α] [PartialOrder β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ x', x' ≤ x) (hy : ∀ y', y' ≤ y) : f x = y

Full source

theorem OrderIso.map_top' [LE α] [PartialOrder β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ x', x' ≤ x)
    (hy : ∀ y', y' ≤ y) : f x = y :=
  f.dual.map_bot' hx hy

Order Isomorphism Preserves Universal Upper Bounds: $f(x) = y$

Informal description

Let $\alpha$ be a preorder and $\beta$ be a partial order. Given an order isomorphism $f \colon \alpha \simeq_o \beta$, an element $x \in \alpha$ that is an upper bound for all elements in $\alpha$ (i.e., $x' \leq x$ for all $x' \in \alpha$), and an element $y \in \beta$ that is an upper bound for all elements in $\beta$ (i.e., $y' \leq y$ for all $y' \in \beta$), then $f(x) = y$.

OrderIso.map_top theorem

[LE α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) : f ⊤ = ⊤

Full source

theorem OrderIso.map_top [LE α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) : f ⊤ = ⊤ :=
  f.dual.map_bot

Order Isomorphism Preserves Top Element: $f(\top) = \top$

Informal description

Let $\alpha$ be a preorder with a greatest element $\top_\alpha$, and $\beta$ be a partial order with a greatest element $\top_\beta$. For any order isomorphism $f \colon \alpha \simeq_o \beta$, we have $f(\top_\alpha) = \top_\beta$.

OrderEmbedding.map_inf_le theorem

[SemilatticeInf α] [SemilatticeInf β] (f : α ↪o β) (x y : α) : f (x ⊓ y) ≤ f x ⊓ f y

Full source

theorem OrderEmbedding.map_inf_le [SemilatticeInf α] [SemilatticeInf β] (f : α ↪o β) (x y : α) :
    f (x ⊓ y) ≤ f x ⊓ f y :=
  f.monotone.map_inf_le x y

Order Embedding Preserves Meet Inequality

Informal description

Let $\alpha$ and $\beta$ be semilattices with infima (meet operations $\sqcap$). For any order embedding $f \colon \alpha \hookrightarrow \beta$ and any elements $x, y \in \alpha$, the image of the meet satisfies $f(x \sqcap y) \leq f(x) \sqcap f(y)$ in $\beta$.

OrderEmbedding.le_map_sup theorem

[SemilatticeSup α] [SemilatticeSup β] (f : α ↪o β) (x y : α) : f x ⊔ f y ≤ f (x ⊔ y)

Full source

theorem OrderEmbedding.le_map_sup [SemilatticeSup α] [SemilatticeSup β] (f : α ↪o β) (x y : α) :
    f x ⊔ f y ≤ f (x ⊔ y) :=
  f.monotone.le_map_sup x y

Order Embedding Preserves Supremum Inequality

Informal description

Let $\alpha$ and $\beta$ be semilattices with supremum operations $\sqcup_\alpha$ and $\sqcup_\beta$ respectively. For any order embedding $f \colon \alpha \hookrightarrow \beta$ and any elements $x, y \in \alpha$, the supremum of $f(x)$ and $f(y)$ in $\beta$ is less than or equal to the image under $f$ of the supremum of $x$ and $y$ in $\alpha$, i.e., $f(x) \sqcup_\beta f(y) \leq f(x \sqcup_\alpha y)$.

OrderIso.map_inf theorem

[SemilatticeInf α] [SemilatticeInf β] (f : α ≃o β) (x y : α) : f (x ⊓ y) = f x ⊓ f y

Full source

theorem OrderIso.map_inf [SemilatticeInf α] [SemilatticeInf β] (f : α ≃o β) (x y : α) :
    f (x ⊓ y) = f x ⊓ f y := by
  refine (f.toOrderEmbedding.map_inf_le x y).antisymm ?_
  apply f.symm.le_iff_le.1
  simpa using f.symm.toOrderEmbedding.map_inf_le (f x) (f y)

Order Isomorphism Preserves Meet: $f(x \sqcap y) = f(x) \sqcap f(y)$

Informal description

Let $\alpha$ and $\beta$ be semilattices with infima (meet operations $\sqcap$). For any order isomorphism $f \colon \alpha \simeq_o \beta$ and any elements $x, y \in \alpha$, the image of the meet under $f$ equals the meet of the images, i.e., $f(x \sqcap y) = f(x) \sqcap f(y)$.

OrderIso.map_sup theorem

[SemilatticeSup α] [SemilatticeSup β] (f : α ≃o β) (x y : α) : f (x ⊔ y) = f x ⊔ f y

Full source

theorem OrderIso.map_sup [SemilatticeSup α] [SemilatticeSup β] (f : α ≃o β) (x y : α) :
    f (x ⊔ y) = f x ⊔ f y :=
  f.dual.map_inf x y

Order Isomorphism Preserves Supremum: $f(x \sqcup y) = f(x) \sqcup f(y)$

Informal description

Let $\alpha$ and $\beta$ be semilattices with supremum operations $\sqcup$. For any order isomorphism $f \colon \alpha \simeq_o \beta$ and any elements $x, y \in \alpha$, the image of the supremum under $f$ equals the supremum of the images, i.e., $f(x \sqcup y) = f(x) \sqcup f(y)$.

OrderIso.isMax_apply theorem

{α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} : IsMax (f x) ↔ IsMax x

Full source

theorem OrderIso.isMax_apply {α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} :
    IsMaxIsMax (f x) ↔ IsMax x := by
  refine ⟨f.strictMono.isMax_of_apply, ?_⟩
  conv_lhs => rw [← f.symm_apply_apply x]
  exact f.symm.strictMono.isMax_of_apply

Order Isomorphism Preserves Maximal Elements: $f(x)$ is maximal iff $x$ is maximal

Informal description

For any order isomorphism $f \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any element $x \in \alpha$, the image $f(x)$ is a maximal element in $\beta$ if and only if $x$ is a maximal element in $\alpha$.

OrderIso.isMin_apply theorem

{α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} : IsMin (f x) ↔ IsMin x

Full source

theorem OrderIso.isMin_apply {α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} :
    IsMinIsMin (f x) ↔ IsMin x := by
  refine ⟨f.strictMono.isMin_of_apply, ?_⟩
  conv_lhs => rw [← f.symm_apply_apply x]
  exact f.symm.strictMono.isMin_of_apply

Order Isomorphism Preserves Minimal Elements: $f(x)$ is minimal iff $x$ is minimal

Informal description

For any order isomorphism $f \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, and for any element $x \in \alpha$, the image $f(x)$ is a minimal element in $\beta$ if and only if $x$ is a minimal element in $\alpha$.

Disjoint.map_orderIso theorem

 [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β] {a b : α} (f : α ≃o β) (ha : Disjoint a b) :
  Disjoint (f a) (f b)

Full source

/-- Note that this goal could also be stated `(Disjoint on f) a b` -/
theorem Disjoint.map_orderIso [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β]
    {a b : α} (f : α ≃o β) (ha : Disjoint a b) : Disjoint (f a) (f b) := by
  rw [disjoint_iff_inf_le, ← f.map_inf, ← f.map_bot]
  exact f.monotone ha.le_bot

Order Isomorphism Preserves Disjointness: $f(a) \sqcap f(b) = \bot$ when $a \sqcap b = \bot$

Informal description

Let $\alpha$ and $\beta$ be semilattices with infima and least elements $\bot_\alpha$ and $\bot_\beta$ respectively. Given an order isomorphism $f \colon \alpha \simeq_o \beta$ and elements $a, b \in \alpha$ such that $a \sqcap b = \bot_\alpha$, then $f(a) \sqcap f(b) = \bot_\beta$.

Codisjoint.map_orderIso theorem

 [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β] {a b : α} (f : α ≃o β) (ha : Codisjoint a b) :
  Codisjoint (f a) (f b)

Full source

/-- Note that this goal could also be stated `(Codisjoint on f) a b` -/
theorem Codisjoint.map_orderIso [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β]
    {a b : α} (f : α ≃o β) (ha : Codisjoint a b) : Codisjoint (f a) (f b) := by
  rw [codisjoint_iff_le_sup, ← f.map_sup, ← f.map_top]
  exact f.monotone ha.top_le

Order Isomorphism Preserves Codisjointness: $f(a) \sqcup f(b) = \top$ when $a \sqcup b = \top$

Informal description

Let $\alpha$ and $\beta$ be semilattices with supremum operations and greatest elements $\top_\alpha$ and $\top_\beta$ respectively. Given an order isomorphism $f \colon \alpha \simeq_o \beta$ and elements $a, b \in \alpha$ such that $a \sqcup b = \top_\alpha$, then $f(a) \sqcup f(b) = \top_\beta$.

disjoint_map_orderIso_iff theorem

 [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β] {a b : α} (f : α ≃o β) :
  Disjoint (f a) (f b) ↔ Disjoint a b

Full source

@[simp]
theorem disjoint_map_orderIso_iff [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β]
    {a b : α} (f : α ≃o β) : DisjointDisjoint (f a) (f b) ↔ Disjoint a b :=
  ⟨fun h => f.symm_apply_apply a ▸ f.symm_apply_apply b ▸ h.map_orderIso f.symm,
   fun h => h.map_orderIso f⟩

Order Isomorphism Preserves Disjointness: $f(a) \sqcap f(b) = \bot_\beta \leftrightarrow a \sqcap b = \bot_\alpha$

Informal description

Let $\alpha$ and $\beta$ be semilattices with infima and least elements $\bot_\alpha$ and $\bot_\beta$ respectively. Given an order isomorphism $f \colon \alpha \simeq_o \beta$ and elements $a, b \in \alpha$, the elements $f(a)$ and $f(b)$ are disjoint (i.e., $f(a) \sqcap f(b) = \bot_\beta$) if and only if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot_\alpha$).

codisjoint_map_orderIso_iff theorem

 [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β] {a b : α} (f : α ≃o β) :
  Codisjoint (f a) (f b) ↔ Codisjoint a b

Full source

@[simp]
theorem codisjoint_map_orderIso_iff [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β]
    {a b : α} (f : α ≃o β) : CodisjointCodisjoint (f a) (f b) ↔ Codisjoint a b :=
  ⟨fun h => f.symm_apply_apply a ▸ f.symm_apply_apply b ▸ h.map_orderIso f.symm,
   fun h => h.map_orderIso f⟩

Order Isomorphism Preserves Codisjointness: $f(a) \sqcup f(b) = \top_\beta \leftrightarrow a \sqcup b = \top_\alpha$

Informal description

Let $\alpha$ and $\beta$ be semilattices with supremum operations and greatest elements $\top_\alpha$ and $\top_\beta$ respectively. Given an order isomorphism $f \colon \alpha \simeq_o \beta$ and elements $a, b \in \alpha$, the elements $f(a)$ and $f(b)$ are codisjoint (i.e., $f(a) \sqcup f(b) = \top_\beta$) if and only if $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top_\alpha$).

OrderIso.isCompl theorem

{x y : α} (h : IsCompl x y) : IsCompl (f x) (f y)

Full source

theorem OrderIso.isCompl {x y : α} (h : IsCompl x y) : IsCompl (f x) (f y) :=
  ⟨h.1.map_orderIso _, h.2.map_orderIso _⟩

Order Isomorphism Preserves Complementedness: $f(x) \sqcap f(y) = \bot$ and $f(x) \sqcup f(y) = \top$ when $x \sqcap y = \bot$ and $x \sqcup y = \top$

Informal description

Let $\alpha$ and $\beta$ be bounded lattices, and let $f \colon \alpha \simeq_o \beta$ be an order isomorphism. For any elements $x, y \in \alpha$ that are complements (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$), their images $f(x)$ and $f(y)$ are complements in $\beta$ (i.e., $f(x) \sqcap f(y) = \bot$ and $f(x) \sqcup f(y) = \top$).

OrderIso.isCompl_iff theorem

{x y : α} : IsCompl x y ↔ IsCompl (f x) (f y)

Full source

theorem OrderIso.isCompl_iff {x y : α} : IsComplIsCompl x y ↔ IsCompl (f x) (f y) :=
  ⟨f.isCompl, fun h => f.symm_apply_apply x ▸ f.symm_apply_apply y ▸ f.symm.isCompl h⟩

Order Isomorphism Characterizes Complementedness: $x \sqcap y = \bot_\alpha \land x \sqcup y = \top_\alpha \leftrightarrow f(x) \sqcap f(y) = \bot_\beta \land f(x) \sqcup f(y) = \top_\beta$

Informal description

Let $\alpha$ and $\beta$ be bounded lattices, and let $f \colon \alpha \simeq_o \beta$ be an order isomorphism. For any elements $x, y \in \alpha$, the following are equivalent: 1. $x$ and $y$ are complements in $\alpha$ (i.e., $x \sqcap y = \bot_\alpha$ and $x \sqcup y = \top_\alpha$). 2. $f(x)$ and $f(y)$ are complements in $\beta$ (i.e., $f(x) \sqcap f(y) = \bot_\beta$ and $f(x) \sqcup f(y) = \top_\beta$).

OrderIso.complementedLattice theorem

[ComplementedLattice α] (f : α ≃o β) : ComplementedLattice β

Full source

theorem OrderIso.complementedLattice [ComplementedLattice α] (f : α ≃o β) : ComplementedLattice β :=
  ⟨fun x => by
    obtain ⟨y, hy⟩ := exists_isCompl (f.symm x)
    rw [← f.symm_apply_apply y] at hy
    exact ⟨f y, f.symm.isCompl_iff.2 hy⟩⟩

Order Isomorphism Preserves Complemented Lattice Property

Informal description

Let $\alpha$ and $\beta$ be bounded lattices, and let $f \colon \alpha \simeq_o \beta$ be an order isomorphism. If $\alpha$ is a complemented lattice, then $\beta$ is also a complemented lattice.

OrderIso.complementedLattice_iff theorem

(f : α ≃o β) : ComplementedLattice α ↔ ComplementedLattice β

Full source

theorem OrderIso.complementedLattice_iff (f : α ≃o β) :
    ComplementedLatticeComplementedLattice α ↔ ComplementedLattice β :=
  ⟨by intro; exact f.complementedLattice,
   by intro; exact f.symm.complementedLattice⟩

Order Isomorphism Characterizes Complemented Lattice Property: $\alpha$ is complemented $\leftrightarrow$ $\beta$ is complemented

Informal description

Let $\alpha$ and $\beta$ be bounded lattices, and let $f \colon \alpha \simeq_o \beta$ be an order isomorphism. Then $\alpha$ is a complemented lattice if and only if $\beta$ is a complemented lattice.

OrderIsoClass.toOrderIsoClassOrderDual instance

[LE α] [LE β] [EquivLike F α β] [OrderIsoClass F α β] : OrderIsoClass F αᵒᵈ βᵒᵈ

Full source

instance (priority := 90) OrderIsoClass.toOrderIsoClassOrderDual [LE α] [LE β]
    [EquivLike F α β] [OrderIsoClass F α β] : OrderIsoClass F αᵒᵈ βᵒᵈ where
  map_le_map_iff f := map_le_map_iff f

Order Isomorphism Class for Order Duals

Informal description

For any type `F` that represents order isomorphisms between types `α` and `β` equipped with a partial order relation `≤`, the same type `F` also represents order isomorphisms between the order duals `αᵒᵈ` and `βᵒᵈ`. This means that if `F` is a class of order-preserving and order-reflecting bijections between `α` and `β`, then it also serves as a class of order-preserving and order-reflecting bijections between their order duals.

denselyOrdered_iff_of_orderIsoClass theorem

 {X Y F : Type*} [Preorder X] [Preorder Y] [EquivLike F X Y] [OrderIsoClass F X Y] (f : F) :
  DenselyOrdered X ↔ DenselyOrdered Y

Full source

lemma denselyOrdered_iff_of_orderIsoClass {X Y F : Type*} [Preorder X] [Preorder Y]
    [EquivLike F X Y] [OrderIsoClass F X Y] (f : F) :
    DenselyOrderedDenselyOrdered X ↔ DenselyOrdered Y := by
  constructor
  · intro H
    refine ⟨fun a b h ↦ ?_⟩
    obtain ⟨c, hc⟩ := exists_between ((map_inv_lt_map_inv_iff f).mpr h)
    exact ⟨f c, by simpa using hc⟩
  · intro H
    refine ⟨fun a b h ↦ ?_⟩
    obtain ⟨c, hc⟩ := exists_between ((map_lt_map_iff f).mpr h)
    exact ⟨EquivLike.inv f c, by simpa using hc⟩

Dense Order Preservation under Order Isomorphism: $X$ is densely ordered if and only if $Y$ is densely ordered for any order isomorphism $f \colon X \to Y$

Informal description

Let $X$ and $Y$ be preorders, and let $F$ be a type of order isomorphisms between $X$ and $Y$. For any order isomorphism $f \in F$, the preorder $X$ is densely ordered if and only if $Y$ is densely ordered. Here, a preorder is densely ordered if for any two elements $x < y$, there exists an element $z$ such that $x < z < y$.

Mathlib.Order.Hom.Basic

Main definitions

Tags