Documentation Verification Report

WithTopBot

📁 Source: Mathlib/Order/Hom/WithTopBot.lean

Statistics

Metric	Count
Definitions `coeWithBot`, `coeWithTop`, `withBot`, `withBot'`, `withTop`, `withTop'`, `withBot`, `withBot'`, `withTop`, `withTop'`, `withTopWithBot`, `withTopWithBot'`, `withBotCoe`, `withBotMap`, `withTopCoe`, `withTopMap`, `withBotMap`, `withTopMap`, `withBotCongr`, `withTopCongr`, `withBot`, `withBot'`, `withTop`, `withTop'`, `coeOrderHom`, `subtypeOrderIso`, `toDualTopEquiv`, `coeOrderHom`, `subtypeOrderIso`, `toDualBotEquiv`, `WithTopBot`	31
Theorems `coeWithBot_apply`, `coeWithTop_apply`, `withBot'_toFun`, `withBot_comp`, `withBot_id`, `withBot_toFun`, `withTop'_toFun`, `withTop_comp`, `withTop_id`, `withTop_toFun`, `coe_withBot`, `coe_withTop`, `coe_withTopWithBot`, `withBot'_toFun`, `withBot_apply`, `withBot_comp`, `withBot_id`, `withBot_toFun`, `withTop'_toFun`, `withTopWithBot'_toFun`, `withTopWithBot_apply`, `withTopWithBot_comp`, `withTopWithBot_id`, `withTopWithBot_toFun`, `withTop_apply`, `withTop_comp`, `withTop_id`, `withTop_toFun`, `withBotCoe_apply`, `withBotMap_apply`, `withTopCoe_apply`, `withTopMap_apply`, `withBotMap_coe`, `withTopMap_coe`, `withBotCongr_apply`, `withBotCongr_refl`, `withBotCongr_symm`, `withBotCongr_symm_apply`, `withBotCongr_trans`, `withTopCongr_apply`, `withTopCongr_refl`, `withTopCongr_symm`, `withTopCongr_symm_apply`, `withTopCongr_trans`, `withBot'_toFun`, `withBot_comp`, `withBot_id`, `withBot_toFun`, `withTop'_toFun`, `withTop_comp`, `withTop_id`, `withTop_toFun`, `coeOrderHom_apply`, `coe_toDualTopEquiv_eq`, `subtypeOrderIso_apply_coe`, `subtypeOrderIso_symm_apply`, `toDualTopEquiv_bot`, `toDualTopEquiv_coe`, `toDualTopEquiv_symm_bot`, `toDualTopEquiv_symm_coe`, `coeOrderHom_apply`, `coe_toDualBotEquiv`, `subtypeOrderIso_apply_coe`, `subtypeOrderIso_symm_apply`, `toDualBotEquiv_coe`, `toDualBotEquiv_symm_coe`, `toDualBotEquiv_symm_top`, `toDualBotEquiv_top`	68
Total	99

Function.Embedding

Definitions

Name	Category	Theorems
`coeWithBot` 📖	CompOp	1 math math: `coeWithBot_apply`
`coeWithTop` 📖	CompOp	1 math math: `coeWithTop_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeWithBot_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `WithBot` `Function.instFunLikeEmbedding` `coeWithBot` `WithBot.some`	—	—
`coeWithTop_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `WithTop` `Function.instFunLikeEmbedding` `coeWithTop` `WithTop.some`	—	—

InfHom

Definitions

Name	Category	Theorems
`withBot` 📖	CompOp	3 math math: `withBot_toFun`, `withBot_comp`, `withBot_id`
`withBot'` 📖	CompOp	1 math math: `withBot'_toFun`
`withTop` 📖	CompOp	3 math math: `withTop_toFun`, `withTop_id`, `withTop_comp`
`withTop'` 📖	CompOp	1 math math: `withTop'_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withBot'_toFun` 📖	mathematical	—	`DFunLike.coe` `InfHom` `WithBot` `SemilatticeInf.toMin` `WithBot.semilatticeInf` `instFunLike` `withBot'` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	—
`withBot_comp` 📖	mathematical	—	`withBot` `comp` `SemilatticeInf.toMin` `WithBot` `WithBot.semilatticeInf`	—	`DFunLike.coe_injective` `WithBot.map_comp_map`
`withBot_id` 📖	mathematical	—	`withBot` `id` `SemilatticeInf.toMin` `WithBot` `WithBot.semilatticeInf`	—	`DFunLike.coe_injective` `WithBot.map_id`
`withBot_toFun` 📖	mathematical	—	`DFunLike.coe` `InfHom` `WithBot` `SemilatticeInf.toMin` `WithBot.semilatticeInf` `instFunLike` `withBot` `WithBot.map`	—	—
`withTop'_toFun` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `WithTop.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `InfTopHom.instFunLike` `withTop'` `Top.top` `InfHom` `instFunLike`	—	—
`withTop_comp` 📖	mathematical	—	`withTop` `comp` `SemilatticeInf.toMin` `InfTopHom.comp` `WithTop` `WithTop.semilatticeInf` `WithTop.top`	—	`DFunLike.coe_injective` `WithTop.map_comp_map`
`withTop_id` 📖	mathematical	—	`withTop` `id` `SemilatticeInf.toMin` `InfTopHom.id` `WithTop` `WithTop.semilatticeInf` `WithTop.top`	—	`DFunLike.coe_injective` `WithTop.map_id`
`withTop_toFun` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `WithTop.top` `InfTopHom.instFunLike` `withTop` `WithTop.map` `InfHom` `instFunLike`	—	—

LatticeHom

Definitions

