Mathlib.Order.Hom.WithTopBot

WithTop.toDualBotEquiv definition

[LE α] : WithTop αᵒᵈ ≃o (WithBot α)ᵒᵈ

Full source

/-- Taking the dual then adding `⊤` is the same as adding `⊥` then taking the dual.
This is the order iso form of `WithTop.ofDual`, as proven by `coe_toDualBotEquiv`. -/
protected def toDualBotEquiv [LE α] : WithTopWithTop αᵒᵈ ≃o (WithBot α)ᵒᵈ :=
  OrderIso.refl _

Order isomorphism between `WithTop αᵒᵈ` and `(WithBot α)ᵒᵈ`

Informal description

For any type $\alpha$ with a preorder (denoted by `[LE α]`), there is an order isomorphism between `WithTop αᵒᵈ` (the type obtained by adding a top element to the order dual of $\alpha$) and `(WithBot α)ᵒᵈ` (the order dual of the type obtained by adding a bottom element to $\alpha$). This isomorphism captures the equivalence between adding a top element to the dual and adding a bottom element then taking the dual.

WithTop.toDualBotEquiv_coe theorem

[LE α] (a : α) : WithTop.toDualBotEquiv ↑(toDual a) = toDual (a : WithBot α)

Full source

@[simp]
theorem toDualBotEquiv_coe [LE α] (a : α) :
    WithTop.toDualBotEquiv ↑(toDual a) = toDual (a : WithBot α) :=
  rfl

Action of `WithTop.toDualBotEquiv` on elements of $\alpha$

Informal description

For any type $\alpha$ equipped with a preorder and any element $a \in \alpha$, the order isomorphism `WithTop.toDualBotEquiv` maps the element $\text{toDual}(a)$ (viewed in `WithTop αᵒᵈ`) to $\text{toDual}(a)$ (viewed in `(WithBot α)ᵒᵈ`). That is, the following equality holds: $$ \text{WithTop.toDualBotEquiv}(\text{toDual}(a)) = \text{toDual}(a). $$

WithTop.toDualBotEquiv_symm_coe theorem

[LE α] (a : α) : WithTop.toDualBotEquiv.symm (toDual (a : WithBot α)) = ↑(toDual a)

Full source

@[simp]
theorem toDualBotEquiv_symm_coe [LE α] (a : α) :
    WithTop.toDualBotEquiv.symm (toDual (a : WithBot α)) = ↑(toDual a) :=
  rfl

Inverse Image of Dual Element under Order Isomorphism $\text{WithTop.toDualBotEquiv}$

Informal description

For any type $\alpha$ equipped with a preorder $\leq$ and any element $a \in \alpha$, the inverse of the order isomorphism $\text{WithTop.toDualBotEquiv}$ maps the dual of the element $a$ in $\text{WithBot} \alpha$ to the dual of $a$ in $\text{WithTop} \alpha^\text{op}$. In symbols: \[ \text{WithTop.toDualBotEquiv}^{-1}(\text{toDual}(a)) = \text{toDual}(a) \] where the left-hand side is interpreted in $(\text{WithBot} \alpha)^\text{op}$ and the right-hand side is interpreted in $\text{WithTop} \alpha^\text{op}$.

WithTop.toDualBotEquiv_top theorem

[LE α] : WithTop.toDualBotEquiv (⊤ : WithTop αᵒᵈ) = ⊤

Full source

@[simp]
theorem toDualBotEquiv_top [LE α] : WithTop.toDualBotEquiv (⊤ : WithTop αᵒᵈ) = ⊤ :=
  rfl

Top Element Preservation in Order Isomorphism `WithTop.toDualBotEquiv`

Informal description

For any type $\alpha$ with a preorder (denoted by `[LE α]`), the order isomorphism `WithTop.toDualBotEquiv` maps the top element $\top$ of `WithTop αᵒᵈ` to the top element $\top$ of `(WithBot α)ᵒᵈ`.

WithTop.toDualBotEquiv_symm_top theorem

[LE α] : WithTop.toDualBotEquiv.symm (⊤ : (WithBot α)ᵒᵈ) = ⊤

Full source

@[simp]
theorem toDualBotEquiv_symm_top [LE α] : WithTop.toDualBotEquiv.symm (⊤ : (WithBot α)ᵒᵈ) = ⊤ :=
  rfl

Inverse of Order Isomorphism Preserves Top Element

Informal description

For any type $\alpha$ equipped with a preorder, the inverse of the order isomorphism `WithTop.toDualBotEquiv` maps the top element of the order dual of `WithBot α` to the top element of `WithTop αᵒᵈ`. In other words, $\text{WithTop.toDualBotEquiv}^{-1}(\top) = \top$.

WithTop.coe_toDualBotEquiv theorem

[LE α] : (WithTop.toDualBotEquiv : WithTop αᵒᵈ → (WithBot α)ᵒᵈ) = toDual ∘ WithTop.ofDual

Full source

theorem coe_toDualBotEquiv [LE α] :
    (WithTop.toDualBotEquiv : WithTop αᵒᵈ → (WithBot α)ᵒᵈ) = toDualtoDual ∘ WithTop.ofDual :=
  funext fun _ => rfl

Equality of `WithTop.toDualBotEquiv` with composition of dual maps

Informal description

For any type $\alpha$ with a preorder, the order isomorphism `WithTop.toDualBotEquiv` from `WithTop αᵒᵈ` to `(WithBot α)ᵒᵈ` is equal to the composition of the order dual map `toDual` with the natural map `WithTop.ofDual` that sends an element of `αᵒᵈ` to its corresponding element in `WithTop αᵒᵈ`.

Function.Embedding.coeWithTop definition

: α ↪ WithTop α

Full source

/-- Embedding into `WithTop α`. -/
@[simps]
def _root_.Function.Embedding.coeWithTop : α ↪ WithTop α where
  toFun := (↑)
  inj' := WithTop.coe_injective

Embedding from $\alpha$ to `WithTop α`

Informal description

The embedding function that maps an element $x$ of type $\alpha$ to the corresponding element in `WithTop α` (i.e., $\alpha$ with a top element adjoined), represented as `some x`. This function is injective, meaning that if two elements of $\alpha$ are mapped to the same element in `WithTop α`, then they must be equal.

WithTop.coeOrderHom definition

{α : Type*} [Preorder α] : α ↪o WithTop α

Full source

/-- The coercion `α → WithTop α` bundled as monotone map. -/
@[simps]
def coeOrderHom {α : Type*} [Preorder α] : α ↪o WithTop α where
  toFun := (↑)
  inj' := WithTop.coe_injective
  map_rel_iff' := WithTop.coe_le_coe

Order embedding of the coercion to `WithTop α`

Informal description

