English
Mapping commutes with objAppend1: applying g to the object on the left equals the object on the right with g applied everywhere and composed with f.
Русский
Отображение сохраняет разложение: отображение objAppend1 под действием g равно объекту на правой стороне с приложенным g повсеместно и композициями.
LaTeX
$$$\text{map_objAppend1}\ {\alpha}\ {\gamma}\ (g)\ (a)\ (f')\ (f) : \nobreakspace\n= \text{objAppend1 } a (g \circ f') (\lambda x. P.wMap g (f x)).$$$
Lean4
theorem map_objAppend1 {α γ : TypeVec n} (g : α ⟹ γ) (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α) :
appendFun g (P.wMap g) <$$> P.objAppend1 a f' f = P.objAppend1 a (g ⊚ f') fun x => P.wMap g (f x) := by
rw [objAppend1, objAppend1, map_eq, appendFun, ← splitFun_comp]; rfl
