Theorems · Definition · category theory
PFunctor.M.head
{F : PFunctor.{uA, uB}} → F.M → F.Agiven a tree generated by F, head gives us the first piece of data
it contains
- Defined in
- Mathlib.Data.PFunctor.Univariate.M
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- PFunctor.Mstatement and proof · cited by 52
- PFunctor.MIntl.approxproof · cited by 14
- PFunctor.Approx.head'proof · cited by 7
Cited by14
Results whose statement or proof uses this declaration.
- PFunctor.M.destproof · cited by 22
- PFunctor.M.iselectproof · cited by 7
- PFunctor.M.childrenstatement and proof · cited by 3
- PFunctor.M.bisimproof · cited by 2
- PFunctor.M.eq_of_bisimproof · cited by 1
- PFunctor.M.ichildrenproof · cited by 1
- PFunctor.M.iselect_consproof · cited by 1
- PFunctor.M.iselect_eq_defaultstatement and proof · cited by 1
- PFunctor.M.nth_of_bisimproof · cited by 1
- PFunctor.M.children_mkstatement and proof · cited by 0
- PFunctor.M.head'_eq_headstatement and proof · cited by 0
- PFunctor.M.head_eq_head'statement and proof · cited by 0