The coercion function from a type $\alpha$ with a preorder to `WithTop α` (the type $\alpha$ with a top element adjoined), bundled as an order embedding. This function maps an element $x \in \alpha$ to `some x \in WithTop α` and satisfies the property that for any $x, y \in \alpha$, $x \leq y$ if and only if $\text{some } x \leq \text{some } y$ in `WithTop α`.

WithBot.toDualTopEquiv definition

[LE α] : WithBot αᵒᵈ ≃o (WithTop α)ᵒᵈ

Full source

/-- Taking the dual then adding `⊥` is the same as adding `⊤` then taking the dual.
This is the order iso form of `WithBot.ofDual`, as proven by `coe_toDualTopEquiv`. -/
protected def toDualTopEquiv [LE α] : WithBotWithBot αᵒᵈ ≃o (WithTop α)ᵒᵈ :=
  OrderIso.refl _

Order isomorphism between `WithBot αᵒᵈ` and `(WithTop α)ᵒᵈ`

Informal description

Given a type $\alpha$ with a preorder, the order isomorphism `WithBot.toDualTopEquiv` establishes an equivalence between the type `WithBot αᵒᵈ` (the dual of $\alpha$ with a bottom element adjoined) and the type `(WithTop α)ᵒᵈ` (the dual of $\alpha$ with a top element adjoined). This isomorphism captures the idea that taking the dual of a type with a bottom element adjoined is equivalent to first adjoining a top element and then taking the dual.

WithBot.toDualTopEquiv_coe theorem

[LE α] (a : α) : WithBot.toDualTopEquiv ↑(toDual a) = toDual (a : WithTop α)

Full source

@[simp]
theorem toDualTopEquiv_coe [LE α] (a : α) :
    WithBot.toDualTopEquiv ↑(toDual a) = toDual (a : WithTop α) :=
  rfl

Behavior of `WithBot.toDualTopEquiv` on Coerced Dual Elements

Informal description

For any type $\alpha$ with a preorder and any element $a \in \alpha$, the order isomorphism `WithBot.toDualTopEquiv` maps the coercion of the dual element $\text{toDual}(a)$ in $\text{WithBot} \alpha^\text{op}$ to the dual of the coercion of $a$ in $\text{WithTop} \alpha$, i.e., $$\text{WithBot.toDualTopEquiv}(\text{toDual}(a)) = \text{toDual}(a).$$

WithBot.toDualTopEquiv_symm_coe theorem

[LE α] (a : α) : WithBot.toDualTopEquiv.symm (toDual (a : WithTop α)) = ↑(toDual a)

Full source

@[simp]
theorem toDualTopEquiv_symm_coe [LE α] (a : α) :
    WithBot.toDualTopEquiv.symm (toDual (a : WithTop α)) = ↑(toDual a) :=
  rfl

Inverse of Order Isomorphism Preserves Dual Elements

Informal description

For any type $\alpha$ with a preorder and any element $a \in \alpha$, the inverse of the order isomorphism `WithBot.toDualTopEquiv` maps the dual of the element $a$ in `WithTop α$ to the dual of $a$ in `WithBot αᵒᵈ`. More precisely, if we denote the order isomorphism as $\varphi : \text{WithBot } \alpha^\text{op} \simeq (\text{WithTop } \alpha)^\text{op}$, then for any $a \in \alpha$, we have: \[ \varphi^{-1}(\text{toDual}(a : \text{WithTop } \alpha)) = \text{toDual}(a : \alpha) \] where $\text{toDual}$ is the canonical map sending an element to its dual in the order-dual structure.

WithBot.toDualTopEquiv_bot theorem

[LE α] : WithBot.toDualTopEquiv (⊥ : WithBot αᵒᵈ) = ⊥

Full source

@[simp]
theorem toDualTopEquiv_bot [LE α] : WithBot.toDualTopEquiv (⊥ : WithBot αᵒᵈ) = ⊥ :=
  rfl

Bottom Element Preservation in `WithBot.toDualTopEquiv`

Informal description

For any type $\alpha$ with a preorder, the order isomorphism `WithBot.toDualTopEquiv` maps the bottom element $\bot$ of `WithBot αᵒᵈ` to the bottom element $\bot$ of `(WithTop α)ᵒᵈ}$.

WithBot.toDualTopEquiv_symm_bot theorem

[LE α] : WithBot.toDualTopEquiv.symm (⊥ : (WithTop α)ᵒᵈ) = ⊥

Full source

@[simp]
theorem toDualTopEquiv_symm_bot [LE α] : WithBot.toDualTopEquiv.symm (⊥ : (WithTop α)ᵒᵈ) = ⊥ :=
  rfl

Inverse of Order Isomorphism Preserves Bottom Element

Informal description

