Hom

📁 Source: Mathlib/Topology/Algebra/SeparationQuotient/Hom.lean

Statistics

Metric	Count
Definitions liftContinuousAddMonoidHom, liftContinuousMonoidHom	2
Theorems liftContinuousAddCommMonoidHom_mk, liftContinuousCommMonoidHom_mk	2
Total	4

SeparationQuotient

Definitions

Name	Category	Theorems
liftContinuousAddMonoidHom 📖	CompOp	2 math math: liftContinuousAddCommMonoidHom_mk, liftNormedAddGroupHom_apply
liftContinuousMonoidHom 📖	CompOp	1 math math: liftContinuousCommMonoidHom_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftContinuousAddCommMonoidHom_mk 📖	mathematical	DFunLike.coe ContinuousAddMonoidHom AddCommMonoid.toAddMonoid ContinuousAddMonoidHom.instFunLike	DFunLike.coe ContinuousAddMonoidHom SeparationQuotient instAddMonoid AddCommMonoid.toAddMonoid instTopologicalSpaceSeparationQuotient ContinuousAddMonoidHom.instFunLike liftContinuousAddMonoidHom	—	—
liftContinuousCommMonoidHom_mk 📖	mathematical	DFunLike.coe ContinuousMonoidHom CommMonoid.toMonoid ContinuousMonoidHom.instFunLike	DFunLike.coe ContinuousMonoidHom SeparationQuotient instMonoid CommMonoid.toMonoid instTopologicalSpaceSeparationQuotient ContinuousMonoidHom.instFunLike liftContinuousMonoidHom	—	—

---

← Back to Index