Bounded

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

Statistics

Metric	Count
Definitions `BotHom`, `comp`, `copy`, `dual`, `id`, `instDistribLattice`, `instFunLike`, `instInhabited`, `instLE`, `instLattice`, `instMax`, `instMin`, `instOrderBot`, `instPartialOrder`, `instPreorder`, `instSemilatticeInf`, `instSemilatticeSup`, `toFun`, `BotHomClass`, `toBotHom`, `BoundedOrderHom`, `comp`, `copy`, `dual`, `id`, `instFunLike`, `instInhabited`, `toBotHom`, `toOrderHom`, `toTopHom`, `BoundedOrderHomClass`, `toBoundedOrderHom`, `TopHom`, `comp`, `copy`, `dual`, `id`, `instDistribLattice`, `instFunLike`, `instInhabited`, `instLE`, `instLattice`, `instMax`, `instMin`, `instOrderTop`, `instPartialOrder`, `instPreorder`, `instSemilatticeInf`, `instSemilatticeSup`, `toFun`, `TopHomClass`, `toTopHom`, `instCoeTCBotHomOfBotHomClass`, `instCoeTCBoundedOrderHomOfBoundedOrderHomClass`, `instCoeTCTopHomOfTopHomClass`	55
Theorems `bot_apply`, `cancel_left`, `cancel_right`, `coe_bot`, `coe_comp`, `coe_copy`, `coe_id`, `coe_inf`, `coe_sup`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `dual_apply_apply`, `dual_comp`, `dual_id`, `dual_symm_apply_apply`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `inf_apply`, `instBotHomClass`, `map_bot'`, `sup_apply`, `symm_dual_comp`, `symm_dual_id`, `map_bot`, `cancel_left`, `cancel_right`, `coe_comp`, `coe_comp_botHom`, `coe_comp_orderHom`, `coe_comp_topHom`, `coe_copy`, `coe_id`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `dual_apply_toOrderHom`, `dual_comp`, `dual_id`, `dual_symm_apply_toOrderHom`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `instBoundedOrderHomClass`, `map_bot'`, `map_top'`, `symm_dual_comp`, `symm_dual_id`, `map_bot`, `map_top`, `toBotHomClass`, `toRelHomClass`, `toTopHomClass`, `toBotHomClass`, `toBoundedOrderHomClass`, `toTopHomClass`, `cancel_left`, `cancel_right`, `coe_comp`, `coe_copy`, `coe_id`, `coe_inf`, `coe_sup`, `coe_top`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `dual_apply_apply`, `dual_comp`, `dual_id`, `dual_symm_apply_apply`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `inf_apply`, `instTopHomClass`, `map_top'`, `sup_apply`, `symm_dual_comp`, `symm_dual_id`, `top_apply`, `map_top`, `map_eq_bot_iff`, `map_eq_top_iff`	91
Total	146

BotHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	12 math math: `cancel_right`, `coe_comp`, `comp_assoc`, `BoundedOrderHom.coe_comp_botHom`, `cancel_left`, `TopHom.symm_dual_comp`, `comp_id`, `id_comp`, `symm_dual_comp`, `dual_comp`, `TopHom.dual_comp`, `comp_apply`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`dual` 📖	CompOp	6 math math: `dual_apply_apply`, `dual_symm_apply_apply`, `symm_dual_id`, `symm_dual_comp`, `dual_comp`, `dual_id`
`id` 📖	CompOp	8 math math: `TopHom.symm_dual_id`, `id_apply`, `coe_id`, `comp_id`, `symm_dual_id`, `id_comp`, `dual_id`, `TopHom.dual_id`
`instDistribLattice` 📖	CompOp	—
`instFunLike` 📖	CompOp	18 math math: `bot_apply`, `coe_comp`, `dual_apply_apply`, `id_apply`, `SupBotHom.coe_toBotHom`, `coe_copy`, `TopHom.dual_symm_apply_apply`, `instBotHomClass`, `coe_bot`, `sup_apply`, `ext_iff`, `dual_symm_apply_apply`, `coe_id`, `TopHom.dual_apply_apply`, `coe_sup`, `inf_apply`, `comp_apply`, `coe_inf`
`instInhabited` 📖	CompOp	—
`instLE` 📖	CompOp	2 math math: `bot_apply`, `coe_bot`
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	2 math math: `sup_apply`, `coe_sup`
`instMin` 📖	CompOp	2 math math: `inf_apply`, `coe_inf`
`instOrderBot` 📖	CompOp	2 math math: `bot_apply`, `coe_bot`
`instPartialOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	—
`instSemilatticeInf` 📖	CompOp	—
`instSemilatticeSup` 📖	CompOp	—
`toFun` 📖	CompOp	1 math math: `map_bot'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_apply` 📖	mathematical	—	`DFunLike.coe` `BotHom` `OrderBot.toBot` `instFunLike` `Bot.bot` `instLE` `instOrderBot`	—	—
`cancel_left` 📖	mathematical	`DFunLike.coe` `BotHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `BotHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_bot` 📖	mathematical	—	`DFunLike.coe` `BotHom` `OrderBot.toBot` `instFunLike` `Bot.bot` `instLE` `instOrderBot` `Pi.instBotForall`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `BotHom` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `BotHom` `instFunLike`	`DFunLike.coe` `BotHom` `instFunLike` `copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `BotHom` `instFunLike` `id`	—	—
`coe_inf` 📖	mathematical	—	`DFunLike.coe` `BotHom` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `instFunLike` `instMin` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `BotHom` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLike` `instMax` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `BotHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `BotHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`dual_apply_apply` 📖	mathematical	—	`DFunLike.coe` `TopHom` `OrderDual` `OrderDual.instTopOfBot` `OrderBot.toBot` `TopHom.instFunLike` `Equiv` `BotHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `instFunLike`	—	—
`dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BotHom` `OrderBot.toBot` `TopHom` `OrderDual` `OrderDual.instTopOfBot` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `comp` `TopHom.comp`	—	—
`dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BotHom` `OrderBot.toBot` `TopHom` `OrderDual` `OrderDual.instTopOfBot` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `id` `TopHom.id`	—	—
`dual_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `BotHom` `OrderBot.toBot` `instFunLike` `Equiv` `TopHom` `OrderDual` `OrderDual.instTopOfBot` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `TopHom.instFunLike`	—	—
`ext` 📖	—	`DFunLike.coe` `BotHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `BotHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `BotHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`inf_apply` 📖	mathematical	—	`DFunLike.coe` `BotHom` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `instFunLike` `instMin` `SemilatticeInf.toMin`	—	—
`instBotHomClass` 📖	mathematical	—	`BotHomClass` `BotHom` `instFunLike`	—	`map_bot'`
`map_bot'` 📖	mathematical	—	`toFun` `Bot.bot`	—	—
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `BotHom` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLike` `instMax` `SemilatticeSup.toMax`	—	—
`symm_dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TopHom` `OrderDual` `OrderDual.instTopOfBot` `OrderBot.toBot` `BotHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `TopHom.comp` `comp`	—	—
`symm_dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TopHom` `OrderDual` `OrderDual.instTopOfBot` `OrderBot.toBot` `BotHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `TopHom.id` `id`	—	—

BotHomClass

Definitions

Name	Category	Theorems
`toBotHom` 📖	CompOp	1 math math: `BoundedOrderHom.coe_comp_botHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_bot` 📖	mathematical	—	`DFunLike.coe` `Bot.bot`	—	—

BoundedOrderHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	14 math math: `comp_apply`, `symm_dual_comp`, `coe_comp_botHom`, `coe_comp`, `coe_comp_topHom`, `dual_comp`, `comp_id`, `cancel_left`, `BddOrd.hom_comp`, `coe_comp_orderHom`, `BddOrd.ofHom_comp`, `cancel_right`, `id_comp`, `comp_assoc`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`dual` 📖	CompOp	7 math math: `symm_dual_id`, `dual_apply_toOrderHom`, `BddOrd.dual_map`, `dual_id`, `symm_dual_comp`, `dual_comp`, `dual_symm_apply_toOrderHom`
`id` 📖	CompOp	8 math math: `symm_dual_id`, `BddOrd.hom_id`, `dual_id`, `comp_id`, `coe_id`, `BddOrd.ofHom_id`, `id_apply`, `id_comp`
`instFunLike` 📖	CompOp	27 math math: `bddOrd_dual_comp_forget_to_bipointed`, `BddOrd.coe_id`, `comp_apply`, `BddOrd.ext_iff`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `bddOrd_dual_comp_forget_to_partOrd`, `coe_comp_botHom`, `coe_comp`, `BddOrd.forget_map`, `coe_comp_topHom`, `BddOrd.id_apply`, `bddLat_dual_comp_forget_to_bddOrd`, `BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `coe_id`, `BoundedLatticeHom.coe_toBoundedOrderHom`, `coe_comp_orderHom`, `BddOrd.hom_inv_apply`, `BddOrd.comp_apply`, `BddLat.coe_forget_to_bddOrd`, `BddOrd.ofHom_apply`, `coe_copy`, `BddOrd.coe_comp`, `instBoundedOrderHomClass`, `ext_iff`, `id_apply`, `BddOrd.inv_hom_apply`
`instInhabited` 📖	CompOp	—
`toBotHom` 📖	CompOp	—
`toOrderHom` 📖	CompOp	4 math math: `dual_apply_toOrderHom`, `dual_symm_apply_toOrderHom`, `map_top'`, `map_bot'`
`toTopHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `BoundedOrderHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `BoundedOrderHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `BoundedOrderHom` `instFunLike` `comp`	—	—
`coe_comp_botHom` 📖	mathematical	—	`BotHomClass.toBotHom` `BoundedOrderHom` `instFunLike` `OrderBot.toBot` `Preorder.toLE` `BoundedOrder.toOrderBot` `BoundedOrderHomClass.toBotHomClass` `instBoundedOrderHomClass` `comp` `BotHom.comp`	—	`BoundedOrderHomClass.toBotHomClass` `instBoundedOrderHomClass`
`coe_comp_orderHom` 📖	mathematical	—	`OrderHomClass.toOrderHom` `BoundedOrderHom` `instFunLike` `BoundedOrderHomClass.toRelHomClass` `Preorder.toLE` `instBoundedOrderHomClass` `comp` `OrderHom.comp`	—	`BoundedOrderHomClass.toRelHomClass` `instBoundedOrderHomClass`
`coe_comp_topHom` 📖	mathematical	—	`TopHomClass.toTopHom` `BoundedOrderHom` `instFunLike` `OrderTop.toTop` `Preorder.toLE` `BoundedOrder.toOrderTop` `BoundedOrderHomClass.toTopHomClass` `instBoundedOrderHomClass` `comp` `TopHom.comp`	—	`BoundedOrderHomClass.toTopHomClass` `instBoundedOrderHomClass`
`coe_copy` 📖	mathematical	`DFunLike.coe` `BoundedOrderHom` `instFunLike`	`DFunLike.coe` `BoundedOrderHom` `instFunLike` `copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `BoundedOrderHom` `instFunLike` `id`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedOrderHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `BoundedOrderHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`dual_apply_toOrderHom` 📖	mathematical	—	`toOrderHom` `OrderDual` `OrderDual.instPreorder` `OrderDual.instBoundedOrder` `Preorder.toLE` `DFunLike.coe` `Equiv` `BoundedOrderHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `OrderHom` `OrderHom.dual`	—	—
`dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BoundedOrderHom` `OrderDual` `OrderDual.instPreorder` `OrderDual.instBoundedOrder` `Preorder.toLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `comp`	—	—
`dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BoundedOrderHom` `OrderDual` `OrderDual.instPreorder` `OrderDual.instBoundedOrder` `Preorder.toLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `id`	—	—
`dual_symm_apply_toOrderHom` 📖	mathematical	—	`toOrderHom` `DFunLike.coe` `Equiv` `BoundedOrderHom` `OrderDual` `OrderDual.instPreorder` `OrderDual.instBoundedOrder` `Preorder.toLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `OrderHom` `OrderHom.dual`	—	—
`ext` 📖	—	`DFunLike.coe` `BoundedOrderHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `BoundedOrderHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedOrderHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instBoundedOrderHomClass` 📖	mathematical	—	`BoundedOrderHomClass` `BoundedOrderHom` `Preorder.toLE` `instFunLike`	—	`OrderHom.monotone'` `map_top'` `map_bot'`
`map_bot'` 📖	mathematical	—	`OrderHom.toFun` `toOrderHom` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `BoundedOrder.toOrderBot`	—	—
`map_top'` 📖	mathematical	—	`OrderHom.toFun` `toOrderHom` `Top.top` `OrderTop.toTop` `Preorder.toLE` `BoundedOrder.toOrderTop`	—	—
`symm_dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BoundedOrderHom` `OrderDual` `OrderDual.instPreorder` `OrderDual.instBoundedOrder` `Preorder.toLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `comp`	—	—
`symm_dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BoundedOrderHom` `OrderDual` `OrderDual.instPreorder` `OrderDual.instBoundedOrder` `Preorder.toLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `id`	—	—

