Theorems · Theorem · category theory

PFunctor.M.isubtree_cons

∀ {F : PFunctor.{uA, uB}} [inst : DecidableEq F.A] [inst_1 : Inhabited F.M] (ps : PFunctor.Approx.Path F) {a : F.A}
  (f : F.B a → F.M) {i : F.B a},
  PFunctor.M.isubtree (⟨a, i⟩ :: ps) (PFunctor.M.mk ⟨a, f⟩) = PFunctor.M.isubtree ps (f i)

Defined in

Mathlib.Data.PFunctor.Univariate.M

Cited by

2 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqInhabited