withConstants_funMap_sumInl — Mathlib

English

In the language with constants, interpreting Sum.inl f on x equals the original funMap f on x.

Русский

При интерпретации Sum.inl f в языке с константами отображение funMap совпадает с исходным funMap f на x.

LaTeX

$$$ (L[[\\alpha]]).funMap(\\mathrm{Sum.inl} f)\\, x = \\mathrm{funMap} f\\, x $$$

Lean4

@[simp]
theorem withConstants_funMap_sumInl [L[[α]].Structure M] [(lhomWithConstants L α).IsExpansionOn M] {n}
    {f : L.Functions n} {x : Fin n → M} : @funMap (L[[α]]) M _ n (Sum.inl f) x = funMap f x :=
  (lhomWithConstants L α).map_onFunction f x

Похожие утверждения