Theorems · Definition · category theory
PFunctor.Approx.Path
PFunctor.{uA, uB} → Type (max uA uB)Path F provides indices to access internal nodes in Corec F
- Defined in
- Mathlib.Data.PFunctor.Univariate.M
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 4 from the axioms · 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.
- PFunctorstatement and proof · cited by 75
- PFunctor.Idxproof · cited by 11
Cited by18
Results whose statement or proof uses this declaration.
- PFunctor.M.iselectstatement and proof · cited by 7
- PFunctor.M.isubtreestatement and proof · cited by 6
- PFunctor.M.IsPathstatement · cited by 6
- PFunctor.M.IsPath.casesOnstatement and proof · cited by 2
- PFunctor.M.isubtree_consstatement and proof · cited by 2
- PFunctor.M.eq_of_bisimproof · cited by 1
- PFunctor.M.extstatement and proof · cited by 1
- PFunctor.M.ext_auxstatement and proof · cited by 1
- PFunctor.M.IsPath.belowstatement · cited by 1
- PFunctor.M.isPath_consstatement and proof · cited by 1
- PFunctor.M.isPath_cons'statement and proof · cited by 1
- PFunctor.M.iselect_consstatement and proof · cited by 1