Lattice

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

Statistics

Metric	Count
Definitions `InfHom`, `comp`, `const`, `copy`, `dual`, `id`, `instBot`, `instBoundedOrder`, `instFunLike`, `instInhabited`, `instMin`, `instOrderBot`, `instOrderTop`, `instPartialOrder`, `instSemilatticeInf`, `instTop`, `subtypeVal`, `toFun`, `InfHomClass`, `LatticeHom`, `comp`, `copy`, `dual`, `fst`, `id`, `instFunLike`, `instInhabited`, `snd`, `subtypeVal`, `toInfHom`, `toSupHom`, `LatticeHomClass`, `toLatticeHom`, `evalLatticeHom`, `SupHom`, `comp`, `const`, `copy`, `dual`, `id`, `instBot`, `instBoundedOrder`, `instFunLike`, `instInhabited`, `instMax`, `instOrderBot`, `instOrderTop`, `instPartialOrder`, `instSemilatticeSup`, `instTop`, `subtypeVal`, `toFun`, `SupHomClass`, `instCoeTCInfHomOfInfHomClass`, `instCoeTCLatticeHomOfLatticeHomClass`, `instCoeTCSupHomOfSupHomClass`, `orderEmbeddingOfInjective`	57
Theorems `bot_apply`, `cancel_left`, `cancel_right`, `coe_bot`, `coe_comp`, `coe_const`, `coe_copy`, `coe_id`, `coe_inf`, `coe_mk`, `coe_top`, `comp_apply`, `comp_assoc`, `comp_id`, `const_apply`, `copy_eq`, `dual_apply_toFun`, `dual_comp`, `dual_id`, `dual_symm_apply_toFun`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `inf_apply`, `instInfHomClass`, `map_inf'`, `mk_le_mk`, `subtypeVal_apply`, `subtypeVal_coe`, `symm_dual_comp`, `symm_dual_id`, `toFun_eq_coe`, `top_apply`, `map_inf`, `toOrderHomClass`, `cancel_left`, `cancel_right`, `coe_comp`, `coe_comp_inf_hom`, `coe_comp_inf_hom'`, `coe_comp_sup_hom`, `coe_comp_sup_hom'`, `coe_copy`, `coe_fst`, `coe_id`, `coe_mk`, `coe_snd`, `coe_toInfHom`, `coe_toSupHom`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `dual_apply_toFun`, `dual_comp`, `dual_id`, `dual_symm_apply_toFun`, `ext`, `ext_iff`, `fst_apply`, `id_apply`, `id_comp`, `instLatticeHomClass`, `map_inf'`, `snd_apply`, `subtypeVal_apply`, `subtypeVal_coe`, `symm_dual_comp`, `symm_dual_id`, `toFun_eq_coe`, `map_inf`, `toInfHomClass`, `toSupHomClass`, `coe_to_lattice_hom`, `toLatticeHomClass`, `to_lattice_hom_apply`, `toInfHomClass`, `toLatticeHomClass`, `toSupHomClass`, `coe_evalLatticeHom`, `evalLatticeHom_apply`, `bot_apply`, `cancel_left`, `cancel_right`, `coe_bot`, `coe_comp`, `coe_const`, `coe_copy`, `coe_id`, `coe_mk`, `coe_sup`, `coe_top`, `comp_apply`, `comp_assoc`, `comp_id`, `const_apply`, `copy_eq`, `dual_apply_toFun`, `dual_comp`, `dual_id`, `dual_symm_apply_toFun`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `instSupHomClass`, `map_sup'`, `mk_le_mk`, `subtypeVal_apply`, `subtypeVal_coe`, `sup_apply`, `symm_dual_comp`, `symm_dual_id`, `toFun_eq_coe`, `top_apply`, `map_sup`, `toOrderHomClass`, `orderEmbeddingOfInjective_apply`	119
Total	176

InfHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	17 math math: `comp_apply`, `symm_dual_comp`, `id_comp`, `comp_id`, `SupHom.symm_dual_comp`, `coe_comp`, `SupHom.dual_comp`, `dual_comp`, `comp_assoc`, `LatticeHom.coe_comp_inf_hom`, `cancel_left`, `withBot_comp`, `LatticeHom.coe_comp_inf_hom'`, `BoundedLatticeHom.coe_comp_inf_hom'`, `BoundedLatticeHom.coe_comp_inf_hom`, `cancel_right`, `withTop_comp`
`const` 📖	CompOp	2 math math: `const_apply`, `coe_const`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`dual` 📖	CompOp	6 math math: `symm_dual_comp`, `dual_apply_toFun`, `dual_id`, `dual_symm_apply_toFun`, `dual_comp`, `symm_dual_id`
`id` 📖	CompOp	10 math math: `SupHom.dual_id`, `id_comp`, `comp_id`, `dual_id`, `id_apply`, `SupHom.symm_dual_id`, `withTop_id`, `symm_dual_id`, `coe_id`, `withBot_id`
`instBot` 📖	CompOp	2 math math: `bot_apply`, `coe_bot`
`instBoundedOrder` 📖	CompOp	—
`instFunLike` 📖	CompOp	33 math math: `top_apply`, `Nucleus.coe_toInfHom`, `comp_apply`, `bot_apply`, `InfTopHom.coe_toInfHom`, `Nucleus.coe_mk`, `coe_comp`, `dual_apply_toFun`, `instInfHomClass`, `id_apply`, `dual_symm_apply_toFun`, `const_apply`, `withBot_toFun`, `withTop_toFun`, `coe_mk`, `withTop'_toFun`, `LowerSet.iicInfHom_apply`, `inf_apply`, `ext_iff`, `withBot'_toFun`, `coe_const`, `InfTopHom.coe_mk`, `LatticeHom.coe_toInfHom`, `LowerSet.coe_iicInfHom`, `coe_id`, `subtypeVal_coe`, `coe_bot`, `coe_inf`, `SupHom.dual_symm_apply_toFun`, `toFun_eq_coe`, `coe_top`, `SupHom.dual_apply_toFun`, `subtypeVal_apply`
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	2 math math: `inf_apply`, `coe_inf`
`instOrderBot` 📖	CompOp	—
`instOrderTop` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	2 math math: `Nucleus.mk_le_mk`, `mk_le_mk`
`instSemilatticeInf` 📖	CompOp	—
`instTop` 📖	CompOp	2 math math: `top_apply`, `coe_top`
`subtypeVal` 📖	CompOp	2 math math: `subtypeVal_coe`, `subtypeVal_apply`
`toFun` 📖	CompOp	9 math math: `Nucleus.idempotent'`, `FrameHom.map_sSup'`, `InfTopHom.map_top'`, `Nucleus.toFun_eq_coe`, `FrameHom.toFun_eq_coe`, `InfTopHom.toFun_eq_coe`, `toFun_eq_coe`, `map_inf'`, `Nucleus.le_apply'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_apply` 📖	mathematical	—	`DFunLike.coe` `InfHom` `SemilatticeInf.toMin` `instFunLike` `Bot.bot` `instBot`	—	—
`cancel_left` 📖	mathematical	`DFunLike.coe` `InfHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `InfHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_bot` 📖	mathematical	—	`DFunLike.coe` `InfHom` `SemilatticeInf.toMin` `instFunLike` `Bot.bot` `instBot` `Pi.instBotForall`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `InfHom` `instFunLike` `comp`	—	—
`coe_const` 📖	mathematical	—	`DFunLike.coe` `InfHom` `SemilatticeInf.toMin` `instFunLike` `const`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `InfHom` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `InfHom` `instFunLike` `id`	—	—
`coe_inf` 📖	mathematical	—	`DFunLike.coe` `InfHom` `SemilatticeInf.toMin` `instFunLike` `instMin` `Pi.instMinForall_mathlib`	—	—
`coe_mk` 📖	mathematical	—	`DFunLike.coe` `InfHom` `instFunLike`	—	—
`coe_top` 📖	mathematical	—	`DFunLike.coe` `InfHom` `SemilatticeInf.toMin` `instFunLike` `Top.top` `instTop` `Pi.instTopForall`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `InfHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`const_apply` 📖	mathematical	—	`DFunLike.coe` `InfHom` `SemilatticeInf.toMin` `instFunLike` `const`	—	—
`copy_eq` 📖	mathematical	`DFunLike.coe` `InfHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`dual_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `SupHom` `OrderDual` `OrderDual.instSup` `SupHom.instFunLike` `Equiv` `InfHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `instFunLike`	—	—
`dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `InfHom` `SupHom` `OrderDual` `OrderDual.instSup` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `comp` `SupHom.comp`	—	—
`dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `InfHom` `SupHom` `OrderDual` `OrderDual.instSup` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `id` `SupHom.id`	—	—
`dual_symm_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `InfHom` `instFunLike` `Equiv` `SupHom` `OrderDual` `OrderDual.instSup` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `SupHom.instFunLike`	—	—
`ext` 📖	—	`DFunLike.coe` `InfHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `InfHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `InfHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`inf_apply` 📖	mathematical	—	`DFunLike.coe` `InfHom` `SemilatticeInf.toMin` `instFunLike` `instMin`	—	—
`instInfHomClass` 📖	mathematical	—	`InfHomClass` `InfHom` `instFunLike`	—	`map_inf'`
`map_inf'` 📖	mathematical	—	`toFun`	—	—
`mk_le_mk` 📖	mathematical	`SemilatticeInf.toMin`	`InfHom` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Pi.hasLe` `SemilatticeInf.toPartialOrder`	—	—
`subtypeVal_apply` 📖	mathematical	`SemilatticeInf.toMin`	`DFunLike.coe` `InfHom` `Subtype.semilatticeInf` `instFunLike` `subtypeVal`	—	—
`subtypeVal_coe` 📖	mathematical	`SemilatticeInf.toMin`	`DFunLike.coe` `InfHom` `Subtype.semilatticeInf` `instFunLike` `subtypeVal`	—	—
`symm_dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SupHom` `OrderDual` `OrderDual.instSup` `InfHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `SupHom.comp` `comp`	—	—
`symm_dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SupHom` `OrderDual` `OrderDual.instSup` `InfHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `SupHom.id` `id`	—	—
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `InfHom` `instFunLike`	—	—
`top_apply` 📖	mathematical	—	`DFunLike.coe` `InfHom` `SemilatticeInf.toMin` `instFunLike` `Top.top` `instTop`	—	—

InfHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_inf` 📖	mathematical	—	`DFunLike.coe`	—	—
`toOrderHomClass` 📖	mathematical	—	`OrderHomClass` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`inf_eq_left` `map_inf`

LatticeHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	26 math math: `BddLat.hom_comp`, `comp_apply`, `coe_comp`, `Sublattice.subtype_comp_inclusion`, `Lat.hom_comp`, `withTopWithBot_comp`, `BoundedLatticeHom.coe_comp_lattice_hom'`, `Sublattice.map_map`, `comp_id`, `cancel_left`, `id_comp`, `symm_dual_comp`, `withBot_comp`, `withTop_comp`, `coe_comp_inf_hom`, `coe_comp_sup_hom`, `dual_comp`, `coe_comp_inf_hom'`, `coe_comp_sup_hom'`, `Lat.ofHom_comp`, `DistLat.hom_comp`, `comp_assoc`, `BoundedLatticeHom.coe_comp_lattice_hom`, `cancel_right`, `DistLat.ofHom_comp`, `Sublattice.comap_comap`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`dual` 📖	CompOp	8 math math: `Lat.dual_map`, `DistLat.dual_map`, `dual_symm_apply_toFun`, `dual_apply_toFun`, `symm_dual_id`, `dual_id`, `symm_dual_comp`, `dual_comp`
`fst` 📖	CompOp	4 math math: `fst_apply`, `Sublattice.le_prod_iff`, `coe_fst`, `Sublattice.prod_top`
`id` 📖	CompOp	17 math math: `withTopWithBot_id`, `id_apply`, `Sublattice.comap_id`, `symm_dual_id`, `DistLat.hom_id`, `withBot_id`, `comp_id`, `id_comp`, `dual_id`, `Sublattice.inclusion_rfl`, `Lat.hom_id`, `DistLat.ofHom_id`, `withTop_id`, `BddLat.hom_id`, `Sublattice.map_id`, `coe_id`, `Lat.ofHom_id`
`instFunLike` 📖	CompOp	92 math math: `toFun_eq_coe`, `DistLat.hom_inv_apply`, `BoundedLatticeHom.coe_toLatticeHom`, `withTopWithBot_apply`, `Lat.ext_iff`, `fst_apply`, `comp_apply`, `Sublattice.coe_map`, `coe_withTopWithBot`, `coe_comp`, `Lat.coe_id`, `subtypeVal_coe`, `subtypeVal_apply`, `id_apply`, `dual_symm_apply_toFun`, `Lat.forget_map`, `Sublattice.inclusion_apply`, `BiheytingHom.toFun_eq_coe_aux`, `bddLat_dual_comp_forget_to_lat`, `exists_birkhoff_representation`, `withTopWithBot'_toFun`, `Lat.comp_apply`, `CoheytingHom.toFun_eq_coe_aux`, `Sublattice.subtype_apply`, `DistLat.ext_iff`, `dual_apply_toFun`, `withTop_apply`, `Pi.coe_evalLatticeHom`, `distLat_dual_comp_forget_to_Lat`, `Sublattice.apply_coe_mem_map`, `DistLat.forget_map`, `Sublattice.coe_comap`, `withTop_toFun`, `Sublattice.mem_map`, `withBot_toFun`, `withTop'_toFun`, `DistLat.id_apply`, `FrameHom.coe_toLatticeHom`, `OrderHomClass.to_lattice_hom_apply`, `Sublattice.subtype_injective`, `ext_iff`, `Sublattice.mem_subtype`, `coe_withTop`, `coe_mk`, `Lat.ofHom_apply`, `coe_toSupHom`, `DistLat.ofHom_apply`, `withTopWithBot_toFun`, `coe_snd`, `HeytingHom.toFun_eq_coe_aux`, `Booleanisation.liftLatticeHom_injective`, `BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `BddLat.coe_forget_to_lat`, `BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat`, `snd_apply`, `withBot'_toFun`, `coe_toInfHom`, `OrderHomClass.coe_to_lattice_hom`, `Sublattice.mem_map_of_mem`, `Lat_dual_comp_forget_to_partOrd`, `coe_comp_inf_hom`, `coe_comp_sup_hom`, `Sublattice.coe_inclusion`, `instLatticeHomClass`, `DistLat.coe_id`, `Lat.hom_inv_apply`, `BddLat.comp_apply`, `SimplexCategory.toCat_obj`, `birkhoffFinset_injective`, `Lat.id_apply`, `BddLat.id_apply`, `DistLat.coe_comp`, `coe_comp_inf_hom'`, `coe_comp_sup_hom'`, `Lat.inv_hom_apply`, `coe_withBot`, `bddDistLat_dual_comp_forget_to_distLat`, `DistLat.comp_apply`, `Function.locallyFinsuppWithin.restrictLatticeHom_apply`, `Sublattice.mem_comap`, `Sublattice.coe_subtype`, `BoundedLatticeHom.coe_mk`, `linOrd_dual_comp_forget_to_Lat`, `coe_id`, `coe_fst`, `SimplexCategory.toCat_map`, `DistLat.inv_hom_apply`, `Sublattice.inclusion_injective`, `CompleteSublattice.subtype_apply`, `Pi.evalLatticeHom_apply`, `withBot_apply`, `Lat.coe_comp`
`instInhabited` 📖	CompOp	—
`snd` 📖	CompOp	4 math math: `coe_snd`, `snd_apply`, `Sublattice.top_prod`, `Sublattice.le_prod_iff`
`subtypeVal` 📖	CompOp	2 math math: `subtypeVal_coe`, `subtypeVal_apply`
`toInfHom` 📖	CompOp	1 math math: `coe_toInfHom`
`toSupHom` 📖	CompOp	16 math math: `toFun_eq_coe`, `BiheytingHom.map_sdiff'`, `withBot_toFun`, `map_inf'`, `BoundedLatticeHom.map_top'`, `CoheytingHom.map_top'`, `BiheytingHom.toFun_eq_coe`, `coe_toSupHom`, `HeytingHom.map_himp'`, `CoheytingHom.map_sdiff'`, `BoundedLatticeHom.map_bot'`, `BoundedLatticeHom.toFun_eq_coe`, `BiheytingHom.map_himp'`, `CoheytingHom.toFun_eq_coe`, `HeytingHom.map_bot'`, `HeytingHom.toFun_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `LatticeHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `LatticeHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `instFunLike` `comp`	—	—
`coe_comp_inf_hom` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DFunLike.coe` `LatticeHom` `instFunLike` `comp` `InfHomClass.map_inf` `LatticeHomClass.toInfHomClass` `instLatticeHomClass` `InfHom.comp`	—	`InfHomClass.map_inf` `LatticeHomClass.toInfHomClass` `instLatticeHomClass`
`coe_comp_inf_hom'` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DFunLike.coe` `LatticeHom` `instFunLike` `InfHomClass.map_inf` `LatticeHomClass.toInfHomClass` `instLatticeHomClass` `comp` `InfHom.comp`	—	`InfHomClass.map_inf` `LatticeHomClass.toInfHomClass` `instLatticeHomClass`
`coe_comp_sup_hom` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DFunLike.coe` `LatticeHom` `instFunLike` `comp` `SupHomClass.map_sup` `LatticeHomClass.toSupHomClass` `instLatticeHomClass` `SupHom.comp`	—	`SupHomClass.map_sup` `LatticeHomClass.toSupHomClass` `instLatticeHomClass`
`coe_comp_sup_hom'` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DFunLike.coe` `LatticeHom` `instFunLike` `SupHomClass.map_sup` `LatticeHomClass.toSupHomClass` `instLatticeHomClass` `comp` `SupHom.comp`	—	`SupHomClass.map_sup` `LatticeHomClass.toSupHomClass` `instLatticeHomClass`
`coe_copy` 📖	mathematical	`DFunLike.coe` `LatticeHom` `instFunLike`	`copy`	—	—
`coe_fst` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `Prod.instLattice` `instFunLike` `fst`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `instFunLike` `id`	—	—
`coe_mk` 📖	mathematical	`SupHom.toFun` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	`DFunLike.coe` `LatticeHom` `instFunLike` `SupHom` `SupHom.instFunLike`	—	—
`coe_snd` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `Prod.instLattice` `instFunLike` `snd`	—	—
`coe_toInfHom` 📖	mathematical	—	`DFunLike.coe` `InfHom` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `InfHom.instFunLike` `toInfHom` `LatticeHom` `instFunLike`	—	—
`coe_toSupHom` 📖	mathematical	—	`DFunLike.coe` `SupHom` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SupHom.instFunLike` `toSupHom` `LatticeHom` `instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `LatticeHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`dual_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `OrderDual` `OrderDual.instLattice` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual`	—	—
`dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LatticeHom` `OrderDual` `OrderDual.instLattice` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `comp`	—	—
`dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LatticeHom` `OrderDual` `OrderDual.instLattice` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `id`	—	—
`dual_symm_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `instFunLike` `Equiv` `OrderDual` `OrderDual.instLattice` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual`	—	—
`ext` 📖	—	`DFunLike.coe` `LatticeHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `instFunLike`	—	`ext`
`fst_apply` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `Prod.instLattice` `instFunLike` `fst`	—	—
`id_apply` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instLatticeHomClass` 📖	mathematical	—	`LatticeHomClass` `LatticeHom` `instFunLike`	—	`SupHom.map_sup'` `map_inf'`
`map_inf'` 📖	mathematical	—	`SupHom.toFun` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `toSupHom` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	—
`snd_apply` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `Prod.instLattice` `instFunLike` `snd`	—	—
`subtypeVal_apply` 📖	mathematical	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	`DFunLike.coe` `LatticeHom` `Subtype.lattice` `instFunLike` `subtypeVal`	—	—
`subtypeVal_coe` 📖	mathematical	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	`DFunLike.coe` `LatticeHom` `Subtype.lattice` `instFunLike` `subtypeVal`	—	—
`symm_dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LatticeHom` `OrderDual` `OrderDual.instLattice` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `comp`	—	—
`symm_dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LatticeHom` `OrderDual` `OrderDual.instLattice` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `id`	—	—
`toFun_eq_coe` 📖	mathematical	—	`SupHom.toFun` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `toSupHom` `DFunLike.coe` `LatticeHom` `instFunLike`	—	—

LatticeHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_inf` 📖	mathematical	—	`DFunLike.coe` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	—
`toInfHomClass` 📖	mathematical	—	`InfHomClass` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`map_inf`
`toSupHomClass` 📖	mathematical	—	`SupHomClass` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	—

OrderHomClass

Definitions

Name	Category	Theorems
`toLatticeHom` 📖	CompOp	2 math math: `to_lattice_hom_apply`, `coe_to_lattice_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_to_lattice_hom` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LatticeHom.instFunLike` `toLatticeHom`	—	—
`toLatticeHomClass` 📖	mathematical	—	`LatticeHomClass` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_total` `sup_eq_right` `mono` `sup_eq_left` `inf_eq_left` `inf_eq_right`
`to_lattice_hom_apply` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LatticeHom.instFunLike` `toLatticeHom`	—	—

OrderIsoClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toInfHomClass` 📖	mathematical	—	`InfHomClass` `SemilatticeInf.toMin` `EquivLike.toFunLike`	—	`toOrderHomClass` `eq_of_forall_le_iff`
`toLatticeHomClass` 📖	mathematical	—	`LatticeHomClass` `EquivLike.toFunLike`	—	`toSupHomClass` `toInfHomClass` `InfHomClass.map_inf`
`toSupHomClass` 📖	mathematical	—	`SupHomClass` `SemilatticeSup.toMax` `EquivLike.toFunLike`	—	`toOrderHomClass` `eq_of_forall_ge_iff`

Pi

Definitions

Name	Category	Theorems
`evalLatticeHom` 📖	CompOp	3 math math: `coe_evalLatticeHom`, `Sublattice.le_pi`, `evalLatticeHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_evalLatticeHom` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `instLattice` `LatticeHom.instFunLike` `evalLatticeHom` `Function.eval`	—	—
`evalLatticeHom_apply` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `instLattice` `LatticeHom.instFunLike` `evalLatticeHom`	—	—

SupHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	18 math math: `InfHom.symm_dual_comp`, `BoundedLatticeHom.coe_comp_sup_hom'`, `symm_dual_comp`, `BoundedLatticeHom.coe_comp_lattice_hom'`, `id_comp`, `dual_comp`, `BoundedLatticeHom.coe_comp_sup_hom`, `InfHom.dual_comp`, `coe_comp`, `cancel_left`, `cancel_right`, `withBot_comp`, `LatticeHom.coe_comp_sup_hom`, `comp_id`, `comp_apply`, `LatticeHom.coe_comp_sup_hom'`, `comp_assoc`, `withTop_comp`
`const` 📖	CompOp	2 math math: `coe_const`, `const_apply`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`dual` 📖	CompOp	6 math math: `dual_id`, `symm_dual_comp`, `dual_comp`, `symm_dual_id`, `dual_symm_apply_toFun`, `dual_apply_toFun`
`id` 📖	CompOp	10 math math: `dual_id`, `withBot_id`, `id_apply`, `InfHom.dual_id`, `id_comp`, `symm_dual_id`, `comp_id`, `InfHom.symm_dual_id`, `withTop_id`, `coe_id`
`instBot` 📖	CompOp	2 math math: `bot_apply`, `coe_bot`
`instBoundedOrder` 📖	CompOp	—
`instFunLike` 📖	CompOp	32 math math: `subtypeVal_coe`, `bot_apply`, `instSupHomClass`, `coe_bot`, `id_apply`, `InfHom.dual_apply_toFun`, `InfHom.dual_symm_apply_toFun`, `coe_top`, `UpperSet.coe_iciSupHom`, `coe_comp`, `coe_const`, `withTop'_toFun`, `withTop_toFun`, `LatticeHom.coe_mk`, `subtypeVal_apply`, `LatticeHom.coe_toSupHom`, `SupBotHom.coe_toSupHom`, `const_apply`, `withBot_toFun`, `UpperSet.iciSupHom_apply`, `withBot'_toFun`, `sup_apply`, `coe_sup`, `comp_apply`, `coe_mk`, `toFun_eq_coe`, `ext_iff`, `dual_symm_apply_toFun`, `coe_id`, `top_apply`, `SupBotHom.coe_mk`, `dual_apply_toFun`
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	2 math math: `sup_apply`, `coe_sup`
`instOrderBot` 📖	CompOp	—
`instOrderTop` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	1 math math: `mk_le_mk`
`instSemilatticeSup` 📖	CompOp	—
`instTop` 📖	CompOp	2 math math: `coe_top`, `top_apply`
`subtypeVal` 📖	CompOp	2 math math: `subtypeVal_coe`, `subtypeVal_apply`
`toFun` 📖	CompOp	18 math math: `LatticeHom.toFun_eq_coe`, `BiheytingHom.map_sdiff'`, `LatticeHom.map_inf'`, `BoundedLatticeHom.map_top'`, `CoheytingHom.map_top'`, `BiheytingHom.toFun_eq_coe`, `HeytingHom.map_himp'`, `CoheytingHom.map_sdiff'`, `BoundedLatticeHom.map_bot'`, `BoundedLatticeHom.toFun_eq_coe`, `SupBotHom.map_bot'`, `SupBotHom.toFun_eq_coe`, `BiheytingHom.map_himp'`, `map_sup'`, `CoheytingHom.toFun_eq_coe`, `HeytingHom.map_bot'`, `toFun_eq_coe`, `HeytingHom.toFun_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_apply` 📖	mathematical	—	`DFunLike.coe` `SupHom` `SemilatticeSup.toMax` `instFunLike` `Bot.bot` `instBot`	—	—
`cancel_left` 📖	mathematical	`DFunLike.coe` `SupHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `SupHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_bot` 📖	mathematical	—	`DFunLike.coe` `SupHom` `SemilatticeSup.toMax` `instFunLike` `Bot.bot` `instBot` `Pi.instBotForall`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `SupHom` `instFunLike` `comp`	—	—
`coe_const` 📖	mathematical	—	`DFunLike.coe` `SupHom` `SemilatticeSup.toMax` `instFunLike` `const`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `SupHom` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `SupHom` `instFunLike` `id`	—	—
`coe_mk` 📖	mathematical	—	`DFunLike.coe` `SupHom` `instFunLike`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `SupHom` `SemilatticeSup.toMax` `instFunLike` `instMax` `Pi.instMaxForall_mathlib`	—	—
`coe_top` 📖	mathematical	—	`DFunLike.coe` `SupHom` `SemilatticeSup.toMax` `instFunLike` `Top.top` `instTop` `Pi.instTopForall`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `SupHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`const_apply` 📖	mathematical	—	`DFunLike.coe` `SupHom` `SemilatticeSup.toMax` `instFunLike` `const`	—	—
`copy_eq` 📖	mathematical	`DFunLike.coe` `SupHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`dual_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `InfHom` `OrderDual` `OrderDual.instInf` `InfHom.instFunLike` `Equiv` `SupHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `instFunLike`	—	—
`dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SupHom` `InfHom` `OrderDual` `OrderDual.instInf` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `comp` `InfHom.comp`	—	—
`dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SupHom` `InfHom` `OrderDual` `OrderDual.instInf` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `id` `InfHom.id`	—	—
`dual_symm_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `SupHom` `instFunLike` `Equiv` `InfHom` `OrderDual` `OrderDual.instInf` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `InfHom.instFunLike`	—	—
`ext` 📖	—	`DFunLike.coe` `SupHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `SupHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `SupHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`instSupHomClass` 📖	mathematical	—	`SupHomClass` `SupHom` `instFunLike`	—	`map_sup'`
`map_sup'` 📖	mathematical	—	`toFun`	—	—
`mk_le_mk` 📖	mathematical	`SemilatticeSup.toMax`	`SupHom` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Pi.hasLe` `SemilatticeSup.toPartialOrder`	—	—
`subtypeVal_apply` 📖	mathematical	`SemilatticeSup.toMax`	`DFunLike.coe` `SupHom` `Subtype.semilatticeSup` `instFunLike` `subtypeVal`	—	—
`subtypeVal_coe` 📖	mathematical	`SemilatticeSup.toMax`	`DFunLike.coe` `SupHom` `Subtype.semilatticeSup` `instFunLike` `subtypeVal`	—	—
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `SupHom` `SemilatticeSup.toMax` `instFunLike` `instMax`	—	—
`symm_dual_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `InfHom` `OrderDual` `OrderDual.instInf` `SupHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `InfHom.comp` `comp`	—	—
`symm_dual_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `InfHom` `OrderDual` `OrderDual.instInf` `SupHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `dual` `InfHom.id` `id`	—	—
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `SupHom` `instFunLike`	—	—
`top_apply` 📖	mathematical	—	`DFunLike.coe` `SupHom` `SemilatticeSup.toMax` `instFunLike` `Top.top` `instTop`	—	—

SupHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_sup` 📖	mathematical	—	`DFunLike.coe`	—	—
`toOrderHomClass` 📖	mathematical	—	`OrderHomClass` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`sup_eq_right` `map_sup`