BoundedOrderHomClass

Definitions

Name	Category	Theorems
`toBoundedOrderHom` 📖	CompOp	2 math math: `BddOrd.Iso.mk_hom`, `BddOrd.Iso.mk_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_bot` 📖	mathematical	—	`DFunLike.coe` `Bot.bot` `OrderBot.toBot` `BoundedOrder.toOrderBot`	—	—
`map_top` 📖	mathematical	—	`DFunLike.coe` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop`	—	—
`toBotHomClass` 📖	mathematical	—	`BotHomClass` `OrderBot.toBot` `BoundedOrder.toOrderBot`	—	`map_bot`
`toRelHomClass` 📖	mathematical	—	`RelHomClass`	—	—
`toTopHomClass` 📖	mathematical	—	`TopHomClass` `OrderTop.toTop` `BoundedOrder.toOrderTop`	—	`map_top`

OrderIsoClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBotHomClass` 📖	mathematical	—	`BotHomClass` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `EquivLike.toFunLike`	—	`le_bot_iff` `le_map_inv_iff` `bot_le`
`toBoundedOrderHomClass` 📖	mathematical	—	`BoundedOrderHomClass` `Preorder.toLE` `PartialOrder.toPreorder` `EquivLike.toFunLike`	—	`toTopHomClass` `toBotHomClass` `toOrderHomClass` `TopHomClass.map_top` `BotHomClass.map_bot`
`toTopHomClass` 📖	mathematical	—	`TopHomClass` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `EquivLike.toFunLike`	—	`top_le_iff` `map_inv_le_iff` `le_top`

TopHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	12 math math: `cancel_right`, `BoundedOrderHom.coe_comp_topHom`, `comp_id`, `symm_dual_comp`, `coe_comp`, `BotHom.symm_dual_comp`, `BotHom.dual_comp`, `cancel_left`, `comp_assoc`, `dual_comp`, `comp_apply`, `id_comp`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`dual` 📖	CompOp	6 math math: `symm_dual_id`, `dual_symm_apply_apply`, `symm_dual_comp`, `dual_apply_apply`, `dual_comp`, `dual_id`
`id` 📖	CompOp	8 math math: `symm_dual_id`, `comp_id`, `BotHom.symm_dual_id`, `coe_id`, `BotHom.dual_id`, `id_apply`, `id_comp`, `dual_id`
`instDistribLattice` 📖	CompOp	—
`instFunLike` 📖	CompOp	18 math math: `instTopHomClass`, `BotHom.dual_apply_apply`, `coe_top`, `coe_inf`, `dual_symm_apply_apply`, `sup_apply`, `ext_iff`, `inf_apply`, `coe_copy`, `coe_sup`, `BotHom.dual_symm_apply_apply`, `top_apply`, `dual_apply_apply`, `coe_comp`, `coe_id`, `comp_apply`, `id_apply`, `InfTopHom.coe_toTopHom`
`instInhabited` 📖	CompOp	—
`instLE` 📖	CompOp	2 math math: `coe_top`, `top_apply`
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	2 math math: `sup_apply`, `coe_sup`
`instMin` 📖	CompOp	2 math math: `coe_inf`, `inf_apply`
`instOrderTop` 📖	CompOp	2 math math: `coe_top`, `top_apply`
`instPartialOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	—
`instSemilatticeInf` 📖	CompOp	—
`instSemilatticeSup` 📖	CompOp	—
`toFun` 📖	CompOp	1 math math: `map_top'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `TopHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `TopHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `TopHom` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `TopHom` `instFunLike`	`DFunLike.coe` `TopHom` `instFunLike` `copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `TopHom` `instFunLike` `id`	—	—
`coe_inf` 📖	mathematical	—	`DFunLike.coe` `TopHom` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `instFunLike` `instMin` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `TopHom` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLike` `instMax` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax`	—	—
`coe_top` 📖	mathematical	—	`DFunLike.coe` `TopHom` `OrderTop.toTop` `instFunLike` `Top.top` `instLE` `instOrderTop` `Pi.instTopForall`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `TopHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `TopHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`dual_apply_apply` 📖	mathematical	—	`DFunLike.coe` `BotHom` `OrderDual` `OrderDual.instBotOfTop` `OrderTop.toTop` `BotHom.instFunLike` `Equiv` `TopHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `instFunLike`	—	—
`dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TopHom` `OrderTop.toTop` `BotHom` `OrderDual` `OrderDual.instBotOfTop` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `comp` `BotHom.comp`	—	—
`dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TopHom` `OrderTop.toTop` `BotHom` `OrderDual` `OrderDual.instBotOfTop` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `id` `BotHom.id`	—	—
`dual_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `TopHom` `OrderTop.toTop` `instFunLike` `Equiv` `BotHom` `OrderDual` `OrderDual.instBotOfTop` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `BotHom.instFunLike`	—	—
`ext` 📖	—	`DFunLike.coe` `TopHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `TopHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `TopHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`inf_apply` 📖	mathematical	—	`DFunLike.coe` `TopHom` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `instFunLike` `instMin` `SemilatticeInf.toMin`	—	—
`instTopHomClass` 📖	mathematical	—	`TopHomClass` `TopHom` `instFunLike`	—	`map_top'`
`map_top'` 📖	mathematical	—	`toFun` `Top.top`	—	—
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `TopHom` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLike` `instMax` `SemilatticeSup.toMax`	—	—
`symm_dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BotHom` `OrderDual` `OrderDual.instBotOfTop` `OrderTop.toTop` `TopHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `BotHom.comp` `comp`	—	—
`symm_dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BotHom` `OrderDual` `OrderDual.instBotOfTop` `OrderTop.toTop` `TopHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `BotHom.id` `id`	—	—
`top_apply` 📖	mathematical	—	`DFunLike.coe` `TopHom` `OrderTop.toTop` `instFunLike` `Top.top` `instLE` `instOrderTop`	—	—

TopHomClass

Definitions

Name	Category	Theorems
`toTopHom` 📖	CompOp	1 math math: `BoundedOrderHom.coe_comp_topHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_top` 📖	mathematical	—	`DFunLike.coe` `Top.top`	—	—

(root)

Definitions

Name	Category	Theorems
`BotHom` 📖	CompData	26 math math: `BotHom.bot_apply`, `TopHom.symm_dual_id`, `BotHom.coe_comp`, `BotHom.dual_apply_apply`, `BotHom.id_apply`, `SupBotHom.coe_toBotHom`, `BotHom.coe_copy`, `TopHom.dual_symm_apply_apply`, `BotHom.instBotHomClass`, `BotHom.coe_bot`, `BotHom.sup_apply`, `BotHom.ext_iff`, `BotHom.dual_symm_apply_apply`, `BotHom.coe_id`, `TopHom.symm_dual_comp`, `TopHom.dual_apply_apply`, `BotHom.symm_dual_id`, `BotHom.coe_sup`, `BotHom.symm_dual_comp`, `BotHom.dual_comp`, `BotHom.dual_id`, `TopHom.dual_comp`, `BotHom.inf_apply`, `BotHom.comp_apply`, `BotHom.coe_inf`, `TopHom.dual_id`
`BotHomClass` 📖	CompData	4 math math: `BotHom.instBotHomClass`, `OrderIsoClass.toBotHomClass`, `BoundedOrderHomClass.toBotHomClass`, `SupBotHomClass.toBotHomClass`
`BoundedOrderHom` 📖	CompData	34 math math: `BoundedOrderHom.symm_dual_id`, `bddOrd_dual_comp_forget_to_bipointed`, `BddOrd.coe_id`, `BoundedOrderHom.comp_apply`, `BddOrd.ext_iff`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `BoundedOrderHom.dual_apply_toOrderHom`, `BddOrd.dual_map`, `BoundedOrderHom.dual_id`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `bddOrd_dual_comp_forget_to_partOrd`, `BoundedOrderHom.symm_dual_comp`, `BoundedOrderHom.coe_comp_botHom`, `BoundedOrderHom.coe_comp`, `BddOrd.forget_map`, `BoundedOrderHom.coe_comp_topHom`, `BoundedOrderHom.dual_comp`, `BddOrd.id_apply`, `bddLat_dual_comp_forget_to_bddOrd`, `BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `BoundedOrderHom.coe_id`, `BoundedOrderHom.dual_symm_apply_toOrderHom`, `BoundedLatticeHom.coe_toBoundedOrderHom`, `BoundedOrderHom.coe_comp_orderHom`, `BddOrd.hom_inv_apply`, `BddOrd.comp_apply`, `BddLat.coe_forget_to_bddOrd`, `BddOrd.ofHom_apply`, `BoundedOrderHom.coe_copy`, `BddOrd.coe_comp`, `BoundedOrderHom.instBoundedOrderHomClass`, `BoundedOrderHom.ext_iff`, `BoundedOrderHom.id_apply`, `BddOrd.inv_hom_apply`
`BoundedOrderHomClass` 📖	CompData	3 math math: `BoundedLatticeHomClass.toBoundedOrderHomClass`, `BoundedOrderHom.instBoundedOrderHomClass`, `OrderIsoClass.toBoundedOrderHomClass`
`TopHom` 📖	CompData	26 math math: `TopHom.symm_dual_id`, `TopHom.instTopHomClass`, `BotHom.dual_apply_apply`, `TopHom.coe_top`, `TopHom.coe_inf`, `TopHom.dual_symm_apply_apply`, `TopHom.sup_apply`, `TopHom.ext_iff`, `TopHom.inf_apply`, `TopHom.coe_copy`, `TopHom.coe_sup`, `BotHom.dual_symm_apply_apply`, `TopHom.top_apply`, `TopHom.symm_dual_comp`, `TopHom.dual_apply_apply`, `BotHom.symm_dual_id`, `TopHom.coe_comp`, `TopHom.coe_id`, `BotHom.symm_dual_comp`, `BotHom.dual_comp`, `BotHom.dual_id`, `TopHom.dual_comp`, `TopHom.comp_apply`, `TopHom.id_apply`, `InfTopHom.coe_toTopHom`, `TopHom.dual_id`
`TopHomClass` 📖	CompData	6 math math: `Nucleus.instTopHomClass`, `TopHom.instTopHomClass`, `OrderIsoClass.toTopHomClass`, `PseudoEpimorphismClass.toTopHomClass`, `BoundedOrderHomClass.toTopHomClass`, `InfTopHomClass.toTopHomClass`
`instCoeTCBotHomOfBotHomClass` 📖	CompOp	—
`instCoeTCBoundedOrderHomOfBoundedOrderHomClass` 📖	CompOp	—
`instCoeTCTopHomOfTopHomClass` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_eq_bot_iff` 📖	mathematical	—	`DFunLike.coe` `EquivLike.toFunLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder`	—	`BotHomClass.map_bot` `OrderIsoClass.toBotHomClass` `EquivLike.injective`
`map_eq_top_iff` 📖	mathematical	—	`DFunLike.coe` `EquivLike.toFunLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder`	—	`TopHomClass.map_top` `OrderIsoClass.toTopHomClass` `EquivLike.injective`

---

← Back to Index