Documentation Verification Report

PartialFun

📁 Source: Mathlib/CategoryTheory/Category/PartialFun.lean

Statistics

Metric	Count
Definitions `PartialFun`, `mk`, `instCoeSortType`, `instInhabited`, `largeCategory`, `of`, `partialFunEquivPointed`, `partialFunToPointed`, `pointedToPartialFun`, `typeToPartialFun`, `typeToPartialFunIsoPartialFunToPointed`	11
Theorems `mk_hom`, `mk_inv`, `instFaithfulPartialFunTypeToPartialFun`, `partialFunEquivPointed_counitIso_hom_app_toFun`, `partialFunEquivPointed_counitIso_inv_app_toFun`, `partialFunEquivPointed_functor_map_toFun`, `partialFunEquivPointed_functor_obj_X`, `partialFunEquivPointed_functor_obj_point`, `partialFunEquivPointed_inverse_map_Dom`, `partialFunEquivPointed_inverse_map_get_coe`, `partialFunEquivPointed_inverse_obj`, `partialFunEquivPointed_unitIso_hom_app`, `partialFunEquivPointed_unitIso_inv_app`, `partialFunToPointed_map`, `partialFunToPointed_obj`, `pointedToPartialFun_map`, `pointedToPartialFun_obj`, `typeToPartialFunIsoPartialFunToPointed_hom_app_toFun`, `typeToPartialFunIsoPartialFunToPointed_inv_app_toFun`	19
Total	30

PartialFun

Definitions

Name	Category	Theorems
`instCoeSortType` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`largeCategory` 📖	CompOp	19 math math: `partialFunToPointed_map`, `typeToPartialFunIsoPartialFunToPointed_inv_app_toFun`, `partialFunEquivPointed_counitIso_inv_app_toFun`, `partialFunEquivPointed_unitIso_hom_app`, `pointedToPartialFun_map`, `partialFunEquivPointed_unitIso_inv_app`, `Iso.mk_inv`, `typeToPartialFunIsoPartialFunToPointed_hom_app_toFun`, `partialFunEquivPointed_functor_map_toFun`, `pointedToPartialFun_obj`, `instFaithfulPartialFunTypeToPartialFun`, `partialFunEquivPointed_inverse_obj`, `partialFunEquivPointed_functor_obj_X`, `partialFunToPointed_obj`, `partialFunEquivPointed_inverse_map_Dom`, `partialFunEquivPointed_counitIso_hom_app_toFun`, `partialFunEquivPointed_inverse_map_get_coe`, `partialFunEquivPointed_functor_obj_point`, `Iso.mk_hom`
`of` 📖	CompOp	—