For any type $\alpha$ with a preorder, the inverse of the order isomorphism `WithBot.toDualTopEquiv` maps the bottom element $\bot$ of the dual of `WithTop α` to the bottom element $\bot$ of `WithBot αᵒᵈ}$.

WithBot.coe_toDualTopEquiv_eq theorem

[LE α] : (WithBot.toDualTopEquiv : WithBot αᵒᵈ → (WithTop α)ᵒᵈ) = toDual ∘ WithBot.ofDual

Full source

theorem coe_toDualTopEquiv_eq [LE α] :
    (WithBot.toDualTopEquiv : WithBot αᵒᵈ → (WithTop α)ᵒᵈ) = toDualtoDual ∘ WithBot.ofDual :=
  funext fun _ => rfl

Decomposition of WithBot-to-WithTop Dual Order Isomorphism

Informal description

For a type $\alpha$ with a preorder, the order isomorphism $\text{WithBot.toDualTopEquiv} : \text{WithBot}\ \alpha^\circ \to (\text{WithTop}\ \alpha)^\circ$ is equal to the composition of the dual map $\text{toDual}$ with the map $\text{WithBot.ofDual}$ that removes the dual structure from $\text{WithBot}\ \alpha^\circ$. Here: - $\alpha^\circ$ denotes the order dual of $\alpha$ - $\text{WithBot}\ \alpha$ is $\alpha$ extended with a bottom element $\bot$ - $\text{WithTop}\ \alpha$ is $\alpha$ extended with a top element $\top$ - $\text{toDual}$ is the canonical map to the order dual - $\text{WithBot.ofDual}$ is the map that removes the dual structure while preserving the order

Function.Embedding.coeWithBot definition

: α ↪ WithBot α

Full source

/-- Embedding into `WithBot α`. -/
@[simps]
def _root_.Function.Embedding.coeWithBot : α ↪ WithBot α where
  toFun := (↑)
  inj' := WithBot.coe_injective

Embedding into $\text{WithBot}\ \alpha$

Informal description

The embedding function that maps an element of type $\alpha$ to the corresponding element in $\text{WithBot}\ \alpha$ (the type $\alpha$ extended with a bottom element $\bot$), preserving injectivity.

WithBot.coeOrderHom definition

{α : Type*} [Preorder α] : α ↪o WithBot α

Full source

/-- The coercion `α → WithBot α` bundled as monotone map. -/
@[simps]
def coeOrderHom {α : Type*} [Preorder α] : α ↪o WithBot α where
  toFun := (↑)
  inj' := WithBot.coe_injective
  map_rel_iff' := WithBot.coe_le_coe

Canonical order embedding into $\text{WithBot}\ \alpha$

Informal description

The canonical embedding of a preordered type $\alpha$ into $\text{WithBot}\ \alpha$ (the type $\alpha$ extended with a bottom element $\bot$), viewed as an order embedding. This map sends each element $x \in \alpha$ to itself in $\text{WithBot}\ \alpha$ and is injective. Moreover, for any $x, y \in \alpha$, the inequality $x \leq y$ holds in $\alpha$ if and only if it holds in $\text{WithBot}\ \alpha$ under this embedding.

OrderHom.withBotMap definition

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

Full source

/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `WithBot α →o WithBot β`. -/
@[simps -fullyApplied]
protected def withBotMap (f : α →o β) : WithBotWithBot α →o WithBot β :=
  ⟨WithBot.map f, f.mono.withBot_map⟩

Lifting an order homomorphism to `WithBot`

Informal description

Given an order homomorphism $ f : \alpha \to \beta $, this function lifts $ f $ to an order homomorphism $ \text{WithBot} \alpha \to \text{WithBot} \beta $ by extending it to preserve the bottom element $ \bot $.

OrderHom.withTopMap definition

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

Full source

/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `WithTop α →o WithTop β`. -/
@[simps -fullyApplied]
protected def withTopMap (f : α →o β) : WithTopWithTop α →o WithTop β :=
  ⟨WithTop.map f, f.mono.withTop_map⟩

Lifting an order homomorphism to `WithTop`

Informal description

Given an order homomorphism $ f : \alpha \to \beta $, this function lifts $ f $ to an order homomorphism $ \text{WithTop} \alpha \to \text{WithTop} \beta $ by extending it to preserve the top element $ \top $.

OrderEmbedding.withBotMap definition

(f : α ↪o β) : WithBot α ↪o WithBot β

Full source

/-- A version of `WithBot.map` for order embeddings. -/
@[simps! -fullyApplied]
protected def withBotMap (f : α ↪o β) : WithBotWithBot α ↪o WithBot β where
  __ := f.toEmbedding.optionMap
  map_rel_iff' := WithBot.map_le_iff f f.map_rel_iff

Lifting an order embedding to `WithBot`

Informal description

Given an order embedding $ f \colon \alpha \hookrightarrow \beta $, the function $\operatorname{withBotMap} f$ extends $ f $ to an order embedding $\operatorname{WithBot} \alpha \hookrightarrow \operatorname{WithBot} \beta$ by mapping $\bot$ to $\bot$ and applying $ f $ to the underlying values when they exist (i.e., $\operatorname{some} x \mapsto \operatorname{some} (f x)$). This preserves the order structure and injectivity.

OrderEmbedding.withTopMap definition

(f : α ↪o β) : WithTop α ↪o WithTop β

Full source

/-- A version of `WithTop.map` for order embeddings. -/
@[simps -fullyApplied]
protected def withTopMap (f : α ↪o β) : WithTopWithTop α ↪o WithTop β :=
  { f.dual.withBotMap.dual with toFun := WithTop.map f }

Lifting an order embedding to `WithTop`

Informal description

Given an order embedding $ f \colon \alpha \hookrightarrow \beta $, the function $\operatorname{withTopMap} f$ extends $ f $ to an order embedding $\operatorname{WithTop} \alpha \hookrightarrow \operatorname{WithTop} \beta$ by mapping $\top$ to $\top$ and applying $ f $ to the underlying values when they exist (i.e., $\operatorname{some} x \mapsto \operatorname{some} (f x)$). This preserves the order structure and injectivity.

OrderEmbedding.withBotCoe definition

: α ↪o WithBot α

Full source

/-- Coercion `α → WithBot α` as an `OrderEmbedding`. -/
@[simps -fullyApplied]
protected def withBotCoe : α ↪o WithBot α where
  toFun := .some
  inj' := Option.some_injective _
  map_rel_iff' := WithBot.coe_le_coe

Canonical order embedding into $\operatorname{WithBot} \alpha$

Informal description

The embedding that maps an element $x$ of a partially ordered type $\alpha$ to $\operatorname{some}(x)$ in $\operatorname{WithBot} \alpha$, preserving the order structure. This is the canonical order embedding from $\alpha$ to $\operatorname{WithBot} \alpha$.

OrderEmbedding.withTopCoe definition

: α ↪o WithTop α

Full source

/-- Coercion `α → WithTop α` as an `OrderEmbedding`. -/
@[simps -fullyApplied]
protected def withTopCoe : α ↪o WithTop α :=
  { (OrderEmbedding.withBotCoe (α := αᵒᵈ)).dual with toFun := .some }

Canonical order embedding into $\operatorname{WithTop} \alpha$

Informal description

The embedding that maps an element $x$ of a partially ordered type $\alpha$ to $\operatorname{some}(x)$ in $\operatorname{WithTop} \alpha$, preserving the order structure. This is the canonical order embedding from $\alpha$ to $\operatorname{WithTop} \alpha$.

OrderIso.withTopCongr definition

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

Full source

/-- A version of `Equiv.optionCongr` for `WithTop`. -/
@[simps! apply]
def withTopCongr (e : α ≃o β) : WithTopWithTop α ≃o WithTop β :=
  { e.toOrderEmbedding.withTopMap with
    toEquiv := e.toEquiv.optionCongr }

Lifting an order isomorphism to `WithTop`

Informal description

Given an order isomorphism $ e \colon \alpha \simeq \beta $, the function $\operatorname{withTopCongr} e$ extends $ e $ to an order isomorphism $\operatorname{WithTop} \alpha \simeq \operatorname{WithTop} \beta$ by mapping $\top$ to $\top$ and applying $ e $ to the underlying values when they exist (i.e., $\operatorname{some} x \mapsto \operatorname{some} (e x)$). This preserves the order structure and bijectivity.

OrderIso.withTopCongr_refl theorem

: (OrderIso.refl α).withTopCongr = OrderIso.refl _

Full source

@[simp]
theorem withTopCongr_refl : (OrderIso.refl α).withTopCongr = OrderIso.refl _ :=
  RelIso.toEquiv_injective Equiv.optionCongr_refl

Identity Preservation in Lifting to $\operatorname{WithTop}$

Informal description

The lifting of the identity order isomorphism on a type $\alpha$ to $\operatorname{WithTop} \alpha$ is equal to the identity order isomorphism on $\operatorname{WithTop} \alpha$. That is, $(\operatorname{refl} \alpha).\operatorname{withTopCongr} = \operatorname{refl} (\operatorname{WithTop} \alpha)$.

OrderIso.withTopCongr_symm theorem

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

Full source

@[simp]
theorem withTopCongr_symm (e : α ≃o β) : e.withTopCongr.symm = e.symm.withTopCongr :=
  RelIso.toEquiv_injective e.toEquiv.optionCongr_symm

Symmetry of Lifted Order Isomorphism to `WithTop`

Informal description

Given an order isomorphism $e \colon \alpha \simeq \beta$, the symmetry of the lifted isomorphism $\operatorname{withTopCongr} e$ is equal to the lifting of the symmetry of $e$. That is, $(\operatorname{withTopCongr} e)^{-1} = \operatorname{withTopCongr} (e^{-1})$.

OrderIso.withTopCongr_trans theorem

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

Full source

@[simp]
theorem withTopCongr_trans (e₁ : α ≃o β) (e₂ : β ≃o γ) :
    e₁.withTopCongr.trans e₂.withTopCongr = (e₁.trans e₂).withTopCongr :=
  RelIso.toEquiv_injective <| e₁.toEquiv.optionCongr_trans e₂.toEquiv

Composition of `WithTop`-extended order isomorphisms equals extension of composed isomorphisms

Informal description

Given order isomorphisms $ e_1 \colon \alpha \simeq \beta $ and $ e_2 \colon \beta \simeq \gamma $, the composition of their extensions to `WithTop` is equal to the extension of their composition to `WithTop`. That is, \[ (e_1.\text{withTopCongr}) \circ (e_2.\text{withTopCongr}) = (e_1 \circ e_2).\text{withTopCongr}. \]

OrderIso.withBotCongr definition

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

Full source

/-- A version of `Equiv.optionCongr` for `WithBot`. -/
@[simps! apply]
def withBotCongr (e : α ≃o β) : WithBotWithBot α ≃o WithBot β :=
  { e.toOrderEmbedding.withBotMap with toEquiv := e.toEquiv.optionCongr }

Order isomorphism extension to `WithBot`

Informal description

Given an order isomorphism $ e \colon \alpha \simeq \beta $, the function $\operatorname{withBotCongr} e$ extends $ e $ to an order isomorphism $\operatorname{WithBot} \alpha \simeq \operatorname{WithBot} \beta$ by mapping $\bot$ to $\bot$ and applying $ e $ to the underlying values when they exist (i.e., $\operatorname{some} x \mapsto \operatorname{some} (e x)$). This preserves the order structure and bijectivity.

OrderIso.withBotCongr_refl theorem

: (OrderIso.refl α).withBotCongr = OrderIso.refl _

Full source

@[simp]
theorem withBotCongr_refl : (OrderIso.refl α).withBotCongr = OrderIso.refl _ :=
  RelIso.toEquiv_injective Equiv.optionCongr_refl

Identity Order Isomorphism Extension to `WithBot`

Informal description

The extension of the identity order isomorphism on a type $\alpha$ to $\operatorname{WithBot} \alpha$ is equal to the identity order isomorphism on $\operatorname{WithBot} \alpha$.

OrderIso.withBotCongr_symm theorem

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

Full source

@[simp]
theorem withBotCongr_symm (e : α ≃o β) : e.withBotCongr.symm = e.symm.withBotCongr :=
  RelIso.toEquiv_injective e.toEquiv.optionCongr_symm

Symmetry of Order Isomorphism Extension to `WithBot`: $(e_{\text{WithBot}})^{-1} = (e^{-1})_{\text{WithBot}}$

Informal description

Given an order isomorphism $e \colon \alpha \simeq \beta$, the symmetry of the extension to `WithBot` satisfies $(e_{\text{WithBot}})^{-1} = (e^{-1})_{\text{WithBot}}$, where $e_{\text{WithBot}}$ denotes the extension of $e$ to `WithBot` types.

OrderIso.withBotCongr_trans theorem

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

Full source

@[simp]
theorem withBotCongr_trans (e₁ : α ≃o β) (e₂ : β ≃o γ) :
    e₁.withBotCongr.trans e₂.withBotCongr = (e₁.trans e₂).withBotCongr :=
  RelIso.toEquiv_injective <| e₁.toEquiv.optionCongr_trans e₂.toEquiv

Composition of Order Isomorphism Extensions to `WithBot` Types

Informal description

Given order isomorphisms $e_1 \colon \alpha \simeq \beta$ and $e_2 \colon \beta \simeq \gamma$, the composition of their extensions to `WithBot` types is equal to the extension of their composition. That is, \[ (e_1.\text{withBotCongr}) \circ (e_2.\text{withBotCongr}) = (e_1 \circ e_2).\text{withBotCongr}. \]

SupHom.withTop definition

(f : SupHom α β) : SupHom (WithTop α) (WithTop β)

Full source

/-- Adjoins a `⊤` to the domain and codomain of a `SupHom`. -/
@[simps]
protected def withTop (f : SupHom α β) : SupHom (WithTop α) (WithTop β) where
  toFun := WithTop.map f
  map_sup' a b :=
    match a, b with
    | ⊤, ⊤ => rfl
    | ⊤, (b : α) => rfl
    | (a : α), ⊤ => rfl
    | (a : α), (b : α) => congr_arg _ (f.map_sup' _ _)

Extension of a supremum-preserving homomorphism to include a top element

Informal description

Given a supremum-preserving homomorphism $f \colon \alpha \to \beta$, this defines its extension to a supremum-preserving homomorphism $\text{WithTop} \alpha \to \text{WithTop} \beta$ by adjoining a top element $\top$ to both the domain and codomain. The extended function maps $\top$ to $\top$ and applies $f$ to elements of $\alpha$.

SupHom.withTop_id theorem

: (SupHom.id α).withTop = SupHom.id _

Full source

@[simp]
theorem withTop_id : (SupHom.id α).withTop = SupHom.id _ := DFunLike.coe_injective Option.map_id

Identity Extension with Top Element for Supremum-Preserving Homomorphisms

Informal description

The extension of the identity supremum-preserving homomorphism on a type $\alpha$ to include a top element is equal to the identity supremum-preserving homomorphism on the type $\text{WithTop} \alpha$. That is, $(\text{id}_\alpha).\text{withTop} = \text{id}_{\text{WithTop} \alpha}$.

SupHom.withTop_comp theorem

(f : SupHom β γ) (g : SupHom α β) : (f.comp g).withTop = f.withTop.comp g.withTop

Full source

@[simp]
theorem withTop_comp (f : SupHom β γ) (g : SupHom α β) :
    (f.comp g).withTop = f.withTop.comp g.withTop :=
  DFunLike.coe_injective <| Eq.symm <| Option.map_comp_map _ _

Composition of Extended Supremum-Preserving Homomorphisms with Top Element

Informal description

For any two supremum-preserving homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the extension of their composition $f \circ g$ to include a top element is equal to the composition of their individual extensions, i.e., $(f \circ g).\text{withTop} = f.\text{withTop} \circ g.\text{withTop}$.

SupHom.withBot definition

(f : SupHom α β) : SupBotHom (WithBot α) (WithBot β)

Full source

/-- Adjoins a `⊥` to the domain and codomain of a `SupHom`. -/
@[simps]
protected def withBot (f : SupHom α β) : SupBotHom (WithBot α) (WithBot β) where
  toFun := Option.map f
  map_sup' a b :=
    match a, b with
    | ⊥, ⊥ => rfl
    | ⊥, (b : α) => rfl
    | (a : α), ⊥ => rfl
    | (a : α), (b : α) => congr_arg _ (f.map_sup' _ _)
  map_bot' := rfl

Extension of a supremum-preserving homomorphism to include a bottom element

Informal description

Given a supremum-preserving homomorphism $f \colon \alpha \to \beta$, the function `SupHom.withBot` extends $f$ to a homomorphism between the types `WithBot α` and `WithBot β` (which adjoin a bottom element `⊥` to `α` and `β` respectively). The extended homomorphism maps `⊥` to `⊥` and applies $f$ to the non-bottom elements, preserving both the supremum operation and the bottom element.

SupHom.withBot_id theorem

: (SupHom.id α).withBot = SupBotHom.id _

Full source

@[simp]
theorem withBot_id : (SupHom.id α).withBot = SupBotHom.id _ := DFunLike.coe_injective Option.map_id

Identity Supremum Homomorphism Extension to `WithBot` Equals Identity SupBot Homomorphism

Informal description

The extension of the identity supremum-preserving homomorphism on a type $\alpha$ to a homomorphism between `WithBot α` and itself (which includes a bottom element $\bot$) is equal to the identity supremum-and-bottom-preserving homomorphism on `WithBot α$.