Name	Category	Theorems
`withBot` 📖	CompOp	5 math math: `withBot_id`, `withBot_toFun`, `withBot_comp`, `coe_withBot`, `withBot_apply`
`withBot'` 📖	CompOp	2 math math: `withTopWithBot'_toFun`, `withBot'_toFun`
`withTop` 📖	CompOp	5 math math: `withTop_apply`, `withTop_toFun`, `coe_withTop`, `withTop_comp`, `withTop_id`
`withTop'` 📖	CompOp	1 math math: `withTop'_toFun`
`withTopWithBot` 📖	CompOp	5 math math: `withTopWithBot_apply`, `coe_withTopWithBot`, `withTopWithBot_id`, `withTopWithBot_comp`, `withTopWithBot_toFun`
`withTopWithBot'` 📖	CompOp	1 math math: `withTopWithBot'_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_withBot` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `WithBot` `WithBot.lattice` `instFunLike` `withBot` `WithBot.map`	—	—
`coe_withTop` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `WithTop` `WithTop.lattice` `instFunLike` `withTop` `WithTop.map`	—	—
`coe_withTopWithBot` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `WithTop` `WithBot` `WithTop.lattice` `WithBot.lattice` `WithTop.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `WithBot.instOrderBot` `BoundedLatticeHom.instFunLike` `withTopWithBot` `WithTop.map` `WithBot.map` `LatticeHom` `instFunLike`	—	—
`withBot'_toFun` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `WithBot` `WithBot.lattice` `instFunLike` `withBot'` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup`	—	—
`withBot_apply` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `WithBot` `WithBot.lattice` `instFunLike` `withBot` `WithBot.map`	—	—
`withBot_comp` 📖	mathematical	—	`withBot` `comp` `WithBot` `WithBot.lattice`	—	`DFunLike.coe_injective` `WithBot.map_comp_map`
`withBot_id` 📖	mathematical	—	`withBot` `id` `WithBot` `WithBot.lattice`	—	`DFunLike.coe_injective` `WithBot.map_id`
`withBot_toFun` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `WithBot` `WithBot.lattice` `instFunLike` `withBot` `SupBotHom` `SemilatticeSup.toMax` `WithBot.semilatticeSup` `Lattice.toSemilatticeSup` `WithBot.bot` `SupBotHom.instFunLike` `SupHom.withBot` `toSupHom`	—	—
`withTop'_toFun` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `WithTop` `WithTop.lattice` `instFunLike` `withTop'` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup`	—	—
`withTopWithBot'_toFun` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `WithTop` `WithBot` `WithTop.lattice` `WithBot.lattice` `WithTop.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `WithBot.instOrderBot` `BoundedLatticeHom.instFunLike` `withTopWithBot'` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `LatticeHom` `instFunLike` `withBot'` `BoundedOrder.toOrderBot`	—	—
`withTopWithBot_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `WithTop` `WithBot` `WithTop.lattice` `WithBot.lattice` `WithTop.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `WithBot.instOrderBot` `BoundedLatticeHom.instFunLike` `withTopWithBot` `WithTop.map` `WithBot.map` `LatticeHom` `instFunLike`	—	—
`withTopWithBot_comp` 📖	mathematical	—	`withTopWithBot` `comp` `BoundedLatticeHom.comp` `WithTop` `WithBot` `WithTop.lattice` `WithBot.lattice` `WithTop.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `WithBot.instOrderBot`	—	`BoundedLatticeHom.ext` `WithTop.map_map` `WithBot.map_comp_map`
`withTopWithBot_id` 📖	mathematical	—	`withTopWithBot` `id` `BoundedLatticeHom.id` `WithTop` `WithBot` `WithTop.lattice` `WithBot.lattice` `WithTop.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `WithBot.instOrderBot`	—	`DFunLike.coe_injective` `WithBot.map_id` `WithTop.map_id`
`withTopWithBot_toFun` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `WithTop` `WithBot` `WithTop.lattice` `WithBot.lattice` `WithTop.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `WithBot.instOrderBot` `BoundedLatticeHom.instFunLike` `withTopWithBot` `WithTop.map` `WithBot.map` `LatticeHom` `instFunLike`	—	—
`withTop_apply` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `WithTop` `WithTop.lattice` `instFunLike` `withTop` `WithTop.map`	—	—
`withTop_comp` 📖	mathematical	—	`withTop` `comp` `WithTop` `WithTop.lattice`	—	`DFunLike.coe_injective` `WithTop.map_comp_map`
`withTop_id` 📖	mathematical	—	`withTop` `id` `WithTop` `WithTop.lattice`	—	`DFunLike.coe_injective` `WithTop.map_id`
`withTop_toFun` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `WithTop` `WithTop.lattice` `instFunLike` `withTop` `WithTop.map`	—	—

OrderEmbedding

Definitions

Name	Category	Theorems
`withBotCoe` 📖	CompOp	—
`withBotMap` 📖	CompOp	1 math math: `withBotMap_apply`
`withTopCoe` 📖	CompOp	—
`withTopMap` 📖	CompOp	1 math math: `withTopMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withBotCoe_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `RelEmbedding.instFunLike` `WithBot.coeOrderHom` `WithBot.some`	—	`WithBot.coeOrderHom_apply`
`withBotMap_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `RelEmbedding.instFunLike` `withBotMap` `WithBot.map` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	—
`withTopCoe_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `RelEmbedding.instFunLike` `WithTop.coeOrderHom` `WithTop.some`	—	`WithTop.coeOrderHom_apply`
`withTopMap_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `RelEmbedding.instFunLike` `withTopMap` `WithTop.map` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	—

OrderHom

Definitions

Name	Category	Theorems
`withBotMap` 📖	CompOp	1 math math: `withBotMap_coe`
`withTopMap` 📖	CompOp	1 math math: `withTopMap_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withBotMap_coe` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `WithBot` `WithBot.instPreorder` `instFunLike` `withBotMap` `WithBot.map`	—	—
`withTopMap_coe` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `WithTop` `WithTop.instPreorder` `instFunLike` `withTopMap` `WithTop.map`	—	—

OrderIso

Definitions

Name	Category	Theorems
`withBotCongr` 📖	CompOp	5 math math: `withBotCongr_symm_apply`, `withBotCongr_refl`, `withBotCongr_apply`, `withBotCongr_trans`, `withBotCongr_symm`
`withTopCongr` 📖	CompOp	5 math math: `withTopCongr_apply`, `withTopCongr_refl`, `withTopCongr_trans`, `withTopCongr_symm`, `withTopCongr_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withBotCongr_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `RelIso.instFunLike` `withBotCongr` `WithBot.map` `OrderIso` `instFunLikeOrderIso`	—	—
`withBotCongr_refl` 📖	mathematical	—	`withBotCongr` `refl` `Preorder.toLE` `PartialOrder.toPreorder` `WithBot` `WithBot.instPreorder`	—	`RelIso.toEquiv_injective` `Equiv.withBotCongr_refl`
`withBotCongr_symm` 📖	mathematical	—	`withBotCongr` `symm` `Preorder.toLE` `PartialOrder.toPreorder` `WithBot` `WithBot.instPreorder`	—	`RelIso.toEquiv_injective` `Equiv.withBotCongr_symm`
`withBotCongr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `RelIso.instFunLike` `RelIso.symm` `withBotCongr` `Equiv.invFun` `Equiv.withBotCongr` `RelIso.toEquiv`	—	—
`withBotCongr_trans` 📖	mathematical	—	`withBotCongr` `trans` `Preorder.toLE` `PartialOrder.toPreorder` `WithBot` `WithBot.instPreorder`	—	`RelIso.toEquiv_injective` `Equiv.withBotCongr_trans`
`withTopCongr_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `RelIso.instFunLike` `withTopCongr` `WithTop.map` `OrderIso` `instFunLikeOrderIso`	—	—
`withTopCongr_refl` 📖	mathematical	—	`withTopCongr` `refl` `Preorder.toLE` `PartialOrder.toPreorder` `WithTop` `WithTop.instPreorder`	—	`RelIso.toEquiv_injective` `Equiv.withTopCongr_refl`
`withTopCongr_symm` 📖	mathematical	—	`withTopCongr` `symm` `Preorder.toLE` `PartialOrder.toPreorder` `WithTop` `WithTop.instPreorder`	—	`RelIso.toEquiv_injective` `Equiv.withTopCongr_symm`
`withTopCongr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `RelIso.instFunLike` `RelIso.symm` `withTopCongr` `Equiv.invFun` `Equiv.withTopCongr` `RelIso.toEquiv`	—	—
`withTopCongr_trans` 📖	mathematical	—	`withTopCongr` `trans` `Preorder.toLE` `PartialOrder.toPreorder` `WithTop` `WithTop.instPreorder`	—	`RelIso.toEquiv_injective` `Equiv.withTopCongr_trans`

SupHom

Definitions

Name	Category	Theorems
`withBot` 📖	CompOp	4 math math: `withBot_id`, `LatticeHom.withBot_toFun`, `withBot_comp`, `withBot_toFun`
`withBot'` 📖	CompOp	1 math math: `withBot'_toFun`
`withTop` 📖	CompOp	3 math math: `withTop_toFun`, `withTop_id`, `withTop_comp`
`withTop'` 📖	CompOp	1 math math: `withTop'_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withBot'_toFun` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `WithBot` `SemilatticeSup.toMax` `WithBot.semilatticeSup` `WithBot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SupBotHom.instFunLike` `withBot'` `Bot.bot` `SupHom` `instFunLike`	—	—
`withBot_comp` 📖	mathematical	—	`withBot` `comp` `SemilatticeSup.toMax` `SupBotHom.comp` `WithBot` `WithBot.semilatticeSup` `WithBot.bot`	—	`DFunLike.coe_injective` `WithBot.map_comp_map`
`withBot_id` 📖	mathematical	—	`withBot` `id` `SemilatticeSup.toMax` `SupBotHom.id` `WithBot` `WithBot.semilatticeSup` `WithBot.bot`	—	`DFunLike.coe_injective` `WithBot.map_id`
`withBot_toFun` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `WithBot` `SemilatticeSup.toMax` `WithBot.semilatticeSup` `WithBot.bot` `SupBotHom.instFunLike` `withBot` `WithBot.map` `SupHom` `instFunLike`	—	—
`withTop'_toFun` 📖	mathematical	—	`DFunLike.coe` `SupHom` `WithTop` `SemilatticeSup.toMax` `WithTop.semilatticeSup` `instFunLike` `withTop'` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	—
`withTop_comp` 📖	mathematical	—	`withTop` `comp` `SemilatticeSup.toMax` `WithTop` `WithTop.semilatticeSup`	—	`DFunLike.coe_injective` `WithTop.map_comp_map`
`withTop_id` 📖	mathematical	—	`withTop` `id` `SemilatticeSup.toMax` `WithTop` `WithTop.semilatticeSup`	—	`DFunLike.coe_injective` `WithTop.map_id`
`withTop_toFun` 📖	mathematical	—	`DFunLike.coe` `SupHom` `WithTop` `SemilatticeSup.toMax` `WithTop.semilatticeSup` `instFunLike` `withTop` `WithTop.map`	—	—

WithBot

Definitions

Name	Category	Theorems
`coeOrderHom` 📖	CompOp	2 math math: `OrderEmbedding.withBotCoe_apply`, `coeOrderHom_apply`
`subtypeOrderIso` 📖	CompOp	2 math math: `subtypeOrderIso_symm_apply`, `subtypeOrderIso_apply_coe`
`toDualTopEquiv` 📖	CompOp	5 math math: `coe_toDualTopEquiv_eq`, `toDualTopEquiv_coe`, `toDualTopEquiv_symm_bot`, `toDualTopEquiv_symm_coe`, `toDualTopEquiv_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeOrderHom_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `WithBot` `Preorder.toLE` `instPreorder` `RelEmbedding.instFunLike` `coeOrderHom` `some`	—	—
`coe_toDualTopEquiv_eq` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithBot` `OrderDual` `WithTop` `instLE` `OrderDual.instLE` `WithTop.instLE` `instFunLikeOrderIso` `toDualTopEquiv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `ofDual`	—	—
`subtypeOrderIso_apply_coe` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithBot` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPreorder` `Subtype.preorder` `instFunLikeOrderIso` `subtypeOrderIso` `WithTop.some`	—	—
`subtypeOrderIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithBot` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPreorder` `Subtype.preorder` `instFunLikeOrderIso` `OrderIso.symm` `subtypeOrderIso` `some`	—	`OrderIso.symm_apply_eq`
`toDualTopEquiv_bot` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithBot` `OrderDual` `WithTop` `instLE` `OrderDual.instLE` `WithTop.instLE` `instFunLikeOrderIso` `toDualTopEquiv` `Bot.bot` `bot` `OrderDual.instBot` `WithTop.top`	—	—
`toDualTopEquiv_coe` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithBot` `OrderDual` `WithTop` `instLE` `OrderDual.instLE` `WithTop.instLE` `instFunLikeOrderIso` `toDualTopEquiv` `some` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `WithTop.some`	—	—
`toDualTopEquiv_symm_bot` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `WithTop` `WithBot` `OrderDual.instLE` `WithTop.instLE` `instLE` `instFunLikeOrderIso` `OrderIso.symm` `toDualTopEquiv` `Bot.bot` `OrderDual.instBot` `WithTop.top` `bot`	—	—
`toDualTopEquiv_symm_coe` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `WithTop` `WithBot` `OrderDual.instLE` `WithTop.instLE` `instLE` `instFunLikeOrderIso` `OrderIso.symm` `toDualTopEquiv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `WithTop.some` `some`	—	—

