Theorems · Theorem · category theory
PFunctor.M.isPath_cons
∀ {F : PFunctor.{uA, uB}} {xs : PFunctor.Approx.Path F} {a a' : F.A} {f : F.B a → F.M} {i : F.B a'},
PFunctor.M.IsPath (⟨a', i⟩ :: xs) (PFunctor.M.mk ⟨a, f⟩) → a = a'- Defined in
- Mathlib.Data.PFunctor.Univariate.M
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PFunctor.Bstatement and proof · cited by 119
- PFunctor.Astatement and proof · cited by 101
- PFunctorstatement and proof · cited by 75
- PFunctor.Mstatement and proof · cited by 52
- PFunctor.M.mkstatement and proof · cited by 27
- PFunctor.Approx.Pathstatement and proof · cited by 11
- PFunctor.Idxstatement · cited by 11
- PFunctor.M.IsPathstatement and proof · cited by 6
- PFunctor.M.mk_injproof · cited by 4
- PFunctor.M.IsPath.casesOnproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- PFunctor.M.nth_of_bisimproof · cited by 1