SupHom.withBot_comp theorem

(f : SupHom β γ) (g : SupHom α β) : (f.comp g).withBot = f.withBot.comp g.withBot

Full source

@[simp]
theorem withBot_comp (f : SupHom β γ) (g : SupHom α β) :
    (f.comp g).withBot = f.withBot.comp g.withBot :=
  DFunLike.coe_injective <| Eq.symm <| Option.map_comp_map _ _

Composition of Extended Supremum-Preserving Homomorphisms via `WithBot`

Informal description

For any two supremum-preserving homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the extension of their composition $f \circ g$ to homomorphisms between `WithBot` types is equal to the composition of their individual extensions. That is, $(f \circ g).\text{withBot} = f.\text{withBot} \circ g.\text{withBot}$.

SupHom.withTop' definition

[OrderTop β] (f : SupHom α β) : SupHom (WithTop α) β

Full source

/-- Adjoins a `⊤` to the codomain of a `SupHom`. -/
@[simps]
def withTop' [OrderTop β] (f : SupHom α β) : SupHom (WithTop α) β where
  toFun a := a.elim ⊤ f
  map_sup' a b :=
    match a, b with
    | ⊤, ⊤ => (top_sup_eq _).symm
    | ⊤, (b : α) => (top_sup_eq _).symm
    | (a : α), ⊤ => (sup_top_eq _).symm
    | (a : α), (b : α) => f.map_sup' _ _

Extension of a supremum-preserving homomorphism to include top elements

Informal description

Given a supremum-preserving homomorphism $f \colon \alpha \to \beta$ where $\beta$ has a top element $\top$, this definition extends $f$ to a supremum-preserving homomorphism from $\text{WithTop}\ \alpha$ to $\beta$. The extension maps $\top$ in $\text{WithTop}\ \alpha$ to $\top$ in $\beta$ and applies $f$ to the non-top elements of $\alpha$.

SupHom.withBot' definition

[OrderBot β] (f : SupHom α β) : SupBotHom (WithBot α) β

Full source

/-- Adjoins a `⊥` to the domain of a `SupHom`. -/
@[simps]
def withBot' [OrderBot β] (f : SupHom α β) : SupBotHom (WithBot α) β where
  toFun a := a.elim ⊥ f
  map_sup' a b :=
    match a, b with
    | ⊥, ⊥ => (bot_sup_eq _).symm
    | ⊥, (b : α) => (bot_sup_eq _).symm
    | (a : α), ⊥ => (sup_bot_eq _).symm
    | (a : α), (b : α) => f.map_sup' _ _
  map_bot' := rfl

Extension of a supremum-preserving homomorphism to include bottom elements

Informal description

Given a supremum-preserving homomorphism $f \colon \alpha \to \beta$ where $\beta$ has a bottom element $\bot$, this definition extends $f$ to a supremum- and bottom-preserving homomorphism from $\text{WithBot}\ \alpha$ to $\beta$. The extension maps $\bot$ in $\text{WithBot}\ \alpha$ to $\bot$ in $\beta$ and applies $f$ to the non-bottom elements of $\alpha$.

InfHom.withTop definition

(f : InfHom α β) : InfTopHom (WithTop α) (WithTop β)

Full source