(root)

Definitions

Name	Category	Theorems
`InfHom` 📖	CompData	43 math math: `InfHom.top_apply`, `Nucleus.coe_toInfHom`, `InfHom.comp_apply`, `InfHom.bot_apply`, `InfHom.symm_dual_comp`, `InfTopHom.coe_toInfHom`, `SupHom.dual_id`, `Nucleus.coe_mk`, `SupHom.symm_dual_comp`, `InfHom.coe_comp`, `InfHom.dual_apply_toFun`, `InfHom.dual_id`, `InfHom.instInfHomClass`, `InfHom.id_apply`, `InfHom.dual_symm_apply_toFun`, `InfHom.const_apply`, `SupHom.dual_comp`, `InfHom.dual_comp`, `InfHom.withBot_toFun`, `SupHom.symm_dual_id`, `InfHom.withTop_toFun`, `InfHom.coe_mk`, `InfHom.withTop'_toFun`, `LowerSet.iicInfHom_apply`, `InfHom.inf_apply`, `InfHom.ext_iff`, `InfHom.withBot'_toFun`, `InfHom.coe_const`, `InfTopHom.coe_mk`, `LatticeHom.coe_toInfHom`, `LowerSet.coe_iicInfHom`, `InfHom.symm_dual_id`, `InfHom.coe_id`, `Nucleus.mk_le_mk`, `InfHom.subtypeVal_coe`, `InfHom.coe_bot`, `InfHom.coe_inf`, `SupHom.dual_symm_apply_toFun`, `InfHom.mk_le_mk`, `InfHom.toFun_eq_coe`, `InfHom.coe_top`, `SupHom.dual_apply_toFun`, `InfHom.subtypeVal_apply`
`InfHomClass` 📖	CompData	5 math math: `OrderIsoClass.toInfHomClass`, `InfTopHomClass.toInfHomClass`, `InfHom.instInfHomClass`, `NucleusClass.toInfHomClass`, `LatticeHomClass.toInfHomClass`
`LatticeHom` 📖	CompData	98 math math: `LatticeHom.toFun_eq_coe`, `DistLat.hom_inv_apply`, `BoundedLatticeHom.coe_toLatticeHom`, `LatticeHom.withTopWithBot_apply`, `Lat.ext_iff`, `LatticeHom.fst_apply`, `LatticeHom.comp_apply`, `Sublattice.coe_map`, `LatticeHom.coe_withTopWithBot`, `Lat.dual_map`, `LatticeHom.coe_comp`, `DistLat.dual_map`, `Lat.coe_id`, `LatticeHom.subtypeVal_coe`, `LatticeHom.subtypeVal_apply`, `LatticeHom.id_apply`, `LatticeHom.dual_symm_apply_toFun`, `Lat.forget_map`, `Sublattice.inclusion_apply`, `BiheytingHom.toFun_eq_coe_aux`, `bddLat_dual_comp_forget_to_lat`, `exists_birkhoff_representation`, `LatticeHom.withTopWithBot'_toFun`, `Lat.comp_apply`, `CoheytingHom.toFun_eq_coe_aux`, `Sublattice.subtype_apply`, `DistLat.ext_iff`, `LatticeHom.dual_apply_toFun`, `LatticeHom.withTop_apply`, `LatticeHom.symm_dual_id`, `Pi.coe_evalLatticeHom`, `distLat_dual_comp_forget_to_Lat`, `Sublattice.apply_coe_mem_map`, `DistLat.forget_map`, `Sublattice.coe_comap`, `LatticeHom.withTop_toFun`, `Sublattice.mem_map`, `LatticeHom.withBot_toFun`, `LatticeHom.withTop'_toFun`, `DistLat.id_apply`, `FrameHom.coe_toLatticeHom`, `OrderHomClass.to_lattice_hom_apply`, `Sublattice.subtype_injective`, `LatticeHom.ext_iff`, `Sublattice.mem_subtype`, `LatticeHom.coe_withTop`, `LatticeHom.dual_id`, `LatticeHom.coe_mk`, `Lat.ofHom_apply`, `LatticeHom.coe_toSupHom`, `DistLat.ofHom_apply`, `LatticeHom.withTopWithBot_toFun`, `LatticeHom.symm_dual_comp`, `LatticeHom.coe_snd`, `HeytingHom.toFun_eq_coe_aux`, `Booleanisation.liftLatticeHom_injective`, `BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `BddLat.coe_forget_to_lat`, `BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat`, `LatticeHom.snd_apply`, `LatticeHom.withBot'_toFun`, `LatticeHom.coe_toInfHom`, `OrderHomClass.coe_to_lattice_hom`, `Sublattice.mem_map_of_mem`, `Lat_dual_comp_forget_to_partOrd`, `LatticeHom.coe_comp_inf_hom`, `LatticeHom.coe_comp_sup_hom`, `LatticeHom.dual_comp`, `Sublattice.coe_inclusion`, `LatticeHom.instLatticeHomClass`, `DistLat.coe_id`, `Lat.hom_inv_apply`, `BddLat.comp_apply`, `SimplexCategory.toCat_obj`, `LatticeHom.birkhoffFinset_injective`, `Lat.id_apply`, `BddLat.id_apply`, `DistLat.coe_comp`, `LatticeHom.coe_comp_inf_hom'`, `LatticeHom.coe_comp_sup_hom'`, `Lat.inv_hom_apply`, `LatticeHom.coe_withBot`, `bddDistLat_dual_comp_forget_to_distLat`, `DistLat.comp_apply`, `Function.locallyFinsuppWithin.restrictLatticeHom_apply`, `Sublattice.mem_comap`, `Sublattice.coe_subtype`, `BoundedLatticeHom.coe_mk`, `linOrd_dual_comp_forget_to_Lat`, `LatticeHom.coe_id`, `LatticeHom.coe_fst`, `SimplexCategory.toCat_map`, `DistLat.inv_hom_apply`, `Sublattice.inclusion_injective`, `CompleteSublattice.subtype_apply`, `Pi.evalLatticeHom_apply`, `LatticeHom.withBot_apply`, `Lat.coe_comp`
`LatticeHomClass` 📖	CompData	7 math math: `CoheytingHomClass.toLatticeHomClass`, `BiheytingHomClass.toLatticeHomClass`, `OrderIsoClass.toLatticeHomClass`, `OrderHomClass.toLatticeHomClass`, `BoundedLatticeHomClass.toLatticeHomClass`, `HeytingHomClass.toLatticeHomClass`, `LatticeHom.instLatticeHomClass`
`SupHom` 📖	CompData	41 math math: `SupHom.subtypeVal_coe`, `SupHom.bot_apply`, `InfHom.symm_dual_comp`, `SupHom.dual_id`, `SupHom.instSupHomClass`, `SupHom.coe_bot`, `SupHom.id_apply`, `SupHom.symm_dual_comp`, `InfHom.dual_apply_toFun`, `InfHom.dual_id`, `InfHom.dual_symm_apply_toFun`, `SupHom.coe_top`, `SupHom.dual_comp`, `UpperSet.coe_iciSupHom`, `InfHom.dual_comp`, `SupHom.coe_comp`, `SupHom.coe_const`, `SupHom.withTop'_toFun`, `SupHom.withTop_toFun`, `SupHom.symm_dual_id`, `LatticeHom.coe_mk`, `SupHom.subtypeVal_apply`, `LatticeHom.coe_toSupHom`, `SupBotHom.coe_toSupHom`, `SupHom.const_apply`, `SupHom.withBot_toFun`, `UpperSet.iciSupHom_apply`, `SupHom.withBot'_toFun`, `SupHom.sup_apply`, `SupHom.coe_sup`, `SupHom.comp_apply`, `SupHom.coe_mk`, `InfHom.symm_dual_id`, `SupHom.toFun_eq_coe`, `SupHom.ext_iff`, `SupHom.dual_symm_apply_toFun`, `SupHom.coe_id`, `SupHom.mk_le_mk`, `SupHom.top_apply`, `SupBotHom.coe_mk`, `SupHom.dual_apply_toFun`
`SupHomClass` 📖	CompData	4 math math: `OrderIsoClass.toSupHomClass`, `SupHom.instSupHomClass`, `SupBotHomClass.toSupHomClass`, `LatticeHomClass.toSupHomClass`
`instCoeTCInfHomOfInfHomClass` 📖	CompOp	—
`instCoeTCLatticeHomOfLatticeHomClass` 📖	CompOp	—
`instCoeTCSupHomOfSupHomClass` 📖	CompOp	—
`orderEmbeddingOfInjective` 📖	CompOp	2 math math: `orderEmbeddingOfInjective_apply`, `CompleteLatticeHom.toOrderIsoRangeOfInjective_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderEmbeddingOfInjective_apply` 📖	mathematical	`DFunLike.coe`	`RelEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `RelEmbedding.instFunLike` `orderEmbeddingOfInjective`	—	—

---

← Back to Index