PUnit

📁 Source: Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.lean

Statistics

Metric	Count
Definitions punitEquivDiscretePUnit	1
Theorems instSubsingletonHomPUnit, punitEquivDiscretePUnit_counitIso, punitEquivDiscretePUnit_functor, punitEquivDiscretePUnit_inverse, punitEquivDiscretePUnit_unitIso, instSubsingletonPUnitUnit	6
Total	7

FundamentalGroupoid

Definitions

Name	Category	Theorems
punitEquivDiscretePUnit 📖	CompOp	4 math math: punitEquivDiscretePUnit_unitIso, punitEquivDiscretePUnit_counitIso, punitEquivDiscretePUnit_inverse, punitEquivDiscretePUnit_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSubsingletonHomPUnit 📖	mathematical	—	Quiver.Hom FundamentalGroupoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory instGroupoid instTopologicalSpacePUnit	—	Quotient.instSubsingletonQuotient Path.instSubsingletonPUnitUnit
punitEquivDiscretePUnit_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso FundamentalGroupoid CategoryTheory.Discrete CategoryTheory.Groupoid.toCategory instGroupoid instTopologicalSpacePUnit CategoryTheory.discreteCategory punitEquivDiscretePUnit CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Functor.star	—	—
punitEquivDiscretePUnit_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor FundamentalGroupoid CategoryTheory.Discrete CategoryTheory.Groupoid.toCategory instGroupoid instTopologicalSpacePUnit CategoryTheory.discreteCategory punitEquivDiscretePUnit CategoryTheory.Functor.star	—	—
punitEquivDiscretePUnit_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse FundamentalGroupoid CategoryTheory.Discrete CategoryTheory.Groupoid.toCategory instGroupoid instTopologicalSpacePUnit CategoryTheory.discreteCategory punitEquivDiscretePUnit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const	—	—
punitEquivDiscretePUnit_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso FundamentalGroupoid CategoryTheory.Discrete CategoryTheory.Groupoid.toCategory instGroupoid instTopologicalSpacePUnit CategoryTheory.discreteCategory punitEquivDiscretePUnit CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.star CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Iso.refl	—	—

Path

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSubsingletonPUnitUnit 📖	mathematical	—	Path instTopologicalSpacePUnit	—	ext

---

← Back to Index