WithTop

Definitions

Name	Category	Theorems
`coeOrderHom` 📖	CompOp	2 math math: `OrderEmbedding.withTopCoe_apply`, `coeOrderHom_apply`
`subtypeOrderIso` 📖	CompOp	2 math math: `subtypeOrderIso_symm_apply`, `subtypeOrderIso_apply_coe`
`toDualBotEquiv` 📖	CompOp	5 math math: `toDualBotEquiv_coe`, `toDualBotEquiv_symm_top`, `toDualBotEquiv_symm_coe`, `coe_toDualBotEquiv`, `toDualBotEquiv_top`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeOrderHom_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `WithTop` `Preorder.toLE` `instPreorder` `RelEmbedding.instFunLike` `coeOrderHom` `some`	—	—
`coe_toDualBotEquiv` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithTop` `OrderDual` `WithBot` `instLE` `OrderDual.instLE` `WithBot.instLE` `instFunLikeOrderIso` `toDualBotEquiv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `ofDual`	—	—
`subtypeOrderIso_apply_coe` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithTop` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `instPreorder` `Subtype.preorder` `instFunLikeOrderIso` `subtypeOrderIso` `some`	—	—
`subtypeOrderIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithTop` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `instPreorder` `Subtype.preorder` `instFunLikeOrderIso` `OrderIso.symm` `subtypeOrderIso` `some`	—	`OrderIso.symm_apply_eq`
`toDualBotEquiv_coe` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithTop` `OrderDual` `WithBot` `instLE` `OrderDual.instLE` `WithBot.instLE` `instFunLikeOrderIso` `toDualBotEquiv` `some` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `WithBot.some`	—	—
`toDualBotEquiv_symm_coe` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `WithBot` `WithTop` `OrderDual.instLE` `WithBot.instLE` `instLE` `instFunLikeOrderIso` `OrderIso.symm` `toDualBotEquiv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `WithBot.some` `some`	—	—
`toDualBotEquiv_symm_top` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `WithBot` `WithTop` `OrderDual.instLE` `WithBot.instLE` `instLE` `instFunLikeOrderIso` `OrderIso.symm` `toDualBotEquiv` `Top.top` `OrderDual.instTop` `WithBot.bot` `top`	—	—
`toDualBotEquiv_top` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithTop` `OrderDual` `WithBot` `instLE` `OrderDual.instLE` `WithBot.instLE` `instFunLikeOrderIso` `toDualBotEquiv` `Top.top` `top` `OrderDual.instTop` `WithBot.bot`	—	—

(root)

Definitions

Name	Category	Theorems
`WithTopBot` 📖	CompOp	—

---

← Back to Index