Theorems · Theorem · category theory

PFunctor.M.iselect_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.iselect (⟨a, i⟩ :: ps) (PFunctor.M.mk ⟨a, f⟩) = PFunctor.M.iselect ps (f i)

Defined in

Mathlib.Data.PFunctor.Univariate.M

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqInhabited