doc-next-gen

Mathlib.Order.Hom.Bounded

Module docstring

{"# Bounded order homomorphisms

This file defines (bounded) order homomorphisms.

We use the DFunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

Types of morphisms

  • TopHom: Maps which preserve ⊤.
  • BotHom: Maps which preserve ⊥.
  • BoundedOrderHom: Bounded order homomorphisms. Monotone maps which preserve ⊤ and ⊥.

Typeclasses

  • TopHomClass
  • BotHomClass
  • BoundedOrderHomClass ","### Top homomorphisms ","### Bot homomorphisms ","### Bounded order homomorphisms ","### Dual homs "}
TopHom structure
(α β : Type*) [Top α] [Top β]
Full source 
/-- The type of `⊤`-preserving functions from `α` to `β`. -/
structure TopHom (α β : Type*) [Top α] [Top β] where
  /-- The underlying function. The preferred spelling is `DFunLike.coe`. -/
  toFun : α → β
  /-- The function preserves the top element. The preferred spelling is `map_top`. -/
  map_top' : toFun ⊤ = ⊤
Top-preserving functions
Informal description
The structure representing functions from a type `α` with a top element `⊤` to a type `β` with a top element `⊤`, that preserve the top element. In other words, a function `f : α → β` is a `TopHom` if it satisfies `f ⊤ = ⊤`.
BotHom structure
(α β : Type*) [Bot α] [Bot β]
Full source 
/-- The type of `⊥`-preserving functions from `α` to `β`. -/
structure BotHom (α β : Type*) [Bot α] [Bot β] where
  /-- The underlying function. The preferred spelling is `DFunLike.coe`. -/
  toFun : α → β
  /-- The function preserves the bottom element. The preferred spelling is `map_bot`. -/
  map_bot' : toFun ⊥ = ⊥
Bottom-preserving functions
Informal description
The structure representing functions from a type $\alpha$ with a bottom element $\bot$ to a type $\beta$ with a bottom element $\bot$, that preserve the bottom element.
BoundedOrderHom structure
(α β : Type*) [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] extends OrderHom α β
Full source 
/-- The type of bounded order homomorphisms from `α` to `β`. -/
structure BoundedOrderHom (α β : Type*) [Preorder α] [Preorder β] [BoundedOrder α]
  [BoundedOrder β] extends OrderHom α β where
  /-- The function preserves the top element. The preferred spelling is `map_top`. -/
  map_top' : toFun ⊤ = ⊤
  /-- The function preserves the bottom element. The preferred spelling is `map_bot`. -/
  map_bot' : toFun ⊥ = ⊥
Bounded Order Homomorphism
Informal description
The structure representing bounded order homomorphisms from a preordered set $\alpha$ with both a greatest element $\top$ and a least element $\bot$ to another preordered set $\beta$ with the same bounded order structure. These are monotone functions that preserve both the top and bottom elements, i.e., a function $f \colon \alpha \to \beta$ is a bounded order homomorphism if it is monotone and satisfies $f(\top) = \top$ and $f(\bot) = \bot$.
TopHomClass structure
(F : Type*) (α β : outParam Type*) [Top α] [Top β] [FunLike F α β]
Full source 
/-- `TopHomClass F α β` states that `F` is a type of `⊤`-preserving morphisms.

You should extend this class when you extend `TopHom`. -/
class TopHomClass (F : Type*) (α β : outParam Type*) [Top α] [Top β] [FunLike F α β] :
    Prop where
  /-- A `TopHomClass` morphism preserves the top element. -/
  map_top (f : F) : f ⊤ = ⊤
Top-preserving morphism class
Informal description
The class `TopHomClass F α β` states that `F` is a type of morphisms from a type `α` with a top element `⊤` to a type `β` with a top element `⊤`, where each morphism in `F` preserves the top element.
BotHomClass structure
(F : Type*) (α β : outParam Type*) [Bot α] [Bot β] [FunLike F α β]
Full source 
/-- `BotHomClass F α β` states that `F` is a type of `⊥`-preserving morphisms.

You should extend this class when you extend `BotHom`. -/
class BotHomClass (F : Type*) (α β : outParam Type*) [Bot α] [Bot β] [FunLike F α β] :
    Prop where
  /-- A `BotHomClass` morphism preserves the bottom element. -/
  map_bot (f : F) : f ⊥ = ⊥
Bottom-preserving morphism class
Informal description
The class `BotHomClass F α β` states that `F` is a type of morphisms from a type `α` with a bottom element `⊥` to a type `β` with a bottom element `⊥`, where each morphism in `F` preserves the bottom element. This means for any `f : F`, we have `f(⊥) = ⊥`.
BoundedOrderHomClass structure
(F α β : Type*) [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [FunLike F α β] : Prop extends RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop)
Full source 
/-- `BoundedOrderHomClass F α β` states that `F` is a type of bounded order morphisms.

You should extend this class when you extend `BoundedOrderHom`. -/
class BoundedOrderHomClass (F α β : Type*) [LE α] [LE β]
    [BoundedOrder α] [BoundedOrder β] [FunLike F α β] : Prop
  extends RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop) where
  /-- Morphisms preserve the top element. The preferred spelling is `_root_.map_top`. -/
  map_top (f : F) : f ⊤ = ⊤
  /-- Morphisms preserve the bottom element. The preferred spelling is `_root_.map_bot`. -/
  map_bot (f : F) : f ⊥ = ⊥
Bounded Order Homomorphism Class
Informal description
The class `BoundedOrderHomClass F α β` states that `F` is a type of bounded order homomorphisms between types `α` and `β`, where both `α` and `β` are equipped with a partial order and have both a greatest element (⊤) and a least element (⊥). A bounded order homomorphism is a monotone function that preserves both the top and bottom elements.
BoundedOrderHomClass.toTopHomClass instance
[LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] : TopHomClass F α β
Full source 
instance (priority := 100) BoundedOrderHomClass.toTopHomClass [LE α] [LE β]
    [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] : TopHomClass F α β :=
  { ‹BoundedOrderHomClass F α β› with }
Bounded Order Homomorphisms Preserve Top Elements
Informal description
For any types $\alpha$ and $\beta$ equipped with partial orders and bounded order structures, every bounded order homomorphism from $\alpha$ to $\beta$ preserves the top element $\top$.
BoundedOrderHomClass.toBotHomClass instance
[LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] : BotHomClass F α β
Full source 
instance (priority := 100) BoundedOrderHomClass.toBotHomClass [LE α] [LE β]
    [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] : BotHomClass F α β :=
  { ‹BoundedOrderHomClass F α β› with }
Bounded Order Homomorphisms Preserve Bottom Elements
Informal description
For any types $\alpha$ and $\beta$ equipped with partial orders and bounded order structures, every bounded order homomorphism from $\alpha$ to $\beta$ preserves the bottom element $\bot$.
OrderIsoClass.toTopHomClass instance
[LE α] [OrderTop α] [PartialOrder β] [OrderTop β] [OrderIsoClass F α β] : TopHomClass F α β
Full source 
instance (priority := 100) OrderIsoClass.toTopHomClass [LE α] [OrderTop α]
    [PartialOrder β] [OrderTop β] [OrderIsoClass F α β] : TopHomClass F α β :=
  { show OrderHomClass F α β from inferInstance with
    map_top := fun f => top_le_iff.1 <| (map_inv_le_iff f).1 le_top }
Order Isomorphisms Preserve Top Elements
Informal description
For any types $\alpha$ and $\beta$ equipped with partial orders and top elements, every order isomorphism from $\alpha$ to $\beta$ preserves the top element $\top$.
OrderIsoClass.toBotHomClass instance
[LE α] [OrderBot α] [PartialOrder β] [OrderBot β] [OrderIsoClass F α β] : BotHomClass F α β
Full source 
instance (priority := 100) OrderIsoClass.toBotHomClass [LE α] [OrderBot α]
    [PartialOrder β] [OrderBot β] [OrderIsoClass F α β] : BotHomClass F α β :=
  { map_bot := fun f => le_bot_iff.1 <| (le_map_inv_iff f).1 bot_le }
Order Isomorphisms Preserve Bottom Elements
Informal description
For any types $\alpha$ and $\beta$ equipped with partial orders and bottom elements, every order isomorphism from $\alpha$ to $\beta$ preserves the bottom element $\bot$.
OrderIsoClass.toBoundedOrderHomClass instance
[LE α] [BoundedOrder α] [PartialOrder β] [BoundedOrder β] [OrderIsoClass F α β] : BoundedOrderHomClass F α β
Full source 
instance (priority := 100) OrderIsoClass.toBoundedOrderHomClass [LE α] [BoundedOrder α]
    [PartialOrder β] [BoundedOrder β] [OrderIsoClass F α β] : BoundedOrderHomClass F α β :=
  { show OrderHomClass F α β from inferInstance, OrderIsoClass.toTopHomClass,
    OrderIsoClass.toBotHomClass with }
Order Isomorphisms Preserve Bounded Order Structure
Informal description
For any types $\alpha$ and $\beta$ equipped with partial orders and both top and bottom elements, every order isomorphism from $\alpha$ to $\beta$ is a bounded order homomorphism, meaning it preserves both the top element $\top$ and the bottom element $\bot$.
map_eq_top_iff theorem
[LE α] [OrderTop α] [PartialOrder β] [OrderTop β] [OrderIsoClass F α β] (f : F) {a : α} : f a = ⊤ ↔ a = ⊤
Full source 
@[simp]
theorem map_eq_top_iff [LE α] [OrderTop α] [PartialOrder β] [OrderTop β] [OrderIsoClass F α β]
    (f : F) {a : α} : f a = ⊤ ↔ a = ⊤ := by
  rw [← map_top f, (EquivLike.injective f).eq_iff]
