Documentation Verification Report

Basic

📁 Source: Mathlib/Topology/Order/Hom/Basic.lean

Statistics

Metric	Count
Definitions `ContinuousOrderHom`, `comp`, `copy`, `id`, `instFunLike`, `instInhabited`, `instPartialOrder`, `instPreorder`, `toContinuousMap`, `toOrderHom`, `ContinuousOrderHomClass`, `instCoeTCContinuousOrderHom`, `toContinuousOrderHom`, `«term_→Co_»`	14
Theorems `cancel_left`, `cancel_right`, `coe_comp`, `coe_copy`, `coe_id`, `coe_toOrderHom`, `comp_apply`, `comp_assoc`, `comp_id`, `continuous_toFun`, `copy_eq`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `instContinuousOrderHomClass`, `toFun_eq_coe`, `map_monotone`, `toContinuousMapClass`, `toOrderHomClass`	20
Total	34

ContinuousOrderHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	8 math math: `comp_assoc`, `coe_comp`, `EsakiaHom.coe_comp_continuousOrderHom`, `comp_apply`, `cancel_left`, `id_comp`, `cancel_right`, `comp_id`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`id` 📖	CompOp	5 math math: `id_apply`, `coe_id`, `EsakiaHom.coe_id_continuousOrderHom`, `id_comp`, `comp_id`
`instFunLike` 📖	CompOp	9 math math: `coe_comp`, `id_apply`, `coe_toOrderHom`, `comp_apply`, `coe_id`, `toFun_eq_coe`, `instContinuousOrderHomClass`, `EsakiaHom.toContinuousOrderHom_coe`, `ext_iff`
`instInhabited` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	—
`toContinuousMap` 📖	CompOp	—
`toOrderHom` 📖	CompOp	4 math math: `coe_toOrderHom`, `continuous_toFun`, `toFun_eq_coe`, `EsakiaHom.toFun_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `ContinuousOrderHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `ContinuousOrderHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `ContinuousOrderHom` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `ContinuousOrderHom` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `ContinuousOrderHom` `instFunLike` `id`	—	—
`coe_toOrderHom` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `toOrderHom` `ContinuousOrderHom` `instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousOrderHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`continuous_toFun` 📖	mathematical	—	`Continuous` `OrderHom.toFun` `toOrderHom`	—	—
`copy_eq` 📖	mathematical	`DFunLike.coe` `ContinuousOrderHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `ContinuousOrderHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousOrderHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousOrderHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instContinuousOrderHomClass` 📖	mathematical	—	`ContinuousOrderHomClass` `ContinuousOrderHom` `instFunLike`	—	`continuous_toFun` `OrderHom.monotone'`
`toFun_eq_coe` 📖	mathematical	—	`OrderHom.toFun` `toOrderHom` `DFunLike.coe` `ContinuousOrderHom` `instFunLike`	—	—

ContinuousOrderHomClass

Definitions

Name	Category	Theorems
`instCoeTCContinuousOrderHom` 📖	CompOp	—
`toContinuousOrderHom` 📖	CompOp	2 math math: `EsakiaHom.coe_comp_continuousOrderHom`, `EsakiaHom.coe_id_continuousOrderHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_monotone` 📖	mathematical	—	`Monotone` `DFunLike.coe`	—	—
`toContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass`	—	—
`toOrderHomClass` 📖	mathematical	—	`OrderHomClass` `Preorder.toLE`	—	`map_monotone`

(root)

Definitions

Name	Category	Theorems
`ContinuousOrderHom` 📖	CompData	9 math math: `ContinuousOrderHom.coe_comp`, `ContinuousOrderHom.id_apply`, `ContinuousOrderHom.coe_toOrderHom`, `ContinuousOrderHom.comp_apply`, `ContinuousOrderHom.coe_id`, `ContinuousOrderHom.toFun_eq_coe`, `ContinuousOrderHom.instContinuousOrderHomClass`, `EsakiaHom.toContinuousOrderHom_coe`, `ContinuousOrderHom.ext_iff`
`ContinuousOrderHomClass` 📖	CompData	2 math math: `ContinuousOrderHom.instContinuousOrderHomClass`, `EsakiaHomClass.toContinuousOrderHomClass`
`«term_→Co_»` 📖	CompOp	—

---

← Back to Index