Theorems · Definition · category theory
partialFunEquivPointed
PartialFun ≌ Pointed
The equivalence induced by PartialFunToPointed and PointedToPartialFun.
Part.equivOption made functorial.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functor.objproof · cited by 19,642
- CategoryTheory.Functor.compproof · cited by 6,529
- CategoryTheory.Functor.idproof · cited by 3,333
- CategoryTheory.Equivalencestatement · cited by 601
- CategoryTheory.NatIso.ofComponentsproof · cited by 178
- Pointedstatement and proof · cited by 56
- Pointed.pointproof · cited by 24
- Equiv.optionSubtypeNeproof · cited by 20
- PartialFunstatement and proof · cited by 18
- partialFunToPointedproof · cited by 8
- pointedToPartialFunproof · cited by 6
- PartialFun.Iso.mkproof · cited by 4
Cited by10
Results whose statement or proof uses this declaration.
- partialFunEquivPointed_counitIso_hom_app_toFunstatement and proof · cited by 0
- partialFunEquivPointed_counitIso_inv_app_toFunstatement and proof · cited by 0
- partialFunEquivPointed_functor_map_toFunstatement and proof · cited by 0
- partialFunEquivPointed_functor_obj_Xstatement and proof · cited by 0
- partialFunEquivPointed_functor_obj_pointstatement and proof · cited by 0
- partialFunEquivPointed_inverse_map_Domstatement and proof · cited by 0
- partialFunEquivPointed_inverse_map_get_coestatement and proof · cited by 0
- partialFunEquivPointed_inverse_objstatement and proof · cited by 0
- partialFunEquivPointed_unitIso_hom_appstatement and proof · cited by 0
- partialFunEquivPointed_unitIso_inv_appstatement and proof · cited by 0