Order isomorphism preserves top element
Informal description
Let $\alpha$ and $\beta$ be partially ordered sets with top elements $\top_\alpha$ and $\top_\beta$ respectively, and let $F$ be a class of order isomorphisms between $\alpha$ and $\beta$. For any order isomorphism $f \in F$ and any element $a \in \alpha$, we have $f(a) = \top_\beta$ if and only if $a = \top_\alpha$.
map_eq_bot_iff theorem
[LE α] [OrderBot α] [PartialOrder β] [OrderBot β] [OrderIsoClass F α β] (f : F) {a : α} : f a = ⊥ ↔ a = ⊥
Full source 
@[simp]
theorem map_eq_bot_iff [LE α] [OrderBot α] [PartialOrder β] [OrderBot β] [OrderIsoClass F α β]
    (f : F) {a : α} : f a = ⊥ ↔ a = ⊥ := by
  rw [← map_bot f, (EquivLike.injective f).eq_iff]
Order isomorphism preserves bottom element
Informal description
Let $\alpha$ and $\beta$ be partially ordered sets with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively, and let $F$ be a type of order isomorphisms between $\alpha$ and $\beta$. For any order isomorphism $f \in F$ and any element $a \in \alpha$, we have $f(a) = \bot_\beta$ if and only if $a = \bot_\alpha$.
TopHomClass.toTopHom definition
[Top α] [Top β] [TopHomClass F α β] (f : F) : TopHom α β
Full source 
/-- Turn an element of a type `F` satisfying `TopHomClass F α β` into an actual
`TopHom`. This is declared as the default coercion from `F` to `TopHom α β`. -/
@[coe]
def TopHomClass.toTopHom [Top α] [Top β] [TopHomClass F α β] (f : F) : TopHom α β :=
  ⟨f, map_top f⟩
Conversion from `TopHomClass` to `TopHom`
Informal description
Given a type `F` satisfying `TopHomClass F α β`, this function converts an element `f : F` into an actual `TopHom α β`. The resulting top-preserving function satisfies `f(⊤) = ⊤`.
instCoeTCTopHomOfTopHomClass instance
[Top α] [Top β] [TopHomClass F α β] : CoeTC F (TopHom α β)
Full source 
instance [Top α] [Top β] [TopHomClass F α β] : CoeTC F (TopHom α β) :=
  ⟨TopHomClass.toTopHom⟩
Canonical View of Top-Preserving Morphisms as Top-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ with top elements $\top_\alpha$ and $\top_\beta$ respectively, and any type $F$ of top-preserving morphisms from $\alpha$ to $\beta$, there is a canonical way to view an element of $F$ as a top-preserving function from $\alpha$ to $\beta$.
BotHomClass.toBotHom definition
[Bot α] [Bot β] [BotHomClass F α β] (f : F) : BotHom α β
Full source 
/-- Turn an element of a type `F` satisfying `BotHomClass F α β` into an actual
`BotHom`. This is declared as the default coercion from `F` to `BotHom α β`. -/
@[coe]
def BotHomClass.toBotHom [Bot α] [Bot β] [BotHomClass F α β] (f : F) : BotHom α β :=
  ⟨f, map_bot f⟩
Conversion from `BotHomClass` to `BotHom`
Informal description
Given a type `F` satisfying `BotHomClass F α β`, this function converts an element `f : F` into an actual `BotHom α β`. The resulting bottom-preserving function satisfies `f(⊥) = ⊥`.
instCoeTCBotHomOfBotHomClass instance
[Bot α] [Bot β] [BotHomClass F α β] : CoeTC F (BotHom α β)
Full source 
instance [Bot α] [Bot β] [BotHomClass F α β] : CoeTC F (BotHom α β) :=
  ⟨BotHomClass.toBotHom⟩
Canonical Coercion from Bottom-Preserving Function Class to Bottom-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ with bottom elements $\bot$, and any type $F$ that satisfies `BotHomClass F α β`, there is a canonical coercion from $F$ to the type of bottom-preserving functions $\text{BotHom} \alpha \beta$. This means any element $f : F$ can be treated as a function that preserves the bottom element, i.e., $f(\bot) = \bot$.
BoundedOrderHomClass.toBoundedOrderHom definition
[Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] (f : F) : BoundedOrderHom α β
Full source 
/-- Turn an element of a type `F` satisfying `BoundedOrderHomClass F α β` into an actual
`BoundedOrderHom`. This is declared as the default coercion from `F` to `BoundedOrderHom α β`. -/
@[coe]
def BoundedOrderHomClass.toBoundedOrderHom [Preorder α] [Preorder β] [BoundedOrder α]
    [BoundedOrder β] [BoundedOrderHomClass F α β] (f : F) : BoundedOrderHom α β :=
  { (f : α →o β) with toFun := f, map_top' := map_top f, map_bot' := map_bot f }
