BoundedLattice

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

Statistics

Metric	Count
Definitions `BoundedLatticeHom`, `comp`, `copy`, `dual`, `id`, `instFunLike`, `instInhabited`, `subtypeVal`, `toBoundedOrderHom`, `toInfTopHom`, `toLatticeHom`, `toSupBotHom`, `BoundedLatticeHomClass`, `InfTopHom`, `comp`, `copy`, `dual`, `id`, `instFunLike`, `instInhabited`, `instMin`, `instOrderTop`, `instPartialOrder`, `instSemilatticeInf`, `subtypeVal`, `toInfHom`, `toTopHom`, `InfTopHomClass`, `SupBotHom`, `comp`, `copy`, `dual`, `id`, `instFunLike`, `instInhabited`, `instMax`, `instOrderBot`, `instPartialOrder`, `instSemilatticeSup`, `subtypeVal`, `toBotHom`, `toSupHom`, `SupBotHomClass`, `instCoeTCBoundedLatticeHomOfBoundedLatticeHomClass`, `instCoeTCInfTopHomOfInfTopHomClass`, `instCoeTCSupBotHomOfSupBotHomClass`	46
Theorems `cancel_left`, `cancel_right`, `coe_comp`, `coe_comp_inf_hom`, `coe_comp_inf_hom'`, `coe_comp_lattice_hom`, `coe_comp_lattice_hom'`, `coe_comp_sup_hom`, `coe_comp_sup_hom'`, `coe_copy`, `coe_id`, `coe_mk`, `coe_toBoundedOrderHom`, `coe_toInfTopHom`, `coe_toLatticeHom`, `coe_toSupBotHom`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `dual_apply_toFun`, `dual_comp`, `dual_id`, `dual_symm_apply_toFun`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `instBoundedLatticeHomClass`, `map_bot'`, `map_top'`, `subtypeVal_apply`, `subtypeVal_coe`, `symm_dual_comp`, `symm_dual_id`, `toFun_eq_coe`, `map_bot`, `map_top`, `toBoundedOrderHomClass`, `toInfTopHomClass`, `toLatticeHomClass`, `toSupBotHomClass`, `map`, `map`, `cancel_left`, `cancel_right`, `coe_comp`, `coe_copy`, `coe_id`, `coe_inf`, `coe_mk`, `coe_toInfHom`, `coe_toTopHom`, `coe_top`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `dual_apply_toFun`, `dual_comp`, `dual_id`, `dual_symm_apply_toFun`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `id_toFun`, `inf_apply`, `instInfTopHomClass`, `map_top'`, `subtypeVal_apply`, `subtypeVal_coe`, `symm_dual_comp`, `symm_dual_id`, `toFun_eq_coe`, `top_apply`, `map_top`, `toInfHomClass`, `toTopHomClass`, `map`, `toBoundedLatticeHomClass`, `toInfTopHomClass`, `toSupBotHomClass`, `bot_apply`, `cancel_left`, `cancel_right`, `coe_bot`, `coe_comp`, `coe_copy`, `coe_id`, `coe_mk`, `coe_sup`, `coe_toBotHom`, `coe_toSupHom`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `dual_comp`, `dual_id`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `id_toFun`, `instSupBotHomClass`, `map_bot'`, `subtypeVal_apply`, `subtypeVal_coe`, `sup_apply`, `symm_dual_comp`, `symm_dual_id`, `toFun_eq_coe`, `map_bot`, `toBotHomClass`, `toSupHomClass`, `map_compl'`, `map_sdiff'`, `map_symmDiff'`	119
Total	165

BoundedLatticeHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	27 math math: `cancel_right`, `BooleanSubalgebra.map_map`, `FinBddDistLat.ofHom_comp`, `coe_comp_sup_hom'`, `comp_id`, `symm_dual_comp`, `LatticeHom.withTopWithBot_comp`, `BooleanSubalgebra.subtype_comp_inclusion`, `BoolAlg.ofHom_comp`, `coe_comp_lattice_hom'`, `id_comp`, `coe_comp_sup_hom`, `cancel_left`, `BoolAlg.hom_comp`, `RingHom.asBoolAlg_comp`, `FinBddDistLat.hom_comp`, `asBoolRing_comp`, `BddDistLat.ofHom_comp`, `dual_comp`, `coe_comp`, `BddDistLat.hom_comp`, `coe_comp_inf_hom'`, `comp_apply`, `coe_comp_inf_hom`, `coe_comp_lattice_hom`, `comp_assoc`, `BooleanSubalgebra.comap_comap`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`dual` 📖	CompOp	11 math math: `dual_id`, `symm_dual_comp`, `dual_symm_apply_toFun`, `BddDistLat.dual_map`, `symm_dual_id`, `BoolAlg.dual_map`, `dual_apply_toFun`, `dual_comp`, `FinBddDistLat.dual_map`, `FinBoolAlg.dual_map`, `BddLat.dual_map`
`id` 📖	CompOp	18 math math: `dual_id`, `comp_id`, `LatticeHom.withTopWithBot_id`, `BddDistLat.hom_id`, `BddDistLat.ofHom_id`, `BoolAlg.hom_id`, `id_comp`, `BooleanSubalgebra.comap_id`, `symm_dual_id`, `RingHom.asBoolAlg_id`, `BoolAlg.ofHom_id`, `asBoolRing_id`, `BooleanSubalgebra.inclusion_rfl`, `BooleanSubalgebra.map_id`, `coe_id`, `FinBddDistLat.hom_id`, `FinBddDistLat.ofHom_id`, `id_apply`
`instFunLike` 📖	CompOp	105 math math: `BoolAlg.coe_id`, `coe_toLatticeHom`, `LatticeHom.withTopWithBot_apply`, `CompleteLatticeHom.coe_toBoundedLatticeHom`, `BoolRing.hasForgetToBoolAlg_forget₂_obj_coe`, `HeytAlg.hasForgetToLat_forget₂_map`, `BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier`, `coe_comp_sup_hom'`, `LatticeHom.coe_withTopWithBot`, `BoolAlg.ext_iff`, `FinBddDistLat.ofHom_apply`, `BoolAlg.hasForgetToBoolRing_forget₂_map`, `BddDistLat.coe_id`, `HeytAlg.hasForgetToLat_forget₂_obj_str`, `FinBddDistLat.hom_inv_apply`, `HeytAlg.hasForgetToLat_forget₂_obj_carrier`, `bddLat_dual_comp_forget_to_lat`, `boolRingCatEquivBoolAlg_functor`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `FinBddDistLat.ext_iff`, `BooleanSubalgebra.mem_comap`, `LatticeHom.withTopWithBot'_toFun`, `FinBddDistLat.coe_id`, `BooleanSubalgebra.coe_map`, `FinBddDistLat.inv_hom_apply`, `finBddDistLat_dual_comp_forget_to_bddDistLat`, `coe_comp_lattice_hom'`, `BoolAlg.hasForgetToHeytAlg_forget₂_map`, `FinBddDistLat.forget_map`, `BddDistLat.coe_comp`, `FinBoolAlg.forgetToFinPartOrdFaithful`, `coe_comp_sup_hom`, `BooleanSubalgebra.subtype_injective`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `coe_toSupBotHom`, `BooleanSubalgebra.apply_coe_mem_map`, `BddDistLat.forget_map`, `dual_symm_apply_toFun`, `BooleanSubalgebra.coe_inclusion`, `ext_iff`, `FinBddDistLat.comp_apply`, `bddLat_dual_comp_forget_to_semilatSupCat`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier`, `BooleanSubalgebra.mem_map_of_mem`, `subtypeVal_coe`, `BddDistLat.inv_hom_apply`, `LatticeHom.withTopWithBot_toFun`, `BooleanSubalgebra.subtype_apply`, `bddLat_dual_comp_forget_to_semilatInfCat`, `BooleanSubalgebra.inclusion_injective`, `toFun_eq_coe`, `BddDistLat.ofHom_apply`, `boolRingCatEquivBoolAlg_inverse`, `BoolAlg.coe_comp`, `asBoolRing_apply`, `HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder`, `BoolRing.hasForgetToBoolAlg_forget₂_map`, `BoolAlg.hom_inv_apply`, `dual_apply_toFun`, `BddDistLat.id_apply`, `bddLat_dual_comp_forget_to_bddOrd`, `BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype`, `BooleanSubalgebra.mem_map`, `BddLat.coe_forget_to_lat`, `BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat`, `BoolAlg.comp_apply`, `finBoolAlg_dual_comp_forget_to_finBddDistLat`, `completeLat_dual_comp_forget_to_bddLat`, `coe_toBoundedOrderHom`, `BddLat.coe_forget_to_semilatSup`, `FinBddDistLat.coe_comp`, `BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe`, `BooleanSubalgebra.coe_subtype`, `instBoundedLatticeHomClass`, `BddDistLat.ext_iff`, `coe_toInfTopHom`, `coe_comp`, `BooleanSubalgebra.coe_comap`, `BddLat.coe_forget_to_bddOrd`, `BoolAlg.inv_hom_apply`, `BddLat.coe_forget_to_semilatInf`, `boolAlg_dual_comp_forget_to_bddDistLat`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_map`, `FinBoolAlg.forgetToBoolAlg_full`, `FinBddDistLat.id_apply`, `BddDistLat.comp_apply`, `BddLat.ext_iff`, `bddDistLat_dual_comp_forget_to_distLat`, `BooleanSubalgebra.inclusion_apply`, `coe_comp_inf_hom'`, `comp_apply`, `coe_mk`, `coe_comp_inf_hom`, `coe_id`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str`, `BoolAlg.id_apply`, `BddDistLat.hom_inv_apply`, `subtypeVal_apply`, `FinBoolAlg.forgetToBoolAlgFaithful`, `coe_comp_lattice_hom`, `id_apply`, `BoolAlg.ofHom_apply`, `BoolAlg.forget_map`, `RingHom.asBoolAlg_toFun`
`instInhabited` 📖	CompOp	—
`subtypeVal` 📖	CompOp	2 math math: `subtypeVal_coe`, `subtypeVal_apply`
`toBoundedOrderHom` 📖	CompOp	1 math math: `coe_toBoundedOrderHom`
`toInfTopHom` 📖	CompOp	1 math math: `coe_toInfTopHom`
`toLatticeHom` 📖	CompOp	4 math math: `coe_toLatticeHom`, `map_top'`, `map_bot'`, `toFun_eq_coe`
`toSupBotHom` 📖	CompOp	1 math math: `coe_toSupBotHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `BoundedLatticeHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `BoundedLatticeHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `instFunLike` `comp`	—	—
`coe_comp_inf_hom` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DFunLike.coe` `BoundedLatticeHom` `instFunLike` `comp` `InfHomClass.map_inf` `InfTopHomClass.toInfHomClass` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `BoundedOrder.toOrderTop` `BoundedLatticeHomClass.toInfTopHomClass` `instBoundedLatticeHomClass` `InfHom.comp`	—	`InfHomClass.map_inf` `InfTopHomClass.toInfHomClass` `BoundedLatticeHomClass.toInfTopHomClass` `instBoundedLatticeHomClass`
`coe_comp_inf_hom'` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DFunLike.coe` `BoundedLatticeHom` `instFunLike` `InfHomClass.map_inf` `InfTopHomClass.toInfHomClass` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `BoundedOrder.toOrderTop` `BoundedLatticeHomClass.toInfTopHomClass` `instBoundedLatticeHomClass` `comp` `InfHom.comp`	—	`InfHomClass.map_inf` `InfTopHomClass.toInfHomClass` `BoundedLatticeHomClass.toInfTopHomClass` `instBoundedLatticeHomClass`
`coe_comp_lattice_hom` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DFunLike.coe` `BoundedLatticeHom` `instFunLike` `comp` `BoundedLatticeHomClass.toLatticeHomClass` `instBoundedLatticeHomClass` `LatticeHom.comp`	—	`BoundedLatticeHomClass.toLatticeHomClass` `instBoundedLatticeHomClass`
`coe_comp_lattice_hom'` 📖	mathematical	—	`SupHom.comp` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DFunLike.coe` `BoundedLatticeHom` `instFunLike` `SupHomClass.map_sup` `SupBotHomClass.toSupHomClass` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderBot` `BoundedLatticeHomClass.toSupBotHomClass` `instBoundedLatticeHomClass` `InfHomClass.map_inf` `SemilatticeInf.toMin` `InfTopHomClass.toInfHomClass` `OrderTop.toTop` `BoundedOrder.toOrderTop` `BoundedLatticeHomClass.toInfTopHomClass` `comp` `LatticeHom.comp` `BoundedLatticeHomClass.toLatticeHomClass`	—	`SupHomClass.map_sup` `SupBotHomClass.toSupHomClass` `BoundedLatticeHomClass.toSupBotHomClass` `instBoundedLatticeHomClass` `InfHomClass.map_inf` `InfTopHomClass.toInfHomClass` `BoundedLatticeHomClass.toInfTopHomClass`
`coe_comp_sup_hom` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DFunLike.coe` `BoundedLatticeHom` `instFunLike` `comp` `SupHomClass.map_sup` `SupBotHomClass.toSupHomClass` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderBot` `BoundedLatticeHomClass.toSupBotHomClass` `instBoundedLatticeHomClass` `SupHom.comp`	—	`SupHomClass.map_sup` `SupBotHomClass.toSupHomClass` `BoundedLatticeHomClass.toSupBotHomClass` `instBoundedLatticeHomClass`
`coe_comp_sup_hom'` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DFunLike.coe` `BoundedLatticeHom` `instFunLike` `SupHomClass.map_sup` `SupBotHomClass.toSupHomClass` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderBot` `BoundedLatticeHomClass.toSupBotHomClass` `instBoundedLatticeHomClass` `comp` `SupHom.comp`	—	`SupHomClass.map_sup` `SupBotHomClass.toSupHomClass` `BoundedLatticeHomClass.toSupBotHomClass` `instBoundedLatticeHomClass`
`coe_copy` 📖	mathematical	`DFunLike.coe` `BoundedLatticeHom` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `instFunLike` `id`	—	—
`coe_mk` 📖	mathematical	`SupHom.toFun` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `LatticeHom.toSupHom` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderTop` `Bot.bot` `OrderBot.toBot` `BoundedOrder.toOrderBot`	`DFunLike.coe` `BoundedLatticeHom` `instFunLike` `LatticeHom` `LatticeHom.instFunLike`	—	—
`coe_toBoundedOrderHom` 📖	mathematical	—	`DFunLike.coe` `BoundedOrderHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrderHom.instFunLike` `toBoundedOrderHom` `BoundedLatticeHom` `instFunLike`	—	—
`coe_toInfTopHom` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `BoundedOrder.toOrderTop` `InfTopHom.instFunLike` `toInfTopHom` `BoundedLatticeHom` `instFunLike`	—	—
`coe_toLatticeHom` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `LatticeHom.instFunLike` `toLatticeHom` `BoundedLatticeHom` `instFunLike`	—	—
`coe_toSupBotHom` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderBot` `SupBotHom.instFunLike` `toSupBotHom` `BoundedLatticeHom` `instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`copy_eq` 📖	mathematical	`DFunLike.coe` `BoundedLatticeHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`dual_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `OrderDual` `OrderDual.instLattice` `OrderDual.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual`	—	—
`dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BoundedLatticeHom` `OrderDual` `OrderDual.instLattice` `OrderDual.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `comp`	—	—
`dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BoundedLatticeHom` `OrderDual` `OrderDual.instLattice` `OrderDual.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `id`	—	—
`dual_symm_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `instFunLike` `Equiv` `OrderDual` `OrderDual.instLattice` `OrderDual.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual`	—	—
`ext` 📖	—	`DFunLike.coe` `BoundedLatticeHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`instBoundedLatticeHomClass` 📖	mathematical	—	`BoundedLatticeHomClass` `BoundedLatticeHom` `instFunLike`	—	`SupHom.map_sup'` `LatticeHom.map_inf'` `map_top'` `map_bot'`
`map_bot'` 📖	mathematical	—	`SupHom.toFun` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `LatticeHom.toSupHom` `toLatticeHom` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderBot`	—	—
`map_top'` 📖	mathematical	—	`SupHom.toFun` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `LatticeHom.toSupHom` `toLatticeHom` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderTop`	—	—
`subtypeVal_apply` 📖	mathematical	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderBot` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin`	`DFunLike.coe` `BoundedLatticeHom` `Subtype.lattice` `Subtype.boundedOrder` `instFunLike` `subtypeVal`	—	—
`subtypeVal_coe` 📖	mathematical	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderBot` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin`	`DFunLike.coe` `BoundedLatticeHom` `Subtype.lattice` `Subtype.boundedOrder` `instFunLike` `subtypeVal`	—	—
`symm_dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BoundedLatticeHom` `OrderDual` `OrderDual.instLattice` `OrderDual.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `comp`	—	—
`symm_dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `BoundedLatticeHom` `OrderDual` `OrderDual.instLattice` `OrderDual.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `id`	—	—
`toFun_eq_coe` 📖	mathematical	—	`SupHom.toFun` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `LatticeHom.toSupHom` `toLatticeHom` `DFunLike.coe` `BoundedLatticeHom` `instFunLike`	—	—

BoundedLatticeHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_bot` 📖	mathematical	—	`DFunLike.coe` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderBot`	—	—
`map_top` 📖	mathematical	—	`DFunLike.coe` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderTop`	—	—
`toBoundedOrderHomClass` 📖	mathematical	—	`BoundedOrderHomClass` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`InfHomClass.toOrderHomClass` `InfTopHomClass.toInfHomClass` `toInfTopHomClass` `map_top` `map_bot`
`toInfTopHomClass` 📖	mathematical	—	`InfTopHomClass` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `BoundedOrder.toOrderTop`	—	`LatticeHomClass.map_inf` `toLatticeHomClass` `map_top`
`toLatticeHomClass` 📖	mathematical	—	`LatticeHomClass`	—	—
`toSupBotHomClass` 📖	mathematical	—	`SupBotHomClass` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderBot`	—	`LatticeHomClass.toSupHomClass` `toLatticeHomClass` `map_bot`

Codisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`Codisjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	`DFunLike.coe`	—	`codisjoint_iff` `SupHomClass.map_sup` `eq_top` `TopHomClass.map_top`

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	`DFunLike.coe`	—	`disjoint_iff` `InfHomClass.map_inf` `eq_bot` `BotHomClass.map_bot`

InfTopHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	12 math math: `comp_id`, `SupBotHom.dual_comp`, `SupBotHom.symm_dual_comp`, `symm_dual_comp`, `cancel_right`, `id_comp`, `comp_assoc`, `cancel_left`, `dual_comp`, `comp_apply`, `coe_comp`, `InfHom.withTop_comp`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`dual` 📖	CompOp	7 math math: `symm_dual_id`, `symm_dual_comp`, `dual_id`, `dual_comp`, `dual_apply_toFun`, `SemilatInfCat.dual_map`, `dual_symm_apply_toFun`
`id` 📖	CompOp	10 math math: `comp_id`, `symm_dual_id`, `id_comp`, `dual_id`, `id_apply`, `coe_id`, `SupBotHom.dual_id`, `InfHom.withTop_id`, `SupBotHom.symm_dual_id`, `id_toFun`
`instFunLike` 📖	CompOp	34 math math: `inf_apply`, `coe_toInfHom`, `SemilatInfCat_dual_comp_forget_to_partOrd`, `id_apply`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `coe_id`, `SemilatInfCat.coe_forget_to_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `InfHom.withTop_toFun`, `FrameHom.coe_toInfTopHom`, `InfHom.withTop'_toFun`, `bddLat_dual_comp_forget_to_semilatInfCat`, `subtypeVal_coe`, `comp_apply`, `SemilatInfCat.Iso.mk_inv_toFun`, `coe_comp`, `dual_apply_toFun`, `coe_mk`, `coe_top`, `FrameHom.coe_mk`, `dual_symm_apply_toFun`, `ext_iff`, `SemilatInfCat.Iso.mk_hom_toFun`, `Ideal.radicalInfTopHom_apply`, `BoundedLatticeHom.coe_toInfTopHom`, `BddLat.coe_forget_to_semilatInf`, `instInfTopHomClass`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `toFun_eq_coe`, `coe_inf`, `top_apply`, `subtypeVal_apply`, `coe_toTopHom`, `id_toFun`
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	2 math math: `inf_apply`, `coe_inf`
`instOrderTop` 📖	CompOp	2 math math: `coe_top`, `top_apply`
`instPartialOrder` 📖	CompOp	2 math math: `coe_top`, `top_apply`
`instSemilatticeInf` 📖	CompOp	—
`subtypeVal` 📖	CompOp	2 math math: `subtypeVal_coe`, `subtypeVal_apply`
`toInfHom` 📖	CompOp	5 math math: `coe_toInfHom`, `FrameHom.map_sSup'`, `map_top'`, `FrameHom.toFun_eq_coe`, `toFun_eq_coe`
`toTopHom` 📖	CompOp	1 math math: `coe_toTopHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `InfTopHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `InfTopHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `InfTopHom` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `instFunLike` `id`	—	—
`coe_inf` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `SemilatticeInf.toMin` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `instFunLike` `instMin` `Pi.instMinForall_mathlib`	—	—
`coe_mk` 📖	mathematical	`InfHom.toFun` `Top.top`	`DFunLike.coe` `InfTopHom` `instFunLike` `InfHom` `InfHom.instFunLike`	—	—
`coe_toInfHom` 📖	mathematical	—	`DFunLike.coe` `InfHom` `InfHom.instFunLike` `toInfHom` `InfTopHom` `instFunLike`	—	—
`coe_toTopHom` 📖	mathematical	—	`DFunLike.coe` `TopHom` `TopHom.instFunLike` `toTopHom` `InfTopHom` `instFunLike`	—	—
`coe_top` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `SemilatticeInf.toMin` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `instFunLike` `Top.top` `instPartialOrder` `instOrderTop` `Pi.instTopForall`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`copy_eq` 📖	mathematical	`DFunLike.coe` `InfTopHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`dual_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `OrderDual` `OrderDual.instSup` `OrderDual.instBot` `SupBotHom.instFunLike` `Equiv` `InfTopHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `instFunLike`	—	—
`dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `InfTopHom` `SupBotHom` `OrderDual` `OrderDual.instSup` `OrderDual.instBot` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `comp` `SupBotHom.comp`	—	—
`dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `InfTopHom` `SupBotHom` `OrderDual` `OrderDual.instSup` `OrderDual.instBot` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `id` `SupBotHom.id`	—	—
`dual_symm_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `instFunLike` `Equiv` `SupBotHom` `OrderDual` `OrderDual.instSup` `OrderDual.instBot` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `SupBotHom.instFunLike`	—	—
`ext` 📖	—	`DFunLike.coe` `InfTopHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`id_toFun` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `instFunLike` `id`	—	—
`inf_apply` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `SemilatticeInf.toMin` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `instFunLike` `instMin`	—	—
`instInfTopHomClass` 📖	mathematical	—	`InfTopHomClass` `InfTopHom` `instFunLike`	—	`InfHom.map_inf'` `map_top'`
`map_top'` 📖	mathematical	—	`InfHom.toFun` `toInfHom` `Top.top`	—	—
`subtypeVal_apply` 📖	mathematical	`Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	`DFunLike.coe` `InfTopHom` `Subtype.semilatticeInf` `Subtype.orderTop` `instFunLike` `subtypeVal`	—	—
`subtypeVal_coe` 📖	mathematical	`Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	`DFunLike.coe` `InfTopHom` `Subtype.semilatticeInf` `Subtype.orderTop` `instFunLike` `subtypeVal`	—	—
`symm_dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SupBotHom` `OrderDual` `OrderDual.instSup` `OrderDual.instBot` `InfTopHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `SupBotHom.comp` `comp`	—	—
`symm_dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SupBotHom` `OrderDual` `OrderDual.instSup` `OrderDual.instBot` `InfTopHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `SupBotHom.id` `id`	—	—
`toFun_eq_coe` 📖	mathematical	—	`InfHom.toFun` `toInfHom` `DFunLike.coe` `InfTopHom` `instFunLike`	—	—
`top_apply` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `SemilatticeInf.toMin` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `instFunLike` `Top.top` `instPartialOrder` `instOrderTop`	—	—

InfTopHomClass

Theorems

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

IsCompl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`IsCompl` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	`DFunLike.coe`	—	`Disjoint.map` `SupBotHomClass.toBotHomClass` `BoundedLatticeHomClass.toSupBotHomClass` `InfTopHomClass.toInfHomClass` `BoundedLatticeHomClass.toInfTopHomClass` `disjoint` `Codisjoint.map` `InfTopHomClass.toTopHomClass` `SupBotHomClass.toSupHomClass` `codisjoint`

OrderIsoClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBoundedLatticeHomClass` 📖	mathematical	—	`BoundedLatticeHomClass` `EquivLike.toFunLike`	—	`toLatticeHomClass` `toBoundedOrderHomClass` `BoundedOrderHomClass.map_top` `BoundedOrderHomClass.map_bot`
`toInfTopHomClass` 📖	mathematical	—	`InfTopHomClass` `SemilatticeInf.toMin` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `EquivLike.toFunLike`	—	`toInfHomClass` `toTopHomClass` `TopHomClass.map_top`
`toSupBotHomClass` 📖	mathematical	—	`SupBotHomClass` `SemilatticeSup.toMax` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `EquivLike.toFunLike`	—	`toSupHomClass` `toBotHomClass` `BotHomClass.map_bot`

SupBotHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	12 math math: `comp_id`, `dual_comp`, `symm_dual_comp`, `InfTopHom.symm_dual_comp`, `cancel_left`, `comp_assoc`, `cancel_right`, `comp_apply`, `InfTopHom.dual_comp`, `coe_comp`, `SupHom.withBot_comp`, `id_comp`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`dual` 📖	CompOp	5 math math: `dual_comp`, `symm_dual_comp`, `SemilatSupCat.dual_map`, `dual_id`, `symm_dual_id`
`id` 📖	CompOp	10 math math: `comp_id`, `InfTopHom.symm_dual_id`, `SupHom.withBot_id`, `InfTopHom.dual_id`, `id_toFun`, `dual_id`, `id_comp`, `symm_dual_id`, `id_apply`, `coe_id`
`instFunLike` 📖	CompOp	32 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `SemilatSupCat.Iso.mk_inv_toFun`, `coe_toBotHom`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `subtypeVal_coe`, `instSupBotHomClass`, `bot_apply`, `BoundedLatticeHom.coe_toSupBotHom`, `comp_apply`, `LatticeHom.withBot_toFun`, `id_toFun`, `subtypeVal_apply`, `coe_sup`, `bddLat_dual_comp_forget_to_semilatSupCat`, `coe_comp`, `coe_toSupHom`, `bddLat_dual_comp_forget_to_semilatInfCat`, `sup_apply`, `SupHom.withBot_toFun`, `SupHom.withBot'_toFun`, `InfTopHom.dual_apply_toFun`, `SemilatSupCat.Iso.mk_hom_toFun`, `toFun_eq_coe`, `ext_iff`, `InfTopHom.dual_symm_apply_toFun`, `BddLat.coe_forget_to_semilatSup`, `coe_bot`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `SemilatSupCat.coe_forget_to_partOrd`, `id_apply`, `coe_mk`, `coe_id`
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	2 math math: `coe_sup`, `sup_apply`
`instOrderBot` 📖	CompOp	2 math math: `bot_apply`, `coe_bot`
`instPartialOrder` 📖	CompOp	2 math math: `bot_apply`, `coe_bot`
`instSemilatticeSup` 📖	CompOp	—
`subtypeVal` 📖	CompOp	2 math math: `subtypeVal_coe`, `subtypeVal_apply`
`toBotHom` 📖	CompOp	1 math math: `coe_toBotHom`
`toSupHom` 📖	CompOp	3 math math: `coe_toSupHom`, `map_bot'`, `toFun_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_apply` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `SemilatticeSup.toMax` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLike` `Bot.bot` `instPartialOrder` `instOrderBot`	—	—
`cancel_left` 📖	mathematical	`DFunLike.coe` `SupBotHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `SupBotHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_bot` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `SemilatticeSup.toMax` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLike` `Bot.bot` `instPartialOrder` `instOrderBot` `Pi.instBotForall`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `SupBotHom` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `instFunLike` `id`	—	—
`coe_mk` 📖	mathematical	`SupHom.toFun` `Bot.bot`	`DFunLike.coe` `SupBotHom` `instFunLike` `SupHom` `SupHom.instFunLike`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `SemilatticeSup.toMax` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLike` `instMax` `Pi.instMaxForall_mathlib`	—	—
`coe_toBotHom` 📖	mathematical	—	`DFunLike.coe` `BotHom` `BotHom.instFunLike` `toBotHom` `SupBotHom` `instFunLike`	—	—
`coe_toSupHom` 📖	mathematical	—	`DFunLike.coe` `SupHom` `SupHom.instFunLike` `toSupHom` `SupBotHom` `instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`copy_eq` 📖	mathematical	`DFunLike.coe` `SupBotHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SupBotHom` `InfTopHom` `OrderDual` `OrderDual.instInf` `OrderDual.instTop` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `comp` `InfTopHom.comp`	—	—
`dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SupBotHom` `InfTopHom` `OrderDual` `OrderDual.instInf` `OrderDual.instTop` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `id` `InfTopHom.id`	—	—
`ext` 📖	—	`DFunLike.coe` `SupBotHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`id_toFun` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `instFunLike` `id`	—	—
`instSupBotHomClass` 📖	mathematical	—	`SupBotHomClass` `SupBotHom` `instFunLike`	—	`SupHom.map_sup'` `map_bot'`
`map_bot'` 📖	mathematical	—	`SupHom.toFun` `toSupHom` `Bot.bot`	—	—
`subtypeVal_apply` 📖	mathematical	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	`DFunLike.coe` `SupBotHom` `Subtype.semilatticeSup` `Subtype.orderBot` `instFunLike` `subtypeVal`	—	—
`subtypeVal_coe` 📖	mathematical	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	`DFunLike.coe` `SupBotHom` `Subtype.semilatticeSup` `Subtype.orderBot` `instFunLike` `subtypeVal`	—	—
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `SemilatticeSup.toMax` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLike` `instMax`	—	—
`symm_dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `InfTopHom` `OrderDual` `OrderDual.instInf` `OrderDual.instTop` `SupBotHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `InfTopHom.comp` `comp`	—	—
`symm_dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `InfTopHom` `OrderDual` `OrderDual.instInf` `OrderDual.instTop` `SupBotHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `InfTopHom.id` `id`	—	—
`toFun_eq_coe` 📖	mathematical	—	`SupHom.toFun` `toSupHom` `DFunLike.coe` `SupBotHom` `instFunLike`	—	—

SupBotHomClass

Theorems

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

(root)

Definitions

Name	Category	Theorems
`BoundedLatticeHom` 📖	CompData	114 math math: `BoolAlg.coe_id`, `BoundedLatticeHom.coe_toLatticeHom`, `LatticeHom.withTopWithBot_apply`, `CompleteLatticeHom.coe_toBoundedLatticeHom`, `BoolRing.hasForgetToBoolAlg_forget₂_obj_coe`, `HeytAlg.hasForgetToLat_forget₂_map`, `BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier`, `BoundedLatticeHom.coe_comp_sup_hom'`, `LatticeHom.coe_withTopWithBot`, `BoundedLatticeHom.dual_id`, `BoolAlg.ext_iff`, `FinBddDistLat.ofHom_apply`, `BoundedLatticeHom.symm_dual_comp`, `BoolAlg.hasForgetToBoolRing_forget₂_map`, `BddDistLat.coe_id`, `HeytAlg.hasForgetToLat_forget₂_obj_str`, `FinBddDistLat.hom_inv_apply`, `HeytAlg.hasForgetToLat_forget₂_obj_carrier`, `bddLat_dual_comp_forget_to_lat`, `boolRingCatEquivBoolAlg_functor`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `FinBddDistLat.ext_iff`, `BooleanSubalgebra.mem_comap`, `LatticeHom.withTopWithBot'_toFun`, `FinBddDistLat.coe_id`, `BooleanSubalgebra.coe_map`, `FinBddDistLat.inv_hom_apply`, `finBddDistLat_dual_comp_forget_to_bddDistLat`, `BoundedLatticeHom.coe_comp_lattice_hom'`, `BoolAlg.hasForgetToHeytAlg_forget₂_map`, `FinBddDistLat.forget_map`, `BddDistLat.coe_comp`, `FinBoolAlg.forgetToFinPartOrdFaithful`, `BoundedLatticeHom.coe_comp_sup_hom`, `BooleanSubalgebra.subtype_injective`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `BoundedLatticeHom.coe_toSupBotHom`, `BooleanSubalgebra.apply_coe_mem_map`, `BddDistLat.forget_map`, `BoundedLatticeHom.dual_symm_apply_toFun`, `BooleanSubalgebra.coe_inclusion`, `BoundedLatticeHom.ext_iff`, `FinBddDistLat.comp_apply`, `BddDistLat.dual_map`, `bddLat_dual_comp_forget_to_semilatSupCat`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier`, `BoundedLatticeHom.symm_dual_id`, `BooleanSubalgebra.mem_map_of_mem`, `BoundedLatticeHom.subtypeVal_coe`, `BddDistLat.inv_hom_apply`, `LatticeHom.withTopWithBot_toFun`, `BooleanSubalgebra.subtype_apply`, `bddLat_dual_comp_forget_to_semilatInfCat`, `BooleanSubalgebra.inclusion_injective`, `BoolAlg.dual_map`, `BoundedLatticeHom.toFun_eq_coe`, `BddDistLat.ofHom_apply`, `boolRingCatEquivBoolAlg_inverse`, `BoolAlg.coe_comp`, `BoundedLatticeHom.asBoolRing_apply`, `HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder`, `BoolRing.hasForgetToBoolAlg_forget₂_map`, `BoolAlg.hom_inv_apply`, `BoundedLatticeHom.dual_apply_toFun`, `BddDistLat.id_apply`, `bddLat_dual_comp_forget_to_bddOrd`, `BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype`, `BooleanSubalgebra.mem_map`, `BddLat.coe_forget_to_lat`, `BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat`, `BoolAlg.comp_apply`, `finBoolAlg_dual_comp_forget_to_finBddDistLat`, `completeLat_dual_comp_forget_to_bddLat`, `BoundedLatticeHom.coe_toBoundedOrderHom`, `BddLat.coe_forget_to_semilatSup`, `FinBddDistLat.coe_comp`, `BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe`, `BooleanSubalgebra.coe_subtype`, `BoundedLatticeHom.dual_comp`, `BoundedLatticeHom.instBoundedLatticeHomClass`, `BddDistLat.ext_iff`, `BoundedLatticeHom.coe_toInfTopHom`, `BoundedLatticeHom.coe_comp`, `BooleanSubalgebra.coe_comap`, `BddLat.coe_forget_to_bddOrd`, `BoolAlg.inv_hom_apply`, `BddLat.coe_forget_to_semilatInf`, `boolAlg_dual_comp_forget_to_bddDistLat`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_map`, `FinBoolAlg.forgetToBoolAlg_full`, `FinBddDistLat.id_apply`, `BddDistLat.comp_apply`, `BddLat.ext_iff`, `bddDistLat_dual_comp_forget_to_distLat`, `BooleanSubalgebra.inclusion_apply`, `BoundedLatticeHom.coe_comp_inf_hom'`, `BoundedLatticeHom.comp_apply`, `BoundedLatticeHom.coe_mk`, `BoundedLatticeHom.coe_comp_inf_hom`, `BoundedLatticeHom.coe_id`, `FinBddDistLat.dual_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str`, `FinBoolAlg.dual_map`, `BoolAlg.id_apply`, `BddLat.dual_map`, `BddDistLat.hom_inv_apply`, `BoundedLatticeHom.subtypeVal_apply`, `FinBoolAlg.forgetToBoolAlgFaithful`, `BoundedLatticeHom.coe_comp_lattice_hom`, `BoundedLatticeHom.id_apply`, `BoolAlg.ofHom_apply`, `BoolAlg.forget_map`, `RingHom.asBoolAlg_toFun`
`BoundedLatticeHomClass` 📖	CompData	6 math math: `FrameHomClass.toBoundedLatticeHomClass`, `CompleteLatticeHomClass.toBoundedLatticeHomClass`, `HeytingHomClass.toBoundedLatticeHomClass`, `OrderIsoClass.toBoundedLatticeHomClass`, `CoheytingHomClass.toBoundedLatticeHomClass`, `BoundedLatticeHom.instBoundedLatticeHomClass`
`InfTopHom` 📖	CompData	44 math math: `SupBotHom.dual_comp`, `InfTopHom.symm_dual_id`, `InfTopHom.inf_apply`, `SupBotHom.symm_dual_comp`, `InfTopHom.coe_toInfHom`, `InfTopHom.symm_dual_comp`, `SemilatInfCat_dual_comp_forget_to_partOrd`, `InfTopHom.dual_id`, `InfTopHom.id_apply`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `InfTopHom.coe_id`, `SemilatSupCat.dual_map`, `SemilatInfCat.coe_forget_to_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `InfHom.withTop_toFun`, `InfTopHom.dual_comp`, `SupBotHom.dual_id`, `FrameHom.coe_toInfTopHom`, `InfHom.withTop'_toFun`, `bddLat_dual_comp_forget_to_semilatInfCat`, `InfTopHom.subtypeVal_coe`, `InfTopHom.comp_apply`, `SemilatInfCat.Iso.mk_inv_toFun`, `InfTopHom.coe_comp`, `InfTopHom.dual_apply_toFun`, `InfTopHom.coe_mk`, `SupBotHom.symm_dual_id`, `InfTopHom.coe_top`, `SemilatInfCat.dual_map`, `FrameHom.coe_mk`, `InfTopHom.dual_symm_apply_toFun`, `InfTopHom.ext_iff`, `SemilatInfCat.Iso.mk_hom_toFun`, `Ideal.radicalInfTopHom_apply`, `BoundedLatticeHom.coe_toInfTopHom`, `BddLat.coe_forget_to_semilatInf`, `InfTopHom.instInfTopHomClass`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `InfTopHom.toFun_eq_coe`, `InfTopHom.coe_inf`, `InfTopHom.top_apply`, `InfTopHom.subtypeVal_apply`, `InfTopHom.coe_toTopHom`, `InfTopHom.id_toFun`
`InfTopHomClass` 📖	CompData	5 math math: `FrameHomClass.toInfTopHomClass`, `sInfHomClass.toInfTopHomClass`, `InfTopHom.instInfTopHomClass`, `BoundedLatticeHomClass.toInfTopHomClass`, `OrderIsoClass.toInfTopHomClass`
`SupBotHom` 📖	CompData	42 math math: `SupBotHom.dual_comp`, `InfTopHom.symm_dual_id`, `SupBotHom.symm_dual_comp`, `InfTopHom.symm_dual_comp`, `SemilatInfCat_dual_comp_forget_to_partOrd`, `SemilatSupCat.Iso.mk_inv_toFun`, `SupBotHom.coe_toBotHom`, `InfTopHom.dual_id`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `SupBotHom.subtypeVal_coe`, `SupBotHom.instSupBotHomClass`, `SupBotHom.bot_apply`, `BoundedLatticeHom.coe_toSupBotHom`, `SupBotHom.comp_apply`, `LatticeHom.withBot_toFun`, `SemilatSupCat.dual_map`, `SupBotHom.id_toFun`, `SupBotHom.subtypeVal_apply`, `SupBotHom.coe_sup`, `bddLat_dual_comp_forget_to_semilatSupCat`, `InfTopHom.dual_comp`, `SupBotHom.dual_id`, `SupBotHom.coe_comp`, `SupBotHom.coe_toSupHom`, `bddLat_dual_comp_forget_to_semilatInfCat`, `SupBotHom.sup_apply`, `SupHom.withBot_toFun`, `SupHom.withBot'_toFun`, `InfTopHom.dual_apply_toFun`, `SemilatSupCat.Iso.mk_hom_toFun`, `SupBotHom.symm_dual_id`, `SupBotHom.toFun_eq_coe`, `SemilatInfCat.dual_map`, `SupBotHom.ext_iff`, `InfTopHom.dual_symm_apply_toFun`, `BddLat.coe_forget_to_semilatSup`, `SupBotHom.coe_bot`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `SemilatSupCat.coe_forget_to_partOrd`, `SupBotHom.id_apply`, `SupBotHom.coe_mk`, `SupBotHom.coe_id`
`SupBotHomClass` 📖	CompData	4 math math: `SupBotHom.instSupBotHomClass`, `OrderIsoClass.toSupBotHomClass`, `BoundedLatticeHomClass.toSupBotHomClass`, `sSupHomClass.toSupBotHomClass`
`instCoeTCBoundedLatticeHomOfBoundedLatticeHomClass` 📖	CompOp	—
`instCoeTCInfTopHomOfInfTopHomClass` 📖	CompOp	—
`instCoeTCSupBotHomOfSupBotHomClass` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_compl'` 📖	mathematical	—	`DFunLike.coe` `Compl.compl` `BooleanAlgebra.toCompl`	—	`IsCompl.compl_eq` `IsCompl.map` `isCompl_compl`
`map_sdiff'` 📖	mathematical	—	`DFunLike.coe` `BooleanAlgebra.toSDiff`	—	`sdiff_eq` `InfHomClass.map_inf` `InfTopHomClass.toInfHomClass` `BoundedLatticeHomClass.toInfTopHomClass` `map_compl'`
`map_symmDiff'` 📖	mathematical	—	`DFunLike.coe` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toSDiff`	—	`symmDiff.eq_1` `SupHomClass.map_sup` `SupBotHomClass.toSupHomClass` `BoundedLatticeHomClass.toSupBotHomClass` `map_sdiff'`

---

← Back to Index