Submonoid

📁 Source: Mathlib/Algebra/Order/Hom/Submonoid.lean

Statistics

Metric	Count
Definitions topOrderMonoidIso	1
Theorems topOrderMonoidIso_apply, topOrderMonoidIso_symm_apply_coe	2
Total	3

Submonoid

Definitions

Name	Category	Theorems
topOrderMonoidIso 📖	CompOp	2 math math: topOrderMonoidIso_symm_apply_coe, topOrderMonoidIso_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topOrderMonoidIso_apply 📖	mathematical	—	DFunLike.coe OrderMonoidIso Submonoid Monoid.toMulOneClass SetLike.instMembership instSetLike Top.top instTop Subtype.preorder mul MulOne.toMul MulOneClass.toMulOne EquivLike.toFunLike OrderMonoidIso.instEquivLike topOrderMonoidIso	—	—
topOrderMonoidIso_symm_apply_coe 📖	mathematical	—	Submonoid Monoid.toMulOneClass SetLike.instMembership instSetLike Top.top instTop DFunLike.coe OrderMonoidIso Subtype.preorder MulOne.toMul MulOneClass.toMulOne mul EquivLike.toFunLike OrderMonoidIso.instEquivLike OrderMonoidIso.symm topOrderMonoidIso	—	—

---

← Back to Index