Conversion from BoundedOrderHomClass to BoundedOrderHom
Informal description
Given a type `F` satisfying `BoundedOrderHomClass F α β`, this function converts an element `f : F` into an actual `BoundedOrderHom α β`. The resulting bounded order homomorphism preserves both the greatest element (⊤) and the least element (⊥), and is monotone with respect to the preorders on `α` and `β`.
instCoeTCBoundedOrderHomOfBoundedOrderHomClass instance
[Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] : CoeTC F (BoundedOrderHom α β)
Full source 
instance [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
    CoeTC F (BoundedOrderHom α β) :=
  ⟨BoundedOrderHomClass.toBoundedOrderHom⟩
Canonical Coercion from Bounded Order Homomorphism Class to Bounded Order Homomorphisms
Informal description
For any preordered sets $\alpha$ and $\beta$ with bounded order structures (having both a greatest element $\top$ and a least element $\bot$), and any type $F$ that satisfies `BoundedOrderHomClass F α β`, there is a canonical coercion from $F$ to the type of bounded order homomorphisms $\text{BoundedOrderHom} \alpha \beta$. This means any element $f : F$ can be treated as a bounded order homomorphism that preserves both $\top$ and $\bot$ and is monotone with respect to the preorders on $\alpha$ and $\beta$.
TopHom.instFunLike instance
: FunLike (TopHom α β) α β
Full source 
instance : FunLike (TopHom α β) α β where
  coe := TopHom.toFun
  coe_injective' f g h := by cases f; cases g; congr
Function-Like Structure for Top-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ equipped with top elements, the type of top-preserving functions $\text{TopHom} \alpha \beta$ has a function-like structure, meaning it can be coerced to a function from $\alpha$ to $\beta$.
TopHom.instTopHomClass instance
: TopHomClass (TopHom α β) α β
Full source 
instance : TopHomClass (TopHom α β) α β where
  map_top := TopHom.map_top'
Top-Preserving Functions as Top Homomorphisms
Informal description
For any types $\alpha$ and $\beta$ equipped with top elements, the type of top-preserving functions $\text{TopHom} \alpha \beta$ forms a `TopHomClass`, meaning every function in this type preserves the top element.
TopHom.ext theorem
{f g : TopHom α β} (h : ∀ a, f a = g a) : f = g
Full source 
@[ext]
theorem ext {f g : TopHom α β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h
Extensionality of Top-Preserving Functions
Informal description
For any two top-preserving functions $f, g : \alpha \to \beta$ between types $\alpha$ and $\beta$ with top elements, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.
TopHom.copy definition
(f : TopHom α β) (f' : α → β) (h : f' = f) : TopHom α β
Full source 
/-- Copy of a `TopHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : TopHom α β) (f' : α → β) (h : f' = f) :
    TopHom α β where
  toFun := f'
  map_top' := h.symm ▸ f.map_top'
Copy of a top-preserving function with a new representation
Informal description
Given a top-preserving function $f : \alpha \to \beta$ (where $\alpha$ and $\beta$ are types with top elements) and a function $f' : \alpha \to \beta$ that is definitionally equal to $f$, the function `TopHom.copy` constructs a new top-preserving function with the same behavior as $f$ but represented by $f'$. This is useful for maintaining definitional equalities when working with top-preserving functions.
TopHom.coe_copy theorem
(f : TopHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f'
Full source 
@[simp]
theorem coe_copy (f : TopHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl
Underlying function of copied top-homomorphism equals copied function
Informal description
Let $f : \alpha \to \beta$ be a top-preserving function between types $\alpha$ and $\beta$ with top elements, and let $f' : \alpha \to \beta$ be a function such that $f' = f$. Then the underlying function of the copied top-homomorphism $f.copy\ f'\ h$ is equal to $f'$.
TopHom.copy_eq theorem
(f : TopHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f
Full source 
theorem copy_eq (f : TopHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h
Copy of Top-Preserving Function Equals Original
Informal description
For any top-preserving function $f \colon \alpha \to \beta$ between types $\alpha$ and $\beta$ with top elements, and any function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with representation $f'$ is equal to $f$ itself.
TopHom.instInhabited instance
: Inhabited (TopHom α β)
Full source 
instance : Inhabited (TopHom α β) :=
  ⟨⟨fun _ => ⊤, rfl⟩⟩
Inhabitedness of Top-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ equipped with top elements $\top$, the type of top-preserving functions from $\alpha$ to $\beta$ is inhabited.
TopHom.id definition
: TopHom α α
Full source 
/-- `id` as a `TopHom`. -/
protected def id : TopHom α α :=
  ⟨id, rfl⟩
Identity as a top-preserving function
Informal description
The identity function on a type $\alpha$ with a top element $\top$, viewed as a top-preserving function. This means it satisfies $\text{id}(\top) = \top$.
TopHom.coe_id theorem
: ⇑(TopHom.id α) = id
Full source 
@[simp, norm_cast]
theorem coe_id : ⇑(TopHom.id α) = id :=
  rfl
Identity Top-Preserving Function Coerces to Identity Function
Informal description
The coercion of the identity top-preserving function on a type $\alpha$ with a top element $\top$ is equal to the identity function, i.e., $\text{id}_{\text{TopHom}} = \text{id}$.
TopHom.id_apply theorem
(a : α) : TopHom.id α a = a
Full source 
@[simp]
theorem id_apply (a : α) : TopHom.id α a = a :=
  rfl
Identity Top-Preserving Function Evaluation
Informal description
For any element $a$ in a type $\alpha$ with a top element $\top$, the identity top-preserving function evaluated at $a$ is equal to $a$, i.e., $\text{id}(a) = a$.
TopHom.comp definition
(f : TopHom β γ) (g : TopHom α β) : TopHom α γ
Full source 
/-- Composition of `TopHom`s as a `TopHom`. -/
def comp (f : TopHom β γ) (g : TopHom α β) :
    TopHom α γ where
  toFun := f ∘ g
  map_top' := by rw [comp_apply, map_top, map_top]
Composition of top-preserving functions
Informal description
The composition of two top-preserving functions \( f : \beta \to \gamma \) and \( g : \alpha \to \beta \), denoted \( f \circ g \), is again a top-preserving function from \( \alpha \) to \( \gamma \). This means that if \( g \) preserves the top element of \( \alpha \) and \( f \) preserves the top element of \( \beta \), then their composition \( f \circ g \) preserves the top element of \( \alpha \).
TopHom.coe_comp theorem
(f : TopHom β γ) (g : TopHom α β) : (f.comp g : α → γ) = f ∘ g
Full source 
@[simp]
theorem coe_comp (f : TopHom β γ) (g : TopHom α β) : (f.comp g : α → γ) = f ∘ g :=
  rfl
Composition of Top-Preserving Functions as Pointwise Composition
Informal description
For any top-preserving functions $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the composition $f \circ g$ as a function from $\alpha$ to $\gamma$ is equal to the pointwise composition of $f$ and $g$.
TopHom.comp_apply theorem
(f : TopHom β γ) (g : TopHom α β) (a : α) : (f.comp g) a = f (g a)
Full source 
@[simp]
theorem comp_apply (f : TopHom β γ) (g : TopHom α β) (a : α) : (f.comp g) a = f (g a) :=
  rfl
Evaluation of Composition of Top-Preserving Functions
Informal description
For any top-preserving functions $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, and for any element $a \in \alpha$, the composition $f \circ g$ evaluated at $a$ equals $f$ evaluated at $g(a)$, i.e., $(f \circ g)(a) = f(g(a))$.
TopHom.comp_assoc theorem
(f : TopHom γ δ) (g : TopHom β γ) (h : TopHom α β) : (f.comp g).comp h = f.comp (g.comp h)
Full source 
@[simp]
theorem comp_assoc (f : TopHom γ δ) (g : TopHom β γ) (h : TopHom α β) :
    (f.comp g).comp h = f.comp (g.comp h) :=
  rfl
Associativity of Composition for Top-Preserving Functions
Informal description
For any top-preserving functions $f \colon \gamma \to \delta$, $g \colon \beta \to \gamma$, and $h \colon \alpha \to \beta$, the composition operation satisfies the associativity property $(f \circ g) \circ h = f \circ (g \circ h)$.
TopHom.comp_id theorem
(f : TopHom α β) : f.comp (TopHom.id α) = f
Full source 
@[simp]
theorem comp_id (f : TopHom α β) : f.comp (TopHom.id α) = f :=
  TopHom.ext fun _ => rfl
Identity Top-Preserving Function is Right Identity for Composition
Informal description
For any top-preserving function $f \colon \alpha \to \beta$, the composition of $f$ with the identity top-preserving function on $\alpha$ equals $f$, i.e., $f \circ \text{id}_\alpha = f$.
TopHom.id_comp theorem
(f : TopHom α β) : (TopHom.id β).comp f = f
Full source 
@[simp]
theorem id_comp (f : TopHom α β) : (TopHom.id β).comp f = f :=
  TopHom.ext fun _ => rfl
Identity Top-Preserving Function is Left Identity for Composition
Informal description
For any top-preserving function $f \colon \alpha \to \beta$, the composition of the identity top-preserving function on $\beta$ with $f$ is equal to $f$, i.e., $\text{id}_\beta \circ f = f$.
TopHom.cancel_right theorem
{g₁ g₂ : TopHom β γ} {f : TopHom α β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂
Full source 
@[simp]
theorem cancel_right {g₁ g₂ : TopHom β γ} {f : TopHom α β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => TopHom.ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (fun g => comp g f)⟩
Right Cancellation Property for Composition of Top-Preserving Functions
Informal description
Let $f \colon \alpha \to \beta$ be a surjective top-preserving function, and let $g_1, g_2 \colon \beta \to \gamma$ be top-preserving functions. Then the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.
TopHom.cancel_left theorem
{g : TopHom β γ} {f₁ f₂ : TopHom α β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
Full source 
@[simp]
theorem cancel_left {g : TopHom β γ} {f₁ f₂ : TopHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => TopHom.ext fun a => hg <| by rw [← TopHom.comp_apply, h, TopHom.comp_apply],
    congr_arg _⟩
Left Cancellation for Composition of Top-Preserving Functions
Informal description
Let $g \colon \beta \to \gamma$ be an injective top-preserving function, and let $f_1, f_2 \colon \alpha \to \beta$ be top-preserving functions. Then the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.
TopHom.instLE instance
[LE β] [Top β] : LE (TopHom α β)
Full source 
instance instLE [LE β] [Top β] : LE (TopHom α β) where
  le f g := (f : α → β) ≤ g
Partial Order on Top-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ equipped with a top element $\top$ and a partial order $\leq$ on $\beta$, the type of top-preserving functions $\text{TopHom} \alpha \beta$ is equipped with a partial order structure where $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x \in \alpha$.
TopHom.instPreorder instance
[Preorder β] [Top β] : Preorder (TopHom α β)
Full source 
instance [Preorder β] [Top β] : Preorder (TopHom α β) :=
  Preorder.lift (DFunLike.coe : TopHom α β → α → β)
Preorder Structure on Top-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ where $\beta$ is equipped with a preorder and a top element $\top$, the type of top-preserving functions $\text{TopHom} \alpha \beta$ is equipped with a preorder structure where $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x \in \alpha$.
TopHom.instPartialOrder instance
[PartialOrder β] [Top β] : PartialOrder (TopHom α β)
Full source 
instance [PartialOrder β] [Top β] : PartialOrder (TopHom α β) :=
  PartialOrder.lift _ DFunLike.coe_injective
Partial Order on Top-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ where $\beta$ is equipped with a partial order and a top element $\top$, the type of top-preserving functions $\text{TopHom} \alpha \beta$ is equipped with a partial order structure where $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x \in \alpha$.
TopHom.instOrderTop instance
: OrderTop (TopHom α β)
Full source 
instance : OrderTop (TopHom α β) where
  top := ⟨⊤, rfl⟩
  le_top := fun _ => @le_top (α → β) _ _ _
Top-Preserving Functions Form an Order with Top Element
Informal description
For any types $\alpha$ and $\beta$ where $\beta$ is equipped with a top element $\top$ and a partial order, the type of top-preserving functions $\text{TopHom} \alpha \beta$ is an order with a top element. The top element in $\text{TopHom} \alpha \beta$ is the constant function that maps every element of $\alpha$ to $\top \in \beta$.
TopHom.coe_top theorem
: ⇑(⊤ : TopHom α β) = ⊤
Full source 
@[simp]
theorem coe_top : ⇑(⊤ : TopHom α β) = ⊤ :=
  rfl
Top Element of Top-Preserving Functions is the Constant Top Function
Informal description
The top element in the order of top-preserving functions from $\alpha$ to $\beta$ is the constant function that maps every element of $\alpha$ to the top element $\top$ in $\beta$.
TopHom.top_apply theorem
(a : α) : (⊤ : TopHom α β) a = ⊤
Full source 
@[simp]
theorem top_apply (a : α) : (⊤ : TopHom α β) a = ⊤ :=
  rfl
Top-Preserving Function Evaluates to Top Element
Informal description
For any element $a$ in a type $\alpha$ with a top element $\top$, the top-preserving function $\top \colon \text{TopHom} \alpha \beta$ evaluated at $a$ equals the top element $\top$ in $\beta$, i.e., $\top(a) = \top$.
TopHom.instSemilatticeInf instance
: SemilatticeInf (TopHom α β)
Full source 
instance : SemilatticeInf (TopHom α β) :=
  (DFunLike.coe_injective.semilatticeInf _) fun _ _ => rfl
Meet-Semilattice Structure on Top-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ equipped with top elements, the type of top-preserving functions $\text{TopHom} \alpha \beta$ forms a meet-semilattice, where the meet operation is defined pointwise.
TopHom.coe_inf theorem
: ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
Full source 
@[simp]
theorem coe_inf : ⇑(f ⊓ g) = ⇑f ⊓ ⇑g :=
  rfl
Infimum of Top-Preserving Functions is Pointwise Infimum
Informal description
For any top-preserving functions $f, g : \alpha \to \beta$ between types $\alpha$ and $\beta$ with top elements, the function corresponding to the infimum of $f$ and $g$ is equal to the pointwise infimum of the functions $f$ and $g$, i.e., $(f \sqcap g)(x) = f(x) \sqcap g(x)$ for all $x \in \alpha$.
TopHom.inf_apply theorem
(a : α) : (f ⊓ g) a = f a ⊓ g a
Full source 
@[simp]
theorem inf_apply (a : α) : (f ⊓ g) a = f a ⊓ g a :=
  rfl
Infimum of Top-Preserving Functions at a Point
Informal description
For any top-preserving functions $f, g : \alpha \to \beta$ between types $\alpha$ and $\beta$ with top elements, and for any element $a \in \alpha$, the infimum of $f$ and $g$ evaluated at $a$ equals the infimum of $f(a)$ and $g(a)$, i.e., $(f \sqcap g)(a) = f(a) \sqcap g(a)$.
TopHom.instSemilatticeSup instance
: SemilatticeSup (TopHom α β)
Full source 
instance : SemilatticeSup (TopHom α β) :=
  (DFunLike.coe_injective.semilatticeSup _) fun _ _ => rfl
Semilattice Structure on Top-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ equipped with top elements, the type of top-preserving functions $\text{TopHom} \alpha \beta$ forms a semilattice with respect to the supremum operation. This means that for any two top-preserving functions $f, g : \alpha \to \beta$, their supremum $f \sqcup g$ is also a top-preserving function, and the supremum operation is associative, commutative, and idempotent.
TopHom.coe_sup theorem
: ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
Full source 
@[simp]
theorem coe_sup : ⇑(f ⊔ g) = ⇑f ⊔ ⇑g :=
  rfl
Supremum of Top-Preserving Functions is Pointwise Supremum
Informal description
For any two top-preserving functions $f, g : \alpha \to \beta$ between types with top elements, the underlying function of their supremum $f \sqcup g$ is equal to the pointwise supremum of the underlying functions of $f$ and $g$. In other words, $(f \sqcup g)(x) = f(x) \sqcup g(x)$ for all $x \in \alpha$.
TopHom.sup_apply theorem
(a : α) : (f ⊔ g) a = f a ⊔ g a
Full source 
@[simp]
theorem sup_apply (a : α) : (f ⊔ g) a = f a ⊔ g a :=
  rfl
Pointwise Supremum of Top-Preserving Functions
Informal description
For any two top-preserving functions $f, g : \alpha \to \beta$ between types with top elements, and for any element $a \in \alpha$, the evaluation of their supremum at $a$ equals the supremum of their evaluations at $a$, i.e., $(f \sqcup g)(a) = f(a) \sqcup g(a)$.
TopHom.instLattice instance
[Lattice β] [OrderTop β] : Lattice (TopHom α β)
Full source 
instance [Lattice β] [OrderTop β] : Lattice (TopHom α β) :=
  DFunLike.coe_injective.lattice _ (fun _ _ => rfl) fun _ _ => rfl
Lattice Structure on Top-Preserving Functions
Informal description
For any lattice $\beta$ with a top element $\top$, the type of top-preserving functions $\text{TopHom}(\alpha, \beta)$ forms a lattice.
TopHom.instDistribLattice instance
[DistribLattice β] [OrderTop β] : DistribLattice (TopHom α β)
Full source 
instance [DistribLattice β] [OrderTop β] : DistribLattice (TopHom α β) :=
  DFunLike.coe_injective.distribLattice _ (fun _ _ => rfl) fun _ _ => rfl
Distributive Lattice Structure on Top-Preserving Functions
Informal description
For any distributive lattice $\beta$ with a top element $\top$, the type of top-preserving functions $\text{TopHom}(\alpha, \beta)$ forms a distributive lattice.
BotHom.instFunLike instance
: FunLike (BotHom α β) α β
Full source 
instance : FunLike (BotHom α β) α β where
  coe := BotHom.toFun
  coe_injective' f g h := by cases f; cases g; congr
Function-Like Structure on Bottom-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ equipped with bottom elements $\bot$, the type `BotHom α β` of bottom-preserving functions from $\alpha$ to $\beta$ has a function-like structure, meaning its elements can be coerced to functions from $\alpha$ to $\beta$ in an injective way.
BotHom.instBotHomClass instance
: BotHomClass (BotHom α β) α β
Full source 
instance : BotHomClass (BotHom α β) α β where
  map_bot := BotHom.map_bot'
Bottom-Preserving Functions Form a `BotHomClass`
Informal description
For any types $\alpha$ and $\beta$ with bottom elements $\bot$, the type `BotHom α β` of bottom-preserving functions from $\alpha$ to $\beta$ forms a `BotHomClass`. This means every function in `BotHom α β` preserves the bottom element, i.e., maps $\bot_\alpha$ to $\bot_\beta$.
BotHom.ext theorem
{f g : BotHom α β} (h : ∀ a, f a = g a) : f = g
Full source 
@[ext]
theorem ext {f g : BotHom α β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h
Extensionality of Bottom-Preserving Functions
Informal description
For any two bottom-preserving functions $f, g : \text{BotHom}(\alpha, \beta)$, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.
BotHom.copy definition
(f : BotHom α β) (f' : α → β) (h : f' = f) : BotHom α β
Full source 
/-- Copy of a `BotHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : BotHom α β) (f' : α → β) (h : f' = f) :
    BotHom α β where
  toFun := f'
  map_bot' := h.symm ▸ f.map_bot'
Copy of a bottom-preserving function with a new underlying function
Informal description
Given a bottom-preserving function $f$ from a type $\alpha$ with a bottom element $\bot$ to a type $\beta$ with a bottom element $\bot$, and a function $f'$ that is definitionally equal to $f$, the function `BotHom.copy` constructs a new bottom-preserving function with $f'$ as its underlying function, ensuring that it still preserves the bottom element.
BotHom.coe_copy theorem
(f : BotHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f'
Full source 
@[simp]
theorem coe_copy (f : BotHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl
Underlying function of copied bottom-preserving homomorphism equals the new function
Informal description
For any bottom-preserving function $f \colon \alpha \to \beta$ between types with bottom elements, and any function $f' \colon \alpha \to \beta$ such that $f' = f$, the underlying function of the copy of $f$ with $f'$ as its new function is equal to $f'$.
BotHom.copy_eq theorem
(f : BotHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f
Full source 
theorem copy_eq (f : BotHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h
Copy of Bottom-Preserving Function Equals Original
Informal description
Given a bottom-preserving function $f$ from a type $\alpha$ with a bottom element $\bot$ to a type $\beta$ with a bottom element $\bot$, and a function $f'$ that is definitionally equal to $f$, the copy of $f$ with $f'$ as its underlying function is equal to $f$ itself.
BotHom.instInhabited instance
: Inhabited (BotHom α β)
Full source 
instance : Inhabited (BotHom α β) :=
  ⟨⟨fun _ => ⊥, rfl⟩⟩
Inhabitedness of Bottom-Preserving Homomorphisms
Informal description
For any types $\alpha$ and $\beta$ equipped with bottom elements $\bot$, the type of bottom-preserving homomorphisms from $\alpha$ to $\beta$ is inhabited.
BotHom.id definition
: BotHom α α
Full source 
/-- `id` as a `BotHom`. -/
protected def id : BotHom α α :=
  ⟨id, rfl⟩
Identity bottom-preserving homomorphism
Informal description
The identity function as a bottom-preserving homomorphism, i.e., the function that maps every element of a type $\alpha$ with a bottom element $\bot$ to itself and preserves the bottom element.
BotHom.coe_id theorem
: ⇑(BotHom.id α) = id
Full source 
@[simp, norm_cast]
theorem coe_id : ⇑(BotHom.id α) = id :=
  rfl
Identity Bottom-Preserving Homomorphism as Identity Function
Informal description
The canonical function associated with the identity bottom-preserving homomorphism on a type $\alpha$ with a bottom element $\bot$ is equal to the identity function on $\alpha$.
BotHom.id_apply theorem
(a : α) : BotHom.id α a = a
Full source 
@[simp]
theorem id_apply (a : α) : BotHom.id α a = a :=
  rfl
Identity Bottom-Preserving Homomorphism Acts as Identity Function
Informal description
For any element $a$ of a type $\alpha$ with a bottom element $\bot$, the identity bottom-preserving homomorphism evaluated at $a$ equals $a$, i.e., $\text{id}(a) = a$.
BotHom.comp definition
(f : BotHom β γ) (g : BotHom α β) : BotHom α γ
Full source 
/-- Composition of `BotHom`s as a `BotHom`. -/
def comp (f : BotHom β γ) (g : BotHom α β) :
    BotHom α γ where
  toFun := f ∘ g
  map_bot' := by rw [comp_apply, map_bot, map_bot]
Composition of bottom-preserving functions
Informal description
The composition of two bottom-preserving functions \( f : \beta \to \gamma \) and \( g : \alpha \to \beta \) is a bottom-preserving function from \( \alpha \) to \( \gamma \), defined by \( f \circ g \). This composition preserves the bottom element, i.e., \((f \circ g)(\bot) = \bot\).
BotHom.coe_comp theorem
(f : BotHom β γ) (g : BotHom α β) : (f.comp g : α → γ) = f ∘ g
Full source 
@[simp]
theorem coe_comp (f : BotHom β γ) (g : BotHom α β) : (f.comp g : α → γ) = f ∘ g :=
  rfl
Composition of Bottom-Preserving Functions as Function Composition
Informal description
For any bottom-preserving functions $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the underlying function of their composition $f \circ g$ is equal to the composition of their underlying functions, i.e., $(f \circ g)(a) = f(g(a))$ for all $a \in \alpha$.
BotHom.comp_apply theorem
(f : BotHom β γ) (g : BotHom α β) (a : α) : (f.comp g) a = f (g a)
Full source 
@[simp]
theorem comp_apply (f : BotHom β γ) (g : BotHom α β) (a : α) : (f.comp g) a = f (g a) :=
  rfl
Application of Composition of Bottom-Preserving Functions
Informal description
For any bottom-preserving functions $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, and for any element $a \in \alpha$, the application of the composition $f \circ g$ to $a$ is equal to $f$ applied to $g(a)$, i.e., $(f \circ g)(a) = f(g(a))$.
BotHom.comp_assoc theorem
(f : BotHom γ δ) (g : BotHom β γ) (h : BotHom α β) : (f.comp g).comp h = f.comp (g.comp h)
Full source 
@[simp]
theorem comp_assoc (f : BotHom γ δ) (g : BotHom β γ) (h : BotHom α β) :
    (f.comp g).comp h = f.comp (g.comp h) :=
  rfl
Associativity of Composition for Bottom-Preserving Functions
Informal description
For any bottom-preserving functions $f \colon \gamma \to \delta$, $g \colon \beta \to \gamma$, and $h \colon \alpha \to \beta$, the composition of these functions is associative, i.e., $(f \circ g) \circ h = f \circ (g \circ h)$.
BotHom.comp_id theorem
(f : BotHom α β) : f.comp (BotHom.id α) = f
Full source 
@[simp]
theorem comp_id (f : BotHom α β) : f.comp (BotHom.id α) = f :=
  BotHom.ext fun _ => rfl
Right Identity Law for Bottom-Preserving Function Composition
Informal description
For any bottom-preserving function $f \colon \alpha \to \beta$, the composition of $f$ with the identity bottom-preserving function on $\alpha$ equals $f$, i.e., $f \circ \text{id} = f$.
BotHom.id_comp theorem
(f : BotHom α β) : (BotHom.id β).comp f = f
Full source 
@[simp]
theorem id_comp (f : BotHom α β) : (BotHom.id β).comp f = f :=
  BotHom.ext fun _ => rfl
Left Identity Property of Bottom-Preserving Function Composition
Informal description
For any bottom-preserving function $f \colon \alpha \to \beta$, the composition of the identity bottom-preserving function on $\beta$ with $f$ equals $f$ itself, i.e., $\text{id}_\beta \circ f = f$.
BotHom.cancel_right theorem
{g₁ g₂ : BotHom β γ} {f : BotHom α β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂
Full source 
@[simp]
theorem cancel_right {g₁ g₂ : BotHom β γ} {f : BotHom α β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => BotHom.ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (comp · f)⟩
Right Cancellation Property for Composition of Bottom-Preserving Functions
Informal description
Let $f : \alpha \to \beta$ be a surjective bottom-preserving function between types with bottom elements, and let $g_1, g_2 : \beta \to \gamma$ be bottom-preserving functions. Then the composition $g_1 \circ f$ equals $g_2 \circ f$ if and only if $g_1 = g_2$.
BotHom.cancel_left theorem
{g : BotHom β γ} {f₁ f₂ : BotHom α β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
Full source 
@[simp]
theorem cancel_left {g : BotHom β γ} {f₁ f₂ : BotHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => BotHom.ext fun a => hg <| by rw [← BotHom.comp_apply, h, BotHom.comp_apply],
    congr_arg _⟩
Left Cancellation Property for Composition of Bottom-Preserving Functions
Informal description
Let $g \colon \beta \to \gamma$ and $f_1, f_2 \colon \alpha \to \beta$ be bottom-preserving functions. If $g$ is injective, then the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.
BotHom.instLE instance
[LE β] [Bot β] : LE (BotHom α β)
Full source 
instance instLE [LE β] [Bot β] : LE (BotHom α β) where
  le f g := (f : α → β) ≤ g
Preorder Structure on Bottom-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ with a bottom element $\bot$ and a preorder structure on $\beta$, the type of bottom-preserving functions from $\alpha$ to $\beta$ inherits a preorder structure where $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x \in \alpha$.
BotHom.instPreorder instance
[Preorder β] [Bot β] : Preorder (BotHom α β)
Full source 
instance [Preorder β] [Bot β] : Preorder (BotHom α β) :=
  Preorder.lift (DFunLike.coe : BotHom α β → α → β)
Preorder Structure on Bottom-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ with a bottom element $\bot$ and a preorder structure on $\beta$, the type of bottom-preserving functions from $\alpha$ to $\beta$ inherits a preorder structure where $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x \in \alpha$.
BotHom.instPartialOrder instance
[PartialOrder β] [Bot β] : PartialOrder (BotHom α β)
Full source 
instance [PartialOrder β] [Bot β] : PartialOrder (BotHom α β) :=
  PartialOrder.lift _ DFunLike.coe_injective
Partial Order Structure on Bottom-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ with a bottom element $\bot$ and a partial order structure on $\beta$, the type of bottom-preserving functions from $\alpha$ to $\beta$ inherits a partial order structure where $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x \in \alpha$.
BotHom.instOrderBot instance
: OrderBot (BotHom α β)
Full source 
instance : OrderBot (BotHom α β) where
  bot := ⟨⊥, rfl⟩
  bot_le := fun _ => @bot_le (α → β) _ _ _
Bottom-Preserving Functions Form an Order with Bottom Element
Informal description
For any types $\alpha$ and $\beta$ with a bottom element $\bot$, the type of bottom-preserving functions from $\alpha$ to $\beta$ is an order with a bottom element, where the bottom element is the constant function that maps every element of $\alpha$ to $\bot$.
BotHom.coe_bot theorem
: ⇑(⊥ : BotHom α β) = ⊥
Full source 
@[simp]
theorem coe_bot : ⇑(⊥ : BotHom α β) = ⊥ :=
  rfl
Bottom Element Coercion in Bottom-Preserving Functions: $\bot(a) = \bot$
Informal description
The coercion of the bottom element in the type of bottom-preserving functions from $\alpha$ to $\beta$ is equal to the constant bottom function, i.e., $\bot(a) = \bot$ for all $a \in \alpha$.
BotHom.bot_apply theorem
(a : α) : (⊥ : BotHom α β) a = ⊥
Full source 
@[simp]
theorem bot_apply (a : α) : (⊥ : BotHom α β) a = ⊥ :=
  rfl
Bottom-Preserving Function Evaluates to Bottom Element
Informal description
For any element $a$ in a type $\alpha$ with a bottom element $\bot$, and any type $\beta$ with a bottom element $\bot$, the bottom-preserving function $\bot : \text{BotHom}(\alpha, \beta)$ satisfies $\bot(a) = \bot$.
BotHom.instSemilatticeInf instance
: SemilatticeInf (BotHom α β)
Full source 
instance : SemilatticeInf (BotHom α β) :=
  (DFunLike.coe_injective.semilatticeInf _) fun _ _ => rfl
Meet-Semilattice Structure on Bottom-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ with bottom elements $\bot$, the type of bottom-preserving functions $\text{BotHom}(\alpha, \beta)$ forms a meet-semilattice, where the meet operation is defined pointwise.
BotHom.coe_inf theorem
: ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
Full source 
@[simp]
theorem coe_inf : ⇑(f ⊓ g) = ⇑f ⊓ ⇑g :=
  rfl
Pointwise Meet of Bottom-Preserving Functions
Informal description
For any two bottom-preserving functions $f, g \colon \alpha \to \beta$ between types with bottom elements, the underlying function of their meet $f \sqcap g$ is equal to the pointwise meet of the underlying functions of $f$ and $g$, i.e., $(f \sqcap g)(x) = f(x) \sqcap g(x)$ for all $x \in \alpha$.
BotHom.inf_apply theorem
(a : α) : (f ⊓ g) a = f a ⊓ g a
Full source 
@[simp]
theorem inf_apply (a : α) : (f ⊓ g) a = f a ⊓ g a :=
  rfl
Pointwise Meet Evaluation for Bottom-Preserving Functions
Informal description
For any two bottom-preserving functions $f, g \colon \alpha \to \beta$ between types with bottom elements, and for any element $a \in \alpha$, the evaluation of their meet $f \sqcap g$ at $a$ is equal to the meet of $f(a)$ and $g(a)$ in $\beta$, i.e., $(f \sqcap g)(a) = f(a) \sqcap g(a)$.
BotHom.instSemilatticeSup instance
: SemilatticeSup (BotHom α β)
Full source 
instance : SemilatticeSup (BotHom α β) :=
  (DFunLike.coe_injective.semilatticeSup _) fun _ _ => rfl
Join-Semilattice Structure on Bottom-Preserving Functions
Informal description
For any types $\alpha$ and $\beta$ equipped with bottom elements $\bot$, the type of bottom-preserving functions $\mathrm{BotHom}(\alpha, \beta)$ forms a join-semilattice. That is, it has a supremum operation $\sqcup$ that is associative, commutative, and idempotent.
BotHom.coe_sup theorem
: ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
Full source 
@[simp]
theorem coe_sup : ⇑(f ⊔ g) = ⇑f ⊔ ⇑g :=
  rfl
Pointwise Supremum of Bottom-Preserving Functions
Informal description
For any bottom-preserving functions $f, g \colon \alpha \to \beta$ between types with bottom elements, the function corresponding to the supremum $f \sqcup g$ is equal to the pointwise supremum of $f$ and $g$, i.e., $(f \sqcup g)(a) = f(a) \sqcup g(a)$ for all $a \in \alpha$.
BotHom.sup_apply theorem
(a : α) : (f ⊔ g) a = f a ⊔ g a
Full source 
@[simp]
theorem sup_apply (a : α) : (f ⊔ g) a = f a ⊔ g a :=
  rfl
Pointwise Supremum of Bottom-Preserving Functions
Informal description
For any bottom-preserving functions $f, g \colon \alpha \to \beta$ between types with bottom elements, and for any element $a \in \alpha$, the evaluation of the supremum $f \sqcup g$ at $a$ equals the supremum of the evaluations $f(a) \sqcup g(a)$ in $\beta$.
BotHom.instLattice instance
[Lattice β] [OrderBot β] : Lattice (BotHom α β)
Full source 
instance [Lattice β] [OrderBot β] : Lattice (BotHom α β) :=
  DFunLike.coe_injective.lattice _ (fun _ _ => rfl) fun _ _ => rfl
Lattice Structure on Bottom-Preserving Functions
Informal description
For any lattice $\beta$ with a bottom element $\bot$, the type of bottom-preserving functions $\mathrm{BotHom}(\alpha, \beta)$ forms a lattice, where the meet and join operations are defined pointwise.
BotHom.instDistribLattice instance
[DistribLattice β] [OrderBot β] : DistribLattice (BotHom α β)
Full source 
instance [DistribLattice β] [OrderBot β] : DistribLattice (BotHom α β) :=
  DFunLike.coe_injective.distribLattice _ (fun _ _ => rfl) fun _ _ => rfl
Distributive Lattice Structure on Bottom-Preserving Functions
Informal description
For any distributive lattice $\beta$ with a bottom element $\bot$, the type of bottom-preserving functions $\mathrm{BotHom}(\alpha, \beta)$ forms a distributive lattice, where the meet and join operations are defined pointwise.
BoundedOrderHom.toTopHom definition
(f : BoundedOrderHom α β) : TopHom α β
Full source 
/-- Reinterpret a `BoundedOrderHom` as a `TopHom`. -/
def toTopHom (f : BoundedOrderHom α β) : TopHom α β :=
  { f with }
Bounded order homomorphism as top-preserving function
Informal description
Given a bounded order homomorphism \( f \colon \alpha \to \beta \) (a monotone function preserving both top and bottom elements), this definition reinterprets \( f \) as a top-preserving function (a `TopHom`), focusing only on its property of preserving the top element \( \top \).
BoundedOrderHom.toBotHom definition
(f : BoundedOrderHom α β) : BotHom α β
Full source 
/-- Reinterpret a `BoundedOrderHom` as a `BotHom`. -/
def toBotHom (f : BoundedOrderHom α β) : BotHom α β :=
  { f with }
Bounded order homomorphism as bottom-preserving function
Informal description
Given a bounded order homomorphism \( f \colon \alpha \to \beta \) (a monotone function preserving both top and bottom elements), this definition reinterprets \( f \) as a bottom-preserving function (a `BotHom`), focusing only on its property of preserving the bottom element \( \bot \).
BoundedOrderHom.instFunLike instance
: FunLike (BoundedOrderHom α β) α β
Full source 
instance : FunLike (BoundedOrderHom α β) α β where
  coe f := f.toFun
  coe_injective' f g h := by obtain ⟨⟨_, _⟩, _⟩ := f; obtain ⟨⟨_, _⟩, _⟩ := g; congr
Function-Like Structure for Bounded Order Homomorphisms
Informal description
For any two preordered sets $\alpha$ and $\beta$ with bounded order structures (i.e., both have a greatest element $\top$ and a least element $\bot$), the type of bounded order homomorphisms from $\alpha$ to $\beta$ is equipped with a function-like structure, meaning each bounded order homomorphism can be treated as a function from $\alpha$ to $\beta$.
BoundedOrderHom.instBoundedOrderHomClass instance
: BoundedOrderHomClass (BoundedOrderHom α β) α β
Full source 
instance : BoundedOrderHomClass (BoundedOrderHom α β) α β where
  map_rel f := @(f.monotone')
  map_top f := f.map_top'
  map_bot f := f.map_bot'
Bounded Order Homomorphisms as a Homomorphism Class
Informal description
The type of bounded order homomorphisms between two preordered sets with top and bottom elements forms a `BoundedOrderHomClass`. This means that any bounded order homomorphism $f \colon \alpha \to \beta$ is a monotone function that preserves both the top element ($f(\top) = \top$) and the bottom element ($f(\bot) = \bot$).
BoundedOrderHom.ext theorem
{f g : BoundedOrderHom α β} (h : ∀ a, f a = g a) : f = g
Full source 
@[ext]
theorem ext {f g : BoundedOrderHom α β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h
Extensionality of Bounded Order Homomorphisms
Informal description
For any two bounded order homomorphisms $f, g \colon \alpha \to \beta$ between preordered sets with top and bottom elements, if $f(a) = g(a)$ for all $a \in \alpha$, then $f = g$.
BoundedOrderHom.copy definition
(f : BoundedOrderHom α β) (f' : α → β) (h : f' = f) : BoundedOrderHom α β
Full source 
/-- Copy of a `BoundedOrderHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : BoundedOrderHom α β) (f' : α → β) (h : f' = f) : BoundedOrderHom α β :=
  { f.toOrderHom.copy f' h, f.toTopHom.copy f' h, f.toBotHom.copy f' h with }
Copy of a bounded order homomorphism with a new underlying function
Informal description
Given a bounded order homomorphism \( f \colon \alpha \to \beta \) (a monotone function preserving both top and bottom elements) and a function \( f' \colon \alpha \to \beta \) that is definitionally equal to \( f \), the function `BoundedOrderHom.copy` constructs a new bounded order homomorphism with \( f' \) as its underlying function, ensuring that it still preserves both the top and bottom elements and remains monotone.
BoundedOrderHom.coe_copy theorem
(f : BoundedOrderHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f'
Full source 
@[simp]
theorem coe_copy (f : BoundedOrderHom α β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl
Underlying function of copied bounded order homomorphism equals the copied function
Informal description
Let $f \colon \alpha \to \beta$ be a bounded order homomorphism between preordered sets with top and bottom elements, and let $f' \colon \alpha \to \beta$ be a function such that $f' = f$. Then the underlying function of the copied homomorphism $f.copy\ f'\ h$ is equal to $f'$.
BoundedOrderHom.copy_eq theorem
(f : BoundedOrderHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f
Full source 
theorem copy_eq (f : BoundedOrderHom α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h
Copy of Bounded Order Homomorphism Equals Original
Informal description
Given a bounded order homomorphism $f \colon \alpha \to \beta$ (a monotone function preserving both $\top$ and $\bot$) and a function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with $f'$ as its underlying function is equal to $f$ itself.
BoundedOrderHom.id definition
: BoundedOrderHom α α
Full source 
/-- `id` as a `BoundedOrderHom`. -/
protected def id : BoundedOrderHom α α :=
  { OrderHom.id, TopHom.id α, BotHom.id α with }
Identity bounded order homomorphism
Informal description
The identity function viewed as a bounded order homomorphism, i.e., a monotone function from a preordered set $\alpha$ with both a greatest element $\top$ and a least element $\bot$ to itself that preserves both $\top$ and $\bot$.
BoundedOrderHom.instInhabited instance
: Inhabited (BoundedOrderHom α α)
Full source 
instance : Inhabited (BoundedOrderHom α α) :=
  ⟨BoundedOrderHom.id α⟩
Inhabitedness of Bounded Order Homomorphisms
Informal description
For any preordered set $\alpha$ with both a greatest element $\top$ and a least element $\bot$, the type of bounded order homomorphisms from $\alpha$ to itself is inhabited. In particular, the identity function serves as a canonical example of such a homomorphism.
BoundedOrderHom.coe_id theorem
: ⇑(BoundedOrderHom.id α) = id
Full source 
@[simp, norm_cast]
theorem coe_id : ⇑(BoundedOrderHom.id α) = id :=
  rfl
Identity Bounded Order Homomorphism as Identity Function
Informal description
The underlying function of the identity bounded order homomorphism on a preordered set $\alpha$ with both a greatest element $\top$ and a least element $\bot$ is equal to the identity function on $\alpha$.
BoundedOrderHom.id_apply theorem
(a : α) : BoundedOrderHom.id α a = a
Full source 
@[simp]
theorem id_apply (a : α) : BoundedOrderHom.id α a = a :=
  rfl
Identity Bounded Order Homomorphism Evaluation
Informal description
For any element $a$ in a preordered set $\alpha$ with both a greatest element $\top$ and a least element $\bot$, the identity bounded order homomorphism evaluated at $a$ is equal to $a$ itself, i.e., $\text{id}(a) = a$.
BoundedOrderHom.comp definition
(f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : BoundedOrderHom α γ
Full source 
/-- Composition of `BoundedOrderHom`s as a `BoundedOrderHom`. -/
def comp (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : BoundedOrderHom α γ :=
  { f.toOrderHom.comp g.toOrderHom, f.toTopHom.comp g.toTopHom, f.toBotHom.comp g.toBotHom with }
Composition of bounded order homomorphisms
Informal description
The composition of two bounded order homomorphisms \( f \colon \beta \to \gamma \) and \( g \colon \alpha \to \beta \) is a bounded order homomorphism \( f \circ g \colon \alpha \to \gamma \). This composition preserves both the top and bottom elements and is monotone.
BoundedOrderHom.coe_comp theorem
(f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : (f.comp g : α → γ) = f ∘ g
Full source 
@[simp]
theorem coe_comp (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : (f.comp g : α → γ) = f ∘ g :=
  rfl
Composition of Bounded Order Homomorphisms as Function Composition
Informal description
For any two bounded order homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the underlying function of their composition $f \circ g \colon \alpha \to \gamma$ is equal to the pointwise composition of the underlying functions of $f$ and $g$.
BoundedOrderHom.comp_apply theorem
(f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) (a : α) : (f.comp g) a = f (g a)
Full source 
@[simp]
theorem comp_apply (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) (a : α) :
    (f.comp g) a = f (g a) :=
  rfl
Composition of Bounded Order Homomorphisms Evaluates Pointwise
Informal description
For any bounded order homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, and any element $a \in \alpha$, the composition $(f \circ g)(a)$ equals $f(g(a))$.
BoundedOrderHom.coe_comp_orderHom theorem
(f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : (f.comp g : OrderHom α γ) = (f : OrderHom β γ).comp g
Full source 
@[simp]
theorem coe_comp_orderHom (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :
    (f.comp g : OrderHom α γ) = (f : OrderHom β γ).comp g :=
  rfl
Composition of Bounded Order Homomorphisms as Order Homomorphisms
Informal description
For any bounded order homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the underlying order homomorphism of their composition $f \circ g \colon \alpha \to \gamma$ is equal to the composition of the underlying order homomorphisms of $f$ and $g$.
BoundedOrderHom.coe_comp_topHom theorem
(f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : (f.comp g : TopHom α γ) = (f : TopHom β γ).comp g
Full source 
@[simp]
theorem coe_comp_topHom (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :
    (f.comp g : TopHom α γ) = (f : TopHom β γ).comp g :=
  rfl
Compatibility of Top-Preserving Function Composition with Bounded Order Homomorphism Composition
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be preordered sets with bounded order structures (i.e., each has a greatest element $\top$ and a least element $\bot$). For any bounded order homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the top-preserving function associated with the composition $f \circ g$ is equal to the composition of the top-preserving functions associated with $f$ and $g$. In other words, $(f \circ g)_{\text{top}} = f_{\text{top}} \circ g_{\text{top}}$, where $f_{\text{top}}$ and $g_{\text{top}}$ denote the underlying top-preserving functions of $f$ and $g$ respectively.
BoundedOrderHom.coe_comp_botHom theorem
(f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : (f.comp g : BotHom α γ) = (f : BotHom β γ).comp g
Full source 
@[simp]
theorem coe_comp_botHom (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :
    (f.comp g : BotHom α γ) = (f : BotHom β γ).comp g :=
  rfl
Compatibility of Composition with Bottom-Preservation in Bounded Order Homomorphisms
Informal description
For any bounded order homomorphisms $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the bottom-preserving function obtained by composing $f$ and $g$ as bounded order homomorphisms is equal to the composition of $f$ and $g$ viewed as bottom-preserving functions. In other words, $(f \circ g)_{\text{BotHom}} = f_{\text{BotHom}} \circ g_{\text{BotHom}}$.
BoundedOrderHom.comp_assoc theorem
(f : BoundedOrderHom γ δ) (g : BoundedOrderHom β γ) (h : BoundedOrderHom α β) : (f.comp g).comp h = f.comp (g.comp h)
Full source 
@[simp]
theorem comp_assoc (f : BoundedOrderHom γ δ) (g : BoundedOrderHom β γ) (h : BoundedOrderHom α β) :
    (f.comp g).comp h = f.comp (g.comp h) :=
  rfl
Associativity of Composition for Bounded Order Homomorphisms
Informal description
For any bounded order homomorphisms $f \colon \gamma \to \delta$, $g \colon \beta \to \gamma$, and $h \colon \alpha \to \beta$, the composition of these homomorphisms is associative, i.e., $(f \circ g) \circ h = f \circ (g \circ h)$.
BoundedOrderHom.comp_id theorem
(f : BoundedOrderHom α β) : f.comp (BoundedOrderHom.id α) = f
Full source 
@[simp]
theorem comp_id (f : BoundedOrderHom α β) : f.comp (BoundedOrderHom.id α) = f :=
  BoundedOrderHom.ext fun _ => rfl
Right Identity Law for Bounded Order Homomorphisms
Informal description
For any bounded order homomorphism $f \colon \alpha \to \beta$ between preordered sets with top and bottom elements, the composition of $f$ with the identity bounded order homomorphism on $\alpha$ equals $f$, i.e., $f \circ \text{id}_\alpha = f$.
BoundedOrderHom.id_comp theorem
(f : BoundedOrderHom α β) : (BoundedOrderHom.id β).comp f = f
Full source 
@[simp]
theorem id_comp (f : BoundedOrderHom α β) : (BoundedOrderHom.id β).comp f = f :=
  BoundedOrderHom.ext fun _ => rfl
Identity Bounded Order Homomorphism Acts as Left Identity Under Composition
Informal description
For any bounded order homomorphism $f \colon \alpha \to \beta$ between preordered sets with top and bottom elements, the composition of the identity bounded order homomorphism on $\beta$ with $f$ equals $f$. That is, $\text{id}_\beta \circ f = f$.
BoundedOrderHom.cancel_right theorem
{g₁ g₂ : BoundedOrderHom β γ} {f : BoundedOrderHom α β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂
Full source 
@[simp]
theorem cancel_right {g₁ g₂ : BoundedOrderHom β γ} {f : BoundedOrderHom α β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => BoundedOrderHom.ext <| hf.forall.2 <| DFunLike.ext_iff.1 h,
   congr_arg (fun g => comp g f)⟩
Right Cancellation Property for Bounded Order Homomorphisms under Surjective Maps
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be preordered sets with bounded order structures (having both a greatest element $\top$ and a least element $\bot$). Given two bounded order homomorphisms $g_1, g_2 \colon \beta \to \gamma$ and a surjective bounded order homomorphism $f \colon \alpha \to \beta$, the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.
BoundedOrderHom.cancel_left theorem
{g : BoundedOrderHom β γ} {f₁ f₂ : BoundedOrderHom α β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
Full source 
@[simp]
theorem cancel_left {g : BoundedOrderHom β γ} {f₁ f₂ : BoundedOrderHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h =>
    BoundedOrderHom.ext fun a =>
      hg <| by rw [← BoundedOrderHom.comp_apply, h, BoundedOrderHom.comp_apply],
    congr_arg _⟩
Left Cancellation Property for Bounded Order Homomorphisms under Injective Maps
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be preordered sets with bounded order structures (having both a greatest element $\top$ and a least element $\bot$). Given a bounded order homomorphism $g \colon \beta \to \gamma$ that is injective, and two bounded order homomorphisms $f_1, f_2 \colon \alpha \to \beta$, the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.
TopHom.dual definition
: TopHom α β ≃ BotHom αᵒᵈ βᵒᵈ
Full source 
/-- Reinterpret a top homomorphism as a bot homomorphism between the dual lattices. -/
@[simps]
protected def dual :
    TopHomTopHom α β ≃ BotHom αᵒᵈ βᵒᵈ where
  toFun f := ⟨f, f.map_top'⟩
  invFun f := ⟨f, f.map_bot'⟩
  left_inv _ := TopHom.ext fun _ => rfl
  right_inv _ := BotHom.ext fun _ => rfl
Duality between top and bottom homomorphisms
Informal description
The equivalence between top-preserving functions from $\alpha$ to $\beta$ and bottom-preserving functions between their order duals $\alpha^{\text{op}}$ and $\beta^{\text{op}}$. Specifically: 1. Given a top-preserving function $f: \alpha \to \beta$, it corresponds to a bottom-preserving function between the dual orders that maps $\bot_{\alpha^{\text{op}}}$ to $\bot_{\beta^{\text{op}}}$. 2. Conversely, any bottom-preserving function between the dual orders corresponds to a top-preserving function between the original orders. This equivalence preserves identities and compositions of homomorphisms.
TopHom.dual_id theorem
: TopHom.dual (TopHom.id α) = BotHom.id _
Full source 
@[simp]
theorem dual_id : TopHom.dual (TopHom.id α) = BotHom.id _ :=
  rfl
Duality of Identity Top Homomorphism: $\text{dual}(\text{id}_{\top}) = \text{id}_{\bot}$
Informal description
The dual of the identity top-preserving homomorphism on a type $\alpha$ with a top element $\top$ is equal to the identity bottom-preserving homomorphism on the order dual $\alpha^{\text{op}}$.
TopHom.dual_comp theorem
(g : TopHom β γ) (f : TopHom α β) : TopHom.dual (g.comp f) = g.dual.comp (TopHom.dual f)
Full source 
@[simp]
theorem dual_comp (g : TopHom β γ) (f : TopHom α β) :
    TopHom.dual (g.comp f) = g.dual.comp (TopHom.dual f) :=
  rfl
Duality of Composition for Top-Preserving Functions: $\text{dual}(g \circ f) = \text{dual}(g) \circ \text{dual}(f)$
Informal description
For any top-preserving functions $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the dual of their composition $g \circ f$ is equal to the composition of their duals, i.e., $\text{dual}(g \circ f) = \text{dual}(g) \circ \text{dual}(f)$. Here, $\text{dual}$ denotes the equivalence between top-preserving functions and bottom-preserving functions on the order duals of the types.
TopHom.symm_dual_id theorem
: TopHom.dual.symm (BotHom.id _) = TopHom.id α
Full source 
@[simp]
theorem symm_dual_id : TopHom.dual.symm (BotHom.id _) = TopHom.id α :=
  rfl
Inverse Duality of Identity Homomorphism: $\text{dual}^{-1}(\text{id}_{\bot}) = \text{id}_{\top}$
Informal description
The inverse of the duality equivalence applied to the identity bottom-preserving homomorphism on the order dual of $\alpha$ yields the identity top-preserving homomorphism on $\alpha$.
TopHom.symm_dual_comp theorem
(g : BotHom βᵒᵈ γᵒᵈ) (f : BotHom αᵒᵈ βᵒᵈ) : TopHom.dual.symm (g.comp f) = (TopHom.dual.symm g).comp (TopHom.dual.symm f)
Full source 
@[simp]
theorem symm_dual_comp (g : BotHom βᵒᵈ γᵒᵈ) (f : BotHom αᵒᵈ βᵒᵈ) :
    TopHom.dual.symm (g.comp f) = (TopHom.dual.symm g).comp (TopHom.dual.symm f) :=
  rfl
Inverse Duality Preserves Composition of Bottom-Preserving Functions: $\text{dual}^{-1}(g \circ f) = \text{dual}^{-1}(g) \circ \text{dual}^{-1}(f)$
Informal description
For any bottom-preserving functions $f \colon \alpha^{\text{op}} \to \beta^{\text{op}}$ and $g \colon \beta^{\text{op}} \to \gamma^{\text{op}}$, the inverse of the duality equivalence applied to their composition $g \circ f$ is equal to the composition of the inverse duality equivalences applied to $g$ and $f$ individually. That is, $\text{dual}^{-1}(g \circ f) = \text{dual}^{-1}(g) \circ \text{dual}^{-1}(f)$.
BotHom.dual definition
: BotHom α β ≃ TopHom αᵒᵈ βᵒᵈ
Full source 
/-- Reinterpret a bot homomorphism as a top homomorphism between the dual lattices. -/
@[simps]
protected def dual :
    BotHomBotHom α β ≃ TopHom αᵒᵈ βᵒᵈ where
  toFun f := ⟨f, f.map_bot'⟩
  invFun f := ⟨f, f.map_top'⟩
  left_inv _ := BotHom.ext fun _ => rfl
  right_inv _ := TopHom.ext fun _ => rfl
Dual equivalence between bottom-preserving and top-preserving functions
Informal description
The equivalence between the type of bottom-preserving functions from $\alpha$ to $\beta$ and the type of top-preserving functions from the order dual $\alpha^{\text{op}}$ to $\beta^{\text{op}}$. Specifically, given a bottom-preserving function $f : \alpha \to \beta$, its dual is the top-preserving function $f^{\text{op}} : \alpha^{\text{op}} \to \beta^{\text{op}}$ defined by $f^{\text{op}}(x) = f(x)$, and vice versa.
BotHom.dual_id theorem
: BotHom.dual (BotHom.id α) = TopHom.id _
Full source 
@[simp]
theorem dual_id : BotHom.dual (BotHom.id α) = TopHom.id _ :=
  rfl
Dual of Identity Bottom-Preserving Homomorphism is Identity Top-Preserving Homomorphism on Order Dual
Informal description
The dual of the identity bottom-preserving homomorphism on a type $\alpha$ with a bottom element is the identity top-preserving homomorphism on the order dual $\alpha^{\text{op}}$. That is, $\text{BotHom.dual}(\text{BotHom.id}(\alpha)) = \text{TopHom.id}(\alpha^{\text{op}})$.
BotHom.dual_comp theorem
(g : BotHom β γ) (f : BotHom α β) : BotHom.dual (g.comp f) = g.dual.comp (BotHom.dual f)
Full source 
@[simp]
theorem dual_comp (g : BotHom β γ) (f : BotHom α β) :
    BotHom.dual (g.comp f) = g.dual.comp (BotHom.dual f) :=
  rfl
Dual of Composition of Bottom-Preserving Functions Equals Composition of Duals
Informal description
For any bottom-preserving functions $g : \beta \to \gamma$ and $f : \alpha \to \beta$, the dual of their composition $g \circ f$ is equal to the composition of their duals $g^{\text{op}} \circ f^{\text{op}}$, where $g^{\text{op}} : \beta^{\text{op}} \to \gamma^{\text{op}}$ and $f^{\text{op}} : \alpha^{\text{op}} \to \beta^{\text{op}}$ are the corresponding top-preserving functions on the order duals. In symbols: \[ (g \circ f)^{\text{op}} = g^{\text{op}} \circ f^{\text{op}} \]
BotHom.symm_dual_id theorem
: BotHom.dual.symm (TopHom.id _) = BotHom.id α
Full source 
@[simp]
theorem symm_dual_id : BotHom.dual.symm (TopHom.id _) = BotHom.id α :=
  rfl
Inverse Dual Equivalence Maps Identity Top-Preserving Homomorphism to Identity Bottom-Preserving Homomorphism
Informal description
The inverse of the dual equivalence applied to the identity top-preserving homomorphism on the order dual $\alpha^{\text{op}}$ yields the identity bottom-preserving homomorphism on $\alpha$. In symbols: \[ \text{BotHom.dual.symm}(\text{TopHom.id}(\alpha^{\text{op}})) = \text{BotHom.id}(\alpha) \]
BotHom.symm_dual_comp theorem
(g : TopHom βᵒᵈ γᵒᵈ) (f : TopHom αᵒᵈ βᵒᵈ) : BotHom.dual.symm (g.comp f) = (BotHom.dual.symm g).comp (BotHom.dual.symm f)
Full source 
@[simp]
theorem symm_dual_comp (g : TopHom βᵒᵈ γᵒᵈ) (f : TopHom αᵒᵈ βᵒᵈ) :
    BotHom.dual.symm (g.comp f) = (BotHom.dual.symm g).comp (BotHom.dual.symm f) :=
  rfl
Inverse Dual Equivalence Preserves Composition of Top-Preserving Functions
Informal description
For any top-preserving functions $g : \beta^{\text{op}} \to \gamma^{\text{op}}$ and $f : \alpha^{\text{op}} \to \beta^{\text{op}}$, the inverse of the dual equivalence applied to the composition $g \circ f$ is equal to the composition of the inverse dual equivalences applied to $g$ and $f$ separately. In symbols: \[ \text{BotHom.dual.symm}(g \circ f) = (\text{BotHom.dual.symm } g) \circ (\text{BotHom.dual.symm } f) \]
BoundedOrderHom.dual definition
: BoundedOrderHom α β ≃ BoundedOrderHom αᵒᵈ βᵒᵈ
Full source 
/-- Reinterpret a bounded order homomorphism as a bounded order homomorphism between the dual
orders. -/
@[simps]
protected def dual :
    BoundedOrderHomBoundedOrderHom α β ≃
      BoundedOrderHom αᵒᵈ
        βᵒᵈ where
  toFun f := ⟨f.toOrderHom.dual, f.map_bot', f.map_top'⟩
  invFun f := ⟨OrderHom.dual.symm f.toOrderHom, f.map_bot', f.map_top'⟩
  left_inv _ := ext fun _ => rfl
  right_inv _ := ext fun _ => rfl
Dual equivalence of bounded order homomorphisms
Informal description
The equivalence between bounded order homomorphisms from $\alpha$ to $\beta$ and bounded order homomorphisms from the order dual $\alpha^{\text{op}}$ to the order dual $\beta^{\text{op}}$. Specifically, it maps a bounded order homomorphism $f \colon \alpha \to \beta$ to its dual $f^{\text{op}} \colon \alpha^{\text{op}} \to \beta^{\text{op}}$, which is also a bounded order homomorphism, and vice versa. This equivalence preserves the properties of mapping the top and bottom elements.
BoundedOrderHom.dual_id theorem
: (BoundedOrderHom.id α).dual = BoundedOrderHom.id _
Full source 
@[simp]
theorem dual_id : (BoundedOrderHom.id α).dual = BoundedOrderHom.id _ :=
  rfl
Dual of Identity Bounded Order Homomorphism is Identity on Dual Order
Informal description
The dual of the identity bounded order homomorphism on a preordered set $\alpha$ with both a greatest element $\top$ and a least element $\bot$ is equal to the identity bounded order homomorphism on the order dual $\alpha^{\text{op}}$.
BoundedOrderHom.dual_comp theorem
(g : BoundedOrderHom β γ) (f : BoundedOrderHom α β) : (g.comp f).dual = g.dual.comp f.dual
Full source 
@[simp]
theorem dual_comp (g : BoundedOrderHom β γ) (f : BoundedOrderHom α β) :
    (g.comp f).dual = g.dual.comp f.dual :=
  rfl
Dual of Composition of Bounded Order Homomorphisms
Informal description
For any bounded order homomorphisms $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the dual of their composition equals the composition of their duals, i.e., $(g \circ f)^{\text{op}} = g^{\text{op}} \circ f^{\text{op}}$.
BoundedOrderHom.symm_dual_id theorem
: BoundedOrderHom.dual.symm (BoundedOrderHom.id _) = BoundedOrderHom.id α
Full source 
@[simp]
theorem symm_dual_id : BoundedOrderHom.dual.symm (BoundedOrderHom.id _) = BoundedOrderHom.id α :=
  rfl
Inverse Dual of Identity Bounded Order Homomorphism is Identity
Informal description
The inverse of the dual equivalence applied to the identity bounded order homomorphism on the order dual of $\alpha$ is equal to the identity bounded order homomorphism on $\alpha$. In other words, if we take the identity homomorphism on $\alpha^{\text{op}}$, apply the dual equivalence to get a homomorphism on $\alpha$, and then take the inverse of this equivalence, we recover the original identity homomorphism on $\alpha$.
BoundedOrderHom.symm_dual_comp theorem
(g : BoundedOrderHom βᵒᵈ γᵒᵈ) (f : BoundedOrderHom αᵒᵈ βᵒᵈ) : BoundedOrderHom.dual.symm (g.comp f) = (BoundedOrderHom.dual.symm g).comp (BoundedOrderHom.dual.symm f)
Full source 
@[simp]
theorem symm_dual_comp (g : BoundedOrderHom βᵒᵈ γᵒᵈ) (f : BoundedOrderHom αᵒᵈ βᵒᵈ) :
    BoundedOrderHom.dual.symm (g.comp f) =
      (BoundedOrderHom.dual.symm g).comp (BoundedOrderHom.dual.symm f) :=
  rfl
Inverse Dual Equivalence Preserves Composition of Bounded Order Homomorphisms
Informal description
For any bounded order homomorphisms $g \colon \beta^{\text{op}} \to \gamma^{\text{op}}$ and $f \colon \alpha^{\text{op}} \to \beta^{\text{op}}$, the inverse of the dual equivalence applied to the composition $g \circ f$ is equal to the composition of the inverse dual equivalences applied to $g$ and $f$ separately. In other words, the following equality holds: \[ \text{BoundedOrderHom.dual.symm}(g \circ f) = (\text{BoundedOrderHom.dual.symm } g) \circ (\text{BoundedOrderHom.dual.symm } f). \]