Theorems · Definition · category theory
PFunctor.B
(self : PFunctor.{uA, uB}) → self.A → Type uBThe child family of types
- Defined in
- Mathlib.Data.PFunctor.Univariate.Basic
- Cited by
- 119 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PFunctor.Astatement · cited by 101
- PFunctorstatement and proof · cited by 75
Cited by216
Results whose statement or proof uses this declaration.
- PFunctor.Objproof · cited by 50
- PFunctor.Wproof · cited by 27
- PFunctor.mapproof · cited by 23
- PFunctor.M.destproof · cited by 22
- MvPFunctor.wMkstatement and proof · cited by 13
- PFunctor.Idxproof · cited by 11
- MvPFunctor.appendContentsstatement and proof · cited by 10
- PFunctor.map_eqstatement and proof · cited by 7
- MvPFunctor.wDest'proof · cited by 7
- MvPFunctor.wPathCasesOnstatement and proof · cited by 7
- PFunctor.Approx.head'proof · cited by 7
- PFunctor.M.casesOn'statement and proof · cited by 7
Showing the 200 most cited of 216.