Theorems · Theorem · category theory

PFunctor.iget_map

∀ {P : PFunctor.{uA, uB}} {α : Type v₁} {β : Type v₂} [inst : DecidableEq P.A] [inst_1 : Inhabited α]
  [inst_2 : Inhabited β] (x : ↑P α) (f : α → β) (i : P.Idx), i.fst = x.fst → (P.map f x).iget i = f (x.iget i)

Defined in

Mathlib.Data.PFunctor.Univariate.Basic

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext

Assumes

DecidableEqInhabitedInhabited