Hom

📁 Source: Mathlib/Order/Prod/Lex/Hom.lean

Statistics

Metric	Count
Definitions toLexOrderHom	1
Theorems toLexOrderHom_coe	1
Total	2

Prod.Lex

Definitions

Name	Category	Theorems
toLexOrderHom 📖	CompOp	1 math math: toLexOrderHom_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLexOrderHom_coe 📖	mathematical	—	DFunLike.coe OrderHom Lex Prod.instPreorder PartialOrder.toPreorder instPreorder OrderHom.instFunLike toLexOrderHom Equiv EquivLike.toFunLike Equiv.instEquivLike toLex	—	—

---

← Back to Index