Documentation Verification Report

Hom

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

Statistics

Metric	Count
Definitions `iicInfHom`, `iicsInfHom`, `iciSupHom`, `icisSupHom`	4
Theorems `coe_iicInfHom`, `coe_iicsInfHom`, `iicInfHom_apply`, `iicsInfHom_apply`, `coe_iciSupHom`, `coe_icisSupHom`, `iciSupHom_apply`, `icisSupHom_apply`	8
Total	12

LowerSet

Definitions

Name	Category	Theorems
`iicInfHom` 📖	CompOp	2 math math: `iicInfHom_apply`, `coe_iicInfHom`
`iicsInfHom` 📖	CompOp	2 math math: `coe_iicsInfHom`, `iicsInfHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_iicInfHom` 📖	mathematical	—	`DFunLike.coe` `InfHom` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin` `instMin` `InfHom.instFunLike` `iicInfHom` `Iic`	—	—
`coe_iicsInfHom` 📖	mathematical	—	`DFunLike.coe` `sInfHom` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteSemilatticeInf.toInfSet` `instInfSet` `sInfHom.instFunLike` `iicsInfHom` `Iic`	—	—
`iicInfHom_apply` 📖	mathematical	—	`DFunLike.coe` `InfHom` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin` `instMin` `InfHom.instFunLike` `iicInfHom` `Iic`	—	—
`iicsInfHom_apply` 📖	mathematical	—	`DFunLike.coe` `sInfHom` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteSemilatticeInf.toInfSet` `instInfSet` `sInfHom.instFunLike` `iicsInfHom` `Iic`	—	—

UpperSet

Definitions

Name	Category	Theorems
`iciSupHom` 📖	CompOp	2 math math: `coe_iciSupHom`, `iciSupHom_apply`
`icisSupHom` 📖	CompOp	2 math math: `coe_icisSupHom`, `icisSupHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_iciSupHom` 📖	mathematical	—	`DFunLike.coe` `SupHom` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax` `instMax` `SupHom.instFunLike` `iciSupHom` `Ici`	—	—
`coe_icisSupHom` 📖	mathematical	—	`DFunLike.coe` `sSupHom` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instSupSet` `sSupHom.instFunLike` `icisSupHom` `Ici`	—	—
`iciSupHom_apply` 📖	mathematical	—	`DFunLike.coe` `SupHom` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax` `instMax` `SupHom.instFunLike` `iciSupHom` `Ici`	—	—
`icisSupHom_apply` 📖	mathematical	—	`DFunLike.coe` `sSupHom` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instSupSet` `sSupHom.instFunLike` `icisSupHom` `Ici`	—	—

---

← Back to Index