PartialFun.Iso

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `PartialFun` `PartialFun.largeCategory` `Part.ofOption` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	—
`mk_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `PartialFun` `PartialFun.largeCategory` `Part.ofOption` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—

(root)

Definitions

Name	Category	Theorems
`PartialFun` 📖	CompOp	19 math math: `partialFunToPointed_map`, `typeToPartialFunIsoPartialFunToPointed_inv_app_toFun`, `partialFunEquivPointed_counitIso_inv_app_toFun`, `partialFunEquivPointed_unitIso_hom_app`, `pointedToPartialFun_map`, `partialFunEquivPointed_unitIso_inv_app`, `PartialFun.Iso.mk_inv`, `typeToPartialFunIsoPartialFunToPointed_hom_app_toFun`, `partialFunEquivPointed_functor_map_toFun`, `pointedToPartialFun_obj`, `instFaithfulPartialFunTypeToPartialFun`, `partialFunEquivPointed_inverse_obj`, `partialFunEquivPointed_functor_obj_X`, `partialFunToPointed_obj`, `partialFunEquivPointed_inverse_map_Dom`, `partialFunEquivPointed_counitIso_hom_app_toFun`, `partialFunEquivPointed_inverse_map_get_coe`, `partialFunEquivPointed_functor_obj_point`, `PartialFun.Iso.mk_hom`
`partialFunEquivPointed` 📖	CompOp	10 math math: `partialFunEquivPointed_counitIso_inv_app_toFun`, `partialFunEquivPointed_unitIso_hom_app`, `partialFunEquivPointed_unitIso_inv_app`, `partialFunEquivPointed_functor_map_toFun`, `partialFunEquivPointed_inverse_obj`, `partialFunEquivPointed_functor_obj_X`, `partialFunEquivPointed_inverse_map_Dom`, `partialFunEquivPointed_counitIso_hom_app_toFun`, `partialFunEquivPointed_inverse_map_get_coe`, `partialFunEquivPointed_functor_obj_point`
`partialFunToPointed` 📖	CompOp	8 math math: `partialFunToPointed_map`, `typeToPartialFunIsoPartialFunToPointed_inv_app_toFun`, `partialFunEquivPointed_counitIso_inv_app_toFun`, `partialFunEquivPointed_unitIso_hom_app`, `partialFunEquivPointed_unitIso_inv_app`, `typeToPartialFunIsoPartialFunToPointed_hom_app_toFun`, `partialFunToPointed_obj`, `partialFunEquivPointed_counitIso_hom_app_toFun`
`pointedToPartialFun` 📖	CompOp	6 math math: `partialFunEquivPointed_counitIso_inv_app_toFun`, `partialFunEquivPointed_unitIso_hom_app`, `pointedToPartialFun_map`, `partialFunEquivPointed_unitIso_inv_app`, `pointedToPartialFun_obj`, `partialFunEquivPointed_counitIso_hom_app_toFun`
`typeToPartialFun` 📖	CompOp	3 math math: `typeToPartialFunIsoPartialFunToPointed_inv_app_toFun`, `typeToPartialFunIsoPartialFunToPointed_hom_app_toFun`, `instFaithfulPartialFunTypeToPartialFun`
`typeToPartialFunIsoPartialFunToPointed` 📖	CompOp	2 math math: `typeToPartialFunIsoPartialFunToPointed_inv_app_toFun`, `typeToPartialFunIsoPartialFunToPointed_hom_app_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulPartialFunTypeToPartialFun` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.types` `PartialFun` `PartialFun.largeCategory` `typeToPartialFun`	—	`PFun.lift_injective`
`partialFunEquivPointed_counitIso_hom_app_toFun` 📖	mathematical	—	`Pointed.Hom.toFun` `CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `CategoryTheory.Functor.comp` `PartialFun` `PartialFun.largeCategory` `pointedToPartialFun` `partialFunToPointed` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `partialFunEquivPointed` `Option.casesOn'` `Pointed.X` `Pointed.point`	—	—
`partialFunEquivPointed_counitIso_inv_app_toFun` 📖	mathematical	—	`Pointed.Hom.toFun` `CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `PartialFun` `PartialFun.largeCategory` `pointedToPartialFun` `partialFunToPointed` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `partialFunEquivPointed` `Pointed.X` `Pointed.point`	—	—
`partialFunEquivPointed_functor_map_toFun` 📖	mathematical	—	`Pointed.Hom.toFun` `CategoryTheory.Functor.map` `PartialFun` `PartialFun.largeCategory` `Pointed` `Pointed.largeCategory` `CategoryTheory.Equivalence.functor` `partialFunEquivPointed` `Option.elim'` `Part.toOption` `Part.Dom`	—	—
`partialFunEquivPointed_functor_obj_X` 📖	mathematical	—	`Pointed.X` `CategoryTheory.Functor.obj` `PartialFun` `PartialFun.largeCategory` `Pointed` `Pointed.largeCategory` `CategoryTheory.Equivalence.functor` `partialFunEquivPointed`	—	—
`partialFunEquivPointed_functor_obj_point` 📖	mathematical	—	`Pointed.point` `CategoryTheory.Functor.obj` `PartialFun` `PartialFun.largeCategory` `Pointed` `Pointed.largeCategory` `CategoryTheory.Equivalence.functor` `partialFunEquivPointed`	—	—
`partialFunEquivPointed_inverse_map_Dom` 📖	mathematical	—	`Part.Dom` `Pointed.X` `Pointed.point` `CategoryTheory.Functor.map` `Pointed` `Pointed.largeCategory` `PartialFun` `PartialFun.largeCategory` `CategoryTheory.Equivalence.inverse` `partialFunEquivPointed` `Pointed.Hom.toFun`	—	—
`partialFunEquivPointed_inverse_map_get_coe` 📖	mathematical	—	`Pointed.X` `Pointed.point` `Part.get` `CategoryTheory.Functor.map` `Pointed` `Pointed.largeCategory` `PartialFun` `PartialFun.largeCategory` `CategoryTheory.Equivalence.inverse` `partialFunEquivPointed` `Pointed.Hom.toFun`	—	—
`partialFunEquivPointed_inverse_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `PartialFun` `PartialFun.largeCategory` `CategoryTheory.Equivalence.inverse` `partialFunEquivPointed` `Pointed.X` `Pointed.point`	—	—
`partialFunEquivPointed_unitIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `PartialFun` `PartialFun.largeCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `Pointed` `Pointed.largeCategory` `partialFunToPointed` `pointedToPartialFun` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `partialFunEquivPointed`	—	—
`partialFunEquivPointed_unitIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `PartialFun` `PartialFun.largeCategory` `CategoryTheory.Functor.comp` `Pointed` `Pointed.largeCategory` `partialFunToPointed` `pointedToPartialFun` `CategoryTheory.Functor.id` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `partialFunEquivPointed`	—	—
`partialFunToPointed_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `PartialFun` `PartialFun.largeCategory` `Pointed` `Pointed.largeCategory` `partialFunToPointed` `Option.elim'` `Pointed.X` `Part.toOption` `Part.Dom`	—	—
`partialFunToPointed_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `PartialFun` `PartialFun.largeCategory` `Pointed` `Pointed.largeCategory` `partialFunToPointed`	—	—
`pointedToPartialFun_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Pointed` `Pointed.largeCategory` `PartialFun` `PartialFun.largeCategory` `pointedToPartialFun` `Pointed.X` `Pointed.point` `Part` `PFun.toSubtype` `Pointed.Hom.toFun`	—	—
`pointedToPartialFun_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `PartialFun` `PartialFun.largeCategory` `pointedToPartialFun` `Pointed.X` `Pointed.point`	—	—
`typeToPartialFunIsoPartialFunToPointed_hom_app_toFun` 📖	mathematical	—	`Pointed.Hom.toFun` `CategoryTheory.Functor.obj` `CategoryTheory.types` `Pointed` `Pointed.largeCategory` `CategoryTheory.Functor.comp` `PartialFun` `PartialFun.largeCategory` `typeToPartialFun` `partialFunToPointed` `typeToPointed` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `typeToPartialFunIsoPartialFunToPointed`	—	—
`typeToPartialFunIsoPartialFunToPointed_inv_app_toFun` 📖	mathematical	—	`Pointed.Hom.toFun` `CategoryTheory.Functor.obj` `CategoryTheory.types` `Pointed` `Pointed.largeCategory` `typeToPointed` `CategoryTheory.Functor.comp` `PartialFun` `PartialFun.largeCategory` `typeToPartialFun` `partialFunToPointed` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `typeToPartialFunIsoPartialFunToPointed`	—	—

---

← Back to Index