Pi

Statistics

Metric	Count
Definitions	0
Theorems `instDiscreteObjWhiskeringRightFunctorCategoryOfFiniteOfContainsIdentities`, `pi`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instDiscreteObjWhiskeringRightFunctorCategoryOfFiniteOfContainsIdentities` 📖	mathematical	—	`CategoryTheory.Functor.IsLocalization` `CategoryTheory.Functor` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.MorphismProperty.functorCategory`	—	`of_equivalences` `pi` `CategoryTheory.MorphismProperty.le_isoClosure` `CategoryTheory.Localization.inverts` `CategoryTheory.NatIso.isIso_of_isIso_app`
`pi` 📖	mathematical	`CategoryTheory.MorphismProperty.ContainsIdentities` `CategoryTheory.Functor.IsLocalization`	`CategoryTheory.pi` `CategoryTheory.Functor.pi` `CategoryTheory.MorphismProperty.pi`	—	`Finite.induction_empty_option` `of_equivalences` `Equiv.apply_symm_apply` `CategoryTheory.MorphismProperty.IsInvertedBy.pi` `CategoryTheory.Localization.inverts` `of_isEquivalence` `CategoryTheory.MorphismProperty.isomorphisms.iff` `CategoryTheory.isIso_pi_iff` `CategoryTheory.Equivalence.instIsEquivalenceForallPi` `prod` `CategoryTheory.MorphismProperty.Pi.containsIdentities`

---