Mathlib Map

Theorems · Definition · category theory

PFunctor.A

PFunctor.{uA, uB} → Type uA

The head type

Defined in
Mathlib.Data.PFunctor.Univariate.Basic
Cited by
101 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PFunctor.B · cited by 119PFunctor.BPFunctor.Obj · cited by 50PFunctor.ObjPFunctor.map · cited by 23PFunctor.mapPFunctor.Idx · cited by 11PFunctor.IdxPFunctor.M.head · cited by 10M.headPFunctor.map_eq · cited by 7PFunctor.map_eqMvPFunctor.wPathCasesOn · cited by 7MvPFunctor.wPathCasesOnPFunctor.Approx.head' · cited by 7Approx.head'PFunctor.M.casesOn' · cited by 7M.casesOn'PFunctor.M.iselect · cited by 7M.iselectPFunctor.W.dest · cited by 7W.destPFunctor.M.isubtree · cited by 6M.isubtreeQPF.IsUniform · cited by 5QPF.IsUniformPFunctor.W.mk · cited by 5W.mkQPF.liftp_iff · cited by 4QPF.liftp_iffPFunctor · cited by 75PFunctorPFunctor.ACITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • PFunctorstatement and proof · cited by 75

Cited by167

Results whose statement or proof uses this declaration.