/-- Adjoins a `⊤` to the domain and codomain of an `InfHom`. -/
@[simps]
protected def withTop (f : InfHom α β) : InfTopHom (WithTop α) (WithTop β) where
  toFun := Option.map f
  map_inf' a b :=
    match a, b with
    | ⊤, ⊤ => rfl
    | ⊤, (b : α) => rfl
    | (a : α), ⊤ => rfl
    | (a : α), (b : α) => congr_arg _ (f.map_inf' _ _)
  map_top' := rfl

Extension of an infimum-preserving function to include top elements

Informal description

Given an infimum-preserving function $f \colon \alpha \to \beta$, this definition extends $f$ to a function between the types $\text{WithTop}\ \alpha$ and $\text{WithTop}\ \beta$ that preserves both infima and the top element. The extension is defined by mapping $\top$ to $\top$ and applying $f$ to the non-top elements of $\alpha$.

InfHom.withTop_id theorem

: (InfHom.id α).withTop = InfTopHom.id _

Full source

@[simp]
theorem withTop_id : (InfHom.id α).withTop = InfTopHom.id _ := DFunLike.coe_injective Option.map_id

Identity Extension to WithTop Preserves Identity

Informal description

The extension of the identity infimum-preserving homomorphism on a type $\alpha$ to $\text{WithTop}\ \alpha$ is equal to the identity infimum- and top-preserving homomorphism on $\text{WithTop}\ \alpha$.

InfHom.withTop_comp theorem

(f : InfHom β γ) (g : InfHom α β) : (f.comp g).withTop = f.withTop.comp g.withTop

Full source

@[simp]
theorem withTop_comp (f : InfHom β γ) (g : InfHom α β) :
    (f.comp g).withTop = f.withTop.comp g.withTop :=
  DFunLike.coe_injective <| Eq.symm <| Option.map_comp_map _ _

Composition of Infimum-Preserving Functions Commutes with Top Extension

Informal description

Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be infimum-preserving functions. Then the extension of their composition $f \circ g$ to functions between $\text{WithTop}\ \alpha$ and $\text{WithTop}\ \gamma$ is equal to the composition of their individual extensions, i.e., $(f \circ g).\text{withTop} = f.\text{withTop} \circ g.\text{withTop}$.

InfHom.withBot definition

(f : InfHom α β) : InfHom (WithBot α) (WithBot β)

Full source

/-- Adjoins a `⊥` to the domain and codomain of an `InfHom`. -/
@[simps]
protected def withBot (f : InfHom α β) : InfHom (WithBot α) (WithBot β) where
  toFun := Option.map f
  map_inf' a b :=
    match a, b with
    | ⊥, ⊥ => rfl
    | ⊥, (b : α) => rfl
    | (a : α), ⊥ => rfl
    | (a : α), (b : α) => congr_arg _ (f.map_inf' _ _)

Extension of an infimum-preserving function with a bottom element

Informal description

Given an infimum-preserving function $f$ between types $\alpha$ and $\beta$, the function `InfHom.withBot` extends $f$ to a function between `WithBot α` and `WithBot β` by adjoining a bottom element `⊥` to both the domain and codomain. The extended function preserves infima, mapping `⊥` to `⊥` and applying $f$ to elements of $\alpha$.

InfHom.withBot_id theorem

: (InfHom.id α).withBot = InfHom.id _

Full source

@[simp]
theorem withBot_id : (InfHom.id α).withBot = InfHom.id _ := DFunLike.coe_injective Option.map_id

Identity Infimum-Preserving Homomorphism Commutes with Bottom Extension

Informal description

The extension of the identity infimum-preserving homomorphism on $\alpha$ to $\text{WithBot}\ \alpha$ is equal to the identity infimum-preserving homomorphism on $\text{WithBot}\ \alpha$. That is, $(\text{id}_\alpha)_{\text{withBot}} = \text{id}_{\text{WithBot}\ \alpha}$.

InfHom.withBot_comp theorem

(f : InfHom β γ) (g : InfHom α β) : (f.comp g).withBot = f.withBot.comp g.withBot

Full source

@[simp]
theorem withBot_comp (f : InfHom β γ) (g : InfHom α β) :
    (f.comp g).withBot = f.withBot.comp g.withBot :=
  DFunLike.coe_injective <| Eq.symm <| Option.map_comp_map _ _

Composition Commutes with Bottom Extension for Infimum-Preserving Functions

Informal description

For any infimum-preserving functions $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the extension of their composition $f \circ g$ with a bottom element is equal to the composition of their individual extensions with a bottom element. That is, $(f \circ g)_{\text{withBot}} = f_{\text{withBot}} \circ g_{\text{withBot}}$.

InfHom.withTop' definition

[OrderTop β] (f : InfHom α β) : InfTopHom (WithTop α) β

Full source

/-- Adjoins a `⊤` to the codomain of an `InfHom`. -/
@[simps]
def withTop' [OrderTop β] (f : InfHom α β) : InfTopHom (WithTop α) β where
  toFun a := a.elim ⊤ f
  map_inf' a b :=
    match a, b with
    | ⊤, ⊤ => (top_inf_eq _).symm
    | ⊤, (b : α) => (top_inf_eq _).symm
    | (a : α), ⊤ => (inf_top_eq _).symm
    | (a : α), (b : α) => f.map_inf' _ _
  map_top' := rfl

Extension of an infimum-preserving function to include a top element

Informal description

Given an infimum-preserving function $ f \colon \alpha \to \beta $ where $ \beta $ has a top element $ \top $, this definition extends $ f $ to a function $ \text{WithTop} \alpha \to \beta $ by mapping $ \top $ (the new top element in $ \text{WithTop} \alpha $) to $ \top $ in $ \beta $, and preserving the infimum operation for all other elements. The resulting function is an infimum- and top-preserving homomorphism.

InfHom.withBot' definition

[OrderBot β] (f : InfHom α β) : InfHom (WithBot α) β

Full source

/-- Adjoins a `⊥` to the codomain of an `InfHom`. -/
@[simps]
def withBot' [OrderBot β] (f : InfHom α β) : InfHom (WithBot α) β where
  toFun a := a.elim ⊥ f
  map_inf' a b :=
    match a, b with
    | ⊥, ⊥ => (bot_inf_eq _).symm
    | ⊥, (b : α) => (bot_inf_eq _).symm
    | (a : α), ⊥ => (inf_bot_eq _).symm
    | (a : α), (b : α) => f.map_inf' _ _

Extension of an infimum-preserving function to include a bottom element

Informal description

Given an infimum-preserving function $ f \colon \alpha \to \beta $ where $ \beta $ has a bottom element $ \bot $, this definition extends $ f $ to a function $ \text{WithBot} \alpha \to \beta $ by mapping $ \bot $ (the new bottom element in $ \text{WithBot} \alpha $) to $ \bot $ in $ \beta $, and preserving the infimum operation for all other elements. The resulting function is an infimum-preserving homomorphism.

LatticeHom.withTop definition

(f : LatticeHom α β) : LatticeHom (WithTop α) (WithTop β)

Full source

/-- Adjoins a `⊤` to the domain and codomain of a `LatticeHom`. -/
@[simps]
protected def withTop (f : LatticeHom α β) : LatticeHom (WithTop α) (WithTop β) :=
  { f.toInfHom.withTop with toSupHom := f.toSupHom.withTop }

Extension of a lattice homomorphism to include top elements

Informal description

Given a lattice homomorphism $f \colon \alpha \to \beta$, this definition extends $f$ to a lattice homomorphism between the types $\text{WithTop}\ \alpha$ and $\text{WithTop}\ \beta$ by adjoining a top element $\top$ to both the domain and codomain. The extended function maps $\top$ to $\top$ and applies $f$ to elements of $\alpha$, preserving both the supremum and infimum operations.

LatticeHom.coe_withTop theorem

(f : LatticeHom α β) : ⇑f.withTop = WithTop.map f

Full source

@[simp, norm_cast]
lemma coe_withTop (f : LatticeHom α β) : ⇑f.withTop = WithTop.map f := rfl

Coefficient Function of Extended Lattice Homomorphism with Top Element

Informal description

For any lattice homomorphism $f \colon \alpha \to \beta$, the underlying function of the extended homomorphism $f.\text{withTop} \colon \text{WithTop}\ \alpha \to \text{WithTop}\ \beta$ is equal to the map obtained by applying $f$ pointwise to elements of $\text{WithTop}\ \alpha$, where $\top$ is mapped to $\top$.

LatticeHom.withTop_apply theorem

(f : LatticeHom α β) (a : WithTop α) : f.withTop a = a.map f

Full source

lemma withTop_apply (f : LatticeHom α β) (a : WithTop α) : f.withTop a = a.map f := rfl

Application of Extended Lattice Homomorphism Preserves Mapping

Informal description

For any lattice homomorphism $f \colon \alpha \to \beta$ and any element $a$ in $\alpha$ extended with a top element $\top$, the application of the extended homomorphism $f.\text{withTop}$ to $a$ equals the result of applying the map $f$ to $a$ (where $\top$ is mapped to itself).

LatticeHom.withTop_id theorem

: (LatticeHom.id α).withTop = LatticeHom.id _

Full source

@[simp]
theorem withTop_id : (LatticeHom.id α).withTop = LatticeHom.id _ :=
  DFunLike.coe_injective Option.map_id

Identity Lattice Homomorphism Extension to WithTop Preserves Identity

Informal description

The extension of the identity lattice homomorphism on $\alpha$ to $\text{WithTop}\ \alpha$ is equal to the identity lattice homomorphism on $\text{WithTop}\ \alpha$.

LatticeHom.withTop_comp theorem

(f : LatticeHom β γ) (g : LatticeHom α β) : (f.comp g).withTop = f.withTop.comp g.withTop

Full source

@[simp]
theorem withTop_comp (f : LatticeHom β γ) (g : LatticeHom α β) :
    (f.comp g).withTop = f.withTop.comp g.withTop :=
  DFunLike.coe_injective <| Eq.symm <| Option.map_comp_map _ _

Composition of Extended Lattice Homomorphisms with Top Elements: $(f \circ g)_{\text{withTop}} = f_{\text{withTop}} \circ g_{\text{withTop}}$

Informal description

For any lattice homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the extension of their composition to lattices with top elements satisfies $(f \circ g)_{\text{withTop}} = f_{\text{withTop}} \circ g_{\text{withTop}}$. Here, $f_{\text{withTop}}$ and $g_{\text{withTop}}$ denote the extensions of $f$ and $g$ to lattices with top elements, respectively.

LatticeHom.withBot definition

(f : LatticeHom α β) : LatticeHom (WithBot α) (WithBot β)

Full source

/-- Adjoins a `⊥` to the domain and codomain of a `LatticeHom`. -/
@[simps]
protected def withBot (f : LatticeHom α β) : LatticeHom (WithBot α) (WithBot β) :=
  { f.toInfHom.withBot with toSupHom := f.toSupHom.withBot }

Extension of a lattice homomorphism with a bottom element

Informal description

Given a lattice homomorphism $f \colon \alpha \to \beta$, the function `LatticeHom.withBot` extends $f$ to a lattice homomorphism between the types `WithBot α` and `WithBot β` (which adjoin a bottom element $\bot$ to $\alpha$ and $\beta$ respectively). The extended homomorphism maps $\bot$ to $\bot$ and applies $f$ to the non-bottom elements, preserving both the supremum ($\sqcup$) and infimum ($\sqcap$) operations.

LatticeHom.coe_withBot theorem

(f : LatticeHom α β) : ⇑f.withBot = Option.map f

Full source

@[simp, norm_cast]
lemma coe_withBot (f : LatticeHom α β) : ⇑f.withBot = Option.map f := rfl

Function Representation of Extended Lattice Homomorphism with Bottom Element

Informal description

For any lattice homomorphism $f \colon \alpha \to \beta$, the underlying function of the extended homomorphism $f_{\text{withBot}} \colon \text{WithBot}\ \alpha \to \text{WithBot}\ \beta$ is equal to the option map of $f$. That is, for any $a \in \text{WithBot}\ \alpha$, we have $f_{\text{withBot}}(a) = \text{Option.map}\ f\ a$.

LatticeHom.withBot_apply theorem

(f : LatticeHom α β) (a : WithBot α) : f.withBot a = a.map f

Full source

lemma withBot_apply (f : LatticeHom α β) (a : WithBot α) : f.withBot a = a.map f := rfl

Application of Extended Lattice Homomorphism with Bottom Element

Informal description

Let $f \colon \alpha \to \beta$ be a lattice homomorphism between lattices $\alpha$ and $\beta$. For any element $a$ in the lattice $\alpha$ extended with a bottom element $\bot$ (denoted as `WithBot α`), the application of the extended homomorphism $f.\text{withBot}$ to $a$ is equal to applying the map $f$ to $a$ when $a$ is not $\bot$, and maps $\bot$ to $\bot$. In other words, $f.\text{withBot}(a) = \text{Option.map}\, f\, a$.

LatticeHom.withBot_id theorem

: (LatticeHom.id α).withBot = LatticeHom.id _

Full source

@[simp]
theorem withBot_id : (LatticeHom.id α).withBot = LatticeHom.id _ :=
  DFunLike.coe_injective Option.map_id

Identity Lattice Homomorphism Preserved Under Bottom Extension

Informal description

The extension of the identity lattice homomorphism on a lattice $\alpha$ to the lattice `WithBot α` (formed by adjoining a bottom element $\bot$ to $\alpha$) is equal to the identity lattice homomorphism on `WithBot α$.

LatticeHom.withBot_comp theorem

(f : LatticeHom β γ) (g : LatticeHom α β) : (f.comp g).withBot = f.withBot.comp g.withBot

Full source

@[simp]
theorem withBot_comp (f : LatticeHom β γ) (g : LatticeHom α β) :
    (f.comp g).withBot = f.withBot.comp g.withBot :=
  DFunLike.coe_injective <| Eq.symm <| Option.map_comp_map _ _

Composition of Extended Lattice Homomorphisms with Bottom Elements

Informal description

Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be lattice homomorphisms. Then the extension of their composition $f \circ g$ to lattices with bottom elements satisfies $(f \circ g).\text{withBot} = f.\text{withBot} \circ g.\text{withBot}$.

LatticeHom.withTopWithBot definition

(f : LatticeHom α β) : BoundedLatticeHom (WithTop <| WithBot α) (WithTop <| WithBot β)

Full source

/-- Adjoins a `⊤` and `⊥` to the domain and codomain of a `LatticeHom`. -/
@[simps]
def withTopWithBot (f : LatticeHom α β) :
    BoundedLatticeHom (WithTop <| WithBot α) (WithTop <| WithBot β) :=
  ⟨f.withBot.withTop, rfl, rfl⟩

Extension of a lattice homomorphism to include top and bottom elements

Informal description

Given a lattice homomorphism $f \colon \alpha \to \beta$, the function `LatticeHom.withTopWithBot` extends $f$ to a bounded lattice homomorphism between the types $\text{WithTop}(\text{WithBot}\ \alpha)$ and $\text{WithTop}(\text{WithBot}\ \beta)$. The extended homomorphism maps the top and bottom elements of the domain to their respective counterparts in the codomain, and applies $f$ to the non-extremal elements, preserving both the supremum and infimum operations.

LatticeHom.coe_withTopWithBot theorem

(f : LatticeHom α β) : ⇑f.withTopWithBot = Option.map (Option.map f)

Full source

@[simp, norm_cast]
lemma coe_withTopWithBot (f : LatticeHom α β) : ⇑f.withTopWithBot = Option.map (Option.map f) := rfl

Coefficient Function of Extended Lattice Homomorphism with Top and Bottom Elements

Informal description

For any lattice homomorphism $f \colon \alpha \to \beta$, the underlying function of the extended homomorphism $f.\text{withTopWithBot}$ is equal to the composition of two `Option.map` operations applied to $f$. That is, for any element $a$ in $\text{WithTop}(\text{WithBot}\ \alpha)$, the value $f.\text{withTopWithBot}(a)$ is obtained by first mapping $f$ over the inner `Option` (if $a$ is not `⊤$) and then mapping the result over the outer `Option`.

LatticeHom.withTopWithBot_apply theorem

(f : LatticeHom α β) (a : WithTop <| WithBot α) : f.withTopWithBot a = a.map (Option.map f)

Full source

lemma withTopWithBot_apply (f : LatticeHom α β) (a : WithTop <| WithBot α) :
    f.withTopWithBot a = a.map (Option.map f) := rfl

Action of Extended Lattice Homomorphism on Elements with Top and Bottom

Informal description

Let $f \colon \alpha \to \beta$ be a lattice homomorphism between lattices $\alpha$ and $\beta$. For any element $a$ in the lattice $\text{WithTop}(\text{WithBot}\ \alpha)$, the extended homomorphism $f.\text{withTopWithBot}$ satisfies: \[ f.\text{withTopWithBot}(a) = \text{map}(\text{map}\ f)(a) \] where the outer $\text{map}$ applies to the $\text{WithTop}$ structure and the inner $\text{map}$ applies to the $\text{WithBot}$ structure.

LatticeHom.withTopWithBot_id theorem

: (LatticeHom.id α).withTopWithBot = BoundedLatticeHom.id _

Full source

@[simp]
theorem withTopWithBot_id : (LatticeHom.id α).withTopWithBot = BoundedLatticeHom.id _ :=
  DFunLike.coe_injective <| by
    refine (congr_arg Option.map ?_).trans Option.map_id
    rw [withBot_id]
    rfl

Identity Lattice Homomorphism Preserved Under Top and Bottom Extension

Informal description

The extension of the identity lattice homomorphism on a lattice $\alpha$ to the lattice $\text{WithTop}(\text{WithBot}\ \alpha)$ (formed by adjoining both top and bottom elements to $\alpha$) is equal to the identity bounded lattice homomorphism on $\text{WithTop}(\text{WithBot}\ \alpha)$.

LatticeHom.withTopWithBot_comp theorem

(f : LatticeHom β γ) (g : LatticeHom α β) : (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot

Full source

@[simp]
theorem withTopWithBot_comp (f : LatticeHom β γ) (g : LatticeHom α β) :
    (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot := by
  ext; simp

Composition of Extended Lattice Homomorphisms Preserves Extension

Informal description

For any lattice homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the extension of their composition $f \circ g$ to include top and bottom elements is equal to the composition of their individual extensions. That is, \[ (f \circ g)\_{\text{WithTopWithBot}} = f\_{\text{WithTopWithBot}} \circ g\_{\text{WithTopWithBot}}. \]

LatticeHom.withTop' definition

[OrderTop β] (f : LatticeHom α β) : LatticeHom (WithTop α) β

Full source

/-- Adjoins a `⊥` to the codomain of a `LatticeHom`. -/
@[simps]
def withTop' [OrderTop β] (f : LatticeHom α β) : LatticeHom (WithTop α) β :=
  { f.toSupHom.withTop', f.toInfHom.withTop' with }

Extension of a lattice homomorphism to include a top element

Informal description

Given a lattice homomorphism $ f \colon \alpha \to \beta $ where $ \beta $ has a top element $ \top $, this definition extends $ f $ to a lattice homomorphism $ \text{WithTop} \alpha \to \beta $ by mapping $ \top $ (the new top element in $ \text{WithTop} \alpha $) to $ \top $ in $ \beta $, and preserving both the supremum and infimum operations for all other elements.

LatticeHom.withBot' definition

[OrderBot β] (f : LatticeHom α β) : LatticeHom (WithBot α) β

Full source

/-- Adjoins a `⊥` to the domain and codomain of a `LatticeHom`. -/
@[simps]
def withBot' [OrderBot β] (f : LatticeHom α β) : LatticeHom (WithBot α) β :=
  { f.toSupHom.withBot', f.toInfHom.withBot' with }

Extension of a lattice homomorphism to include a bottom element

Informal description

Given a lattice homomorphism $ f \colon \alpha \to \beta $ where $ \beta $ has a bottom element $ \bot $, this definition extends $ f $ to a lattice homomorphism $ \text{WithBot} \alpha \to \beta $ by mapping $ \bot $ (the new bottom element in $ \text{WithBot} \alpha $) to $ \bot $ in $ \beta $, and preserving both the supremum and infimum operations for all other elements.

LatticeHom.withTopWithBot' definition

[BoundedOrder β] (f : LatticeHom α β) : BoundedLatticeHom (WithTop <| WithBot α) β

Full source

/-- Adjoins a `⊤` and `⊥` to the codomain of a `LatticeHom`. -/
@[simps]
def withTopWithBot' [BoundedOrder β] (f : LatticeHom α β) :
    BoundedLatticeHom (WithTop <| WithBot α) β where
  toLatticeHom := f.withBot'.withTop'
  map_top' := rfl
  map_bot' := rfl

Extension of a lattice homomorphism to include both top and bottom elements

Informal description

Given a lattice homomorphism $ f \colon \alpha \to \beta $ where $ \beta $ is a bounded order (having both a top element $ \top $ and a bottom element $ \bot $), this definition extends $ f $ to a bounded lattice homomorphism $ \text{WithTop} (\text{WithBot} \alpha) \to \beta $. The extension maps the new top element in $ \text{WithTop} (\text{WithBot} \alpha) $ to $ \top $ in $ \beta $, the new bottom element to $ \bot $ in $ \beta $, and preserves both the supremum and infimum operations for all other elements.