Esakia

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

Statistics

Metric	Count
Definitions `EsakiaHom`, `comp`, `copy`, `id`, `instFunLike`, `instInhabited`, `toContinuousOrderHom`, `toPseudoEpimorphism`, `EsakiaHomClass`, `PseudoEpimorphism`, `comp`, `copy`, `id`, `instFunLike`, `instInhabited`, `toOrderHom`, `PseudoEpimorphismClass`, `instCoeTCEsakiaHomOfEsakiaHomClass`, `instCoeTCPseudoEpimorphismOfPseudoEpimorphismClass`	19
Theorems `cancel_left`, `cancel_right`, `coe_comp`, `coe_comp_continuousOrderHom`, `coe_comp_pseudoEpimorphism`, `coe_copy`, `coe_id`, `coe_id_continuousOrderHom`, `coe_id_pseudoEpimorphism`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `exists_map_eq_of_map_le'`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `instEsakiaHomClass`, `toContinuousOrderHom_coe`, `toFun_eq_coe`, `exists_map_eq_of_map_le`, `toContinuousOrderHomClass`, `toPseudoEpimorphismClass`, `toPseudoEpimorphismClass`, `cancel_left`, `cancel_right`, `coe_comp`, `coe_comp_orderHom`, `coe_copy`, `coe_id`, `coe_id_orderHom`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `exists_map_eq_of_map_le'`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `instPseudoEpimorphismClass`, `toFun_eq_coe`, `toOrderHom_eq_coe`, `exists_map_eq_of_map_le`, `toRelHomClass`, `toTopHomClass`	47
Total	66

EsakiaHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	9 math math: `id_comp`, `comp_id`, `comp_apply`, `coe_comp_continuousOrderHom`, `cancel_left`, `cancel_right`, `coe_comp_pseudoEpimorphism`, `coe_comp`, `comp_assoc`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`id` 📖	CompOp	6 math math: `id_comp`, `comp_id`, `coe_id`, `coe_id_continuousOrderHom`, `coe_id_pseudoEpimorphism`, `id_apply`
`instFunLike` 📖	CompOp	12 math math: `comp_apply`, `coe_comp_continuousOrderHom`, `coe_id`, `coe_comp_pseudoEpimorphism`, `coe_comp`, `coe_id_continuousOrderHom`, `instEsakiaHomClass`, `ext_iff`, `toContinuousOrderHom_coe`, `coe_id_pseudoEpimorphism`, `id_apply`, `toFun_eq_coe`
`instInhabited` 📖	CompOp	—
`toContinuousOrderHom` 📖	CompOp	2 math math: `toContinuousOrderHom_coe`, `toFun_eq_coe`
`toPseudoEpimorphism` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `EsakiaHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `EsakiaHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `EsakiaHom` `instFunLike` `comp`	—	—
`coe_comp_continuousOrderHom` 📖	mathematical	—	`ContinuousOrderHomClass.toContinuousOrderHom` `EsakiaHom` `instFunLike` `EsakiaHomClass.toContinuousOrderHomClass` `instEsakiaHomClass` `comp` `ContinuousOrderHom.comp`	—	`EsakiaHomClass.toContinuousOrderHomClass` `instEsakiaHomClass`
`coe_comp_pseudoEpimorphism` 📖	mathematical	—	`OrderHomClass.toOrderHom` `EsakiaHom` `instFunLike` `PseudoEpimorphismClass.toRelHomClass` `EsakiaHomClass.toPseudoEpimorphismClass` `instEsakiaHomClass` `comp` `PseudoEpimorphismClass.exists_map_eq_of_map_le` `PseudoEpimorphism.comp`	—	`PseudoEpimorphismClass.toRelHomClass` `EsakiaHomClass.toPseudoEpimorphismClass` `instEsakiaHomClass` `PseudoEpimorphismClass.exists_map_eq_of_map_le`
`coe_copy` 📖	mathematical	`DFunLike.coe` `EsakiaHom` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `EsakiaHom` `instFunLike` `id`	—	—
`coe_id_continuousOrderHom` 📖	mathematical	—	`ContinuousOrderHomClass.toContinuousOrderHom` `EsakiaHom` `instFunLike` `EsakiaHomClass.toContinuousOrderHomClass` `instEsakiaHomClass` `id` `ContinuousOrderHom.id`	—	`EsakiaHomClass.toContinuousOrderHomClass` `instEsakiaHomClass`
`coe_id_pseudoEpimorphism` 📖	mathematical	—	`OrderHomClass.toOrderHom` `EsakiaHom` `instFunLike` `PseudoEpimorphismClass.toRelHomClass` `EsakiaHomClass.toPseudoEpimorphismClass` `instEsakiaHomClass` `id` `PseudoEpimorphismClass.exists_map_eq_of_map_le` `PseudoEpimorphism.id`	—	`PseudoEpimorphismClass.toRelHomClass` `EsakiaHomClass.toPseudoEpimorphismClass` `instEsakiaHomClass` `PseudoEpimorphismClass.exists_map_eq_of_map_le`
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `EsakiaHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `EsakiaHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`exists_map_eq_of_map_le'` 📖	—	`Preorder.toLE` `OrderHom.toFun` `ContinuousOrderHom.toOrderHom` `toContinuousOrderHom`	—	—	—
`ext` 📖	—	`DFunLike.coe` `EsakiaHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `EsakiaHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `EsakiaHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instEsakiaHomClass` 📖	mathematical	—	`EsakiaHomClass` `EsakiaHom` `instFunLike`	—	`ContinuousOrderHom.continuous_toFun` `OrderHom.monotone'` `exists_map_eq_of_map_le'`
`toContinuousOrderHom_coe` 📖	mathematical	—	`DFunLike.coe` `ContinuousOrderHom` `ContinuousOrderHom.instFunLike` `toContinuousOrderHom` `EsakiaHom` `instFunLike`	—	—
`toFun_eq_coe` 📖	mathematical	—	`OrderHom.toFun` `ContinuousOrderHom.toOrderHom` `toContinuousOrderHom` `DFunLike.coe` `EsakiaHom` `instFunLike`	—	—

EsakiaHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_map_eq_of_map_le` 📖	—	`Preorder.toLE` `DFunLike.coe`	—	—	—
`toContinuousOrderHomClass` 📖	mathematical	—	`ContinuousOrderHomClass`	—	—
`toPseudoEpimorphismClass` 📖	mathematical	—	`PseudoEpimorphismClass`	—	`ContinuousOrderHomClass.map_monotone` `toContinuousOrderHomClass` `exists_map_eq_of_map_le`

OrderIsoClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPseudoEpimorphismClass` 📖	mathematical	—	`PseudoEpimorphismClass` `EquivLike.toFunLike`	—	`toOrderHomClass` `le_map_inv_iff` `EquivLike.right_inv`

PseudoEpimorphism

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	9 math math: `cancel_right`, `comp_id`, `id_comp`, `comp_apply`, `coe_comp`, `EsakiaHom.coe_comp_pseudoEpimorphism`, `comp_assoc`, `cancel_left`, `coe_comp_orderHom`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`id` 📖	CompOp	6 math math: `comp_id`, `coe_id`, `id_comp`, `EsakiaHom.coe_id_pseudoEpimorphism`, `id_apply`, `coe_id_orderHom`
`instFunLike` 📖	CompOp	10 math math: `coe_id`, `toFun_eq_coe`, `comp_apply`, `coe_comp`, `instPseudoEpimorphismClass`, `ext_iff`, `id_apply`, `toOrderHom_eq_coe`, `coe_id_orderHom`, `coe_comp_orderHom`
`instInhabited` 📖	CompOp	—
`toOrderHom` 📖	CompOp	2 math math: `toFun_eq_coe`, `toOrderHom_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_left` 📖	mathematical	`DFunLike.coe` `PseudoEpimorphism` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `PseudoEpimorphism` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `PseudoEpimorphism` `instFunLike` `comp`	—	—
`coe_comp_orderHom` 📖	mathematical	—	`OrderHomClass.toOrderHom` `PseudoEpimorphism` `instFunLike` `PseudoEpimorphismClass.toRelHomClass` `instPseudoEpimorphismClass` `comp` `OrderHom.comp`	—	`PseudoEpimorphismClass.toRelHomClass` `instPseudoEpimorphismClass`
`coe_copy` 📖	mathematical	`DFunLike.coe` `PseudoEpimorphism` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `PseudoEpimorphism` `instFunLike` `id`	—	—
`coe_id_orderHom` 📖	mathematical	—	`OrderHomClass.toOrderHom` `PseudoEpimorphism` `instFunLike` `PseudoEpimorphismClass.toRelHomClass` `instPseudoEpimorphismClass` `id` `OrderHom.id`	—	`PseudoEpimorphismClass.toRelHomClass` `instPseudoEpimorphismClass`
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `PseudoEpimorphism` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `PseudoEpimorphism` `instFunLike`	`copy`	—	`DFunLike.ext'`
`exists_map_eq_of_map_le'` 📖	—	`Preorder.toLE` `OrderHom.toFun` `toOrderHom`	—	—	—
`ext` 📖	—	`DFunLike.coe` `PseudoEpimorphism` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `PseudoEpimorphism` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `PseudoEpimorphism` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instPseudoEpimorphismClass` 📖	mathematical	—	`PseudoEpimorphismClass` `PseudoEpimorphism` `instFunLike`	—	`OrderHom.monotone'` `exists_map_eq_of_map_le'`
`toFun_eq_coe` 📖	mathematical	—	`OrderHom.toFun` `toOrderHom` `DFunLike.coe` `PseudoEpimorphism` `instFunLike`	—	—
`toOrderHom_eq_coe` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `toOrderHom` `PseudoEpimorphism` `instFunLike`	—	—

PseudoEpimorphismClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_map_eq_of_map_le` 📖	—	`Preorder.toLE` `DFunLike.coe`	—	—	—
`toRelHomClass` 📖	mathematical	—	`RelHomClass` `Preorder.toLE`	—	—
`toTopHomClass` 📖	mathematical	—	`TopHomClass` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder`	—	`exists_map_eq_of_map_le` `le_top` `top_le_iff`

(root)

Definitions

Name	Category	Theorems
`EsakiaHom` 📖	CompData	12 math math: `EsakiaHom.comp_apply`, `EsakiaHom.coe_comp_continuousOrderHom`, `EsakiaHom.coe_id`, `EsakiaHom.coe_comp_pseudoEpimorphism`, `EsakiaHom.coe_comp`, `EsakiaHom.coe_id_continuousOrderHom`, `EsakiaHom.instEsakiaHomClass`, `EsakiaHom.ext_iff`, `EsakiaHom.toContinuousOrderHom_coe`, `EsakiaHom.coe_id_pseudoEpimorphism`, `EsakiaHom.id_apply`, `EsakiaHom.toFun_eq_coe`
`EsakiaHomClass` 📖	CompData	1 math math: `EsakiaHom.instEsakiaHomClass`
`PseudoEpimorphism` 📖	CompData	10 math math: `PseudoEpimorphism.coe_id`, `PseudoEpimorphism.toFun_eq_coe`, `PseudoEpimorphism.comp_apply`, `PseudoEpimorphism.coe_comp`, `PseudoEpimorphism.instPseudoEpimorphismClass`, `PseudoEpimorphism.ext_iff`, `PseudoEpimorphism.id_apply`, `PseudoEpimorphism.toOrderHom_eq_coe`, `PseudoEpimorphism.coe_id_orderHom`, `PseudoEpimorphism.coe_comp_orderHom`
`PseudoEpimorphismClass` 📖	CompData	3 math math: `OrderIsoClass.toPseudoEpimorphismClass`, `EsakiaHomClass.toPseudoEpimorphismClass`, `PseudoEpimorphism.instPseudoEpimorphismClass`
`instCoeTCEsakiaHomOfEsakiaHomClass` 📖	CompOp	—
`instCoeTCPseudoEpimorphismOfPseudoEpimorphismClass` 📖	CompOp	—

---

← Back to Index