funMap_sumInr — Mathlib

English

For L1,L2 languages and S a type, the funMap on the left injection satisfies (L1.sum L2).funMap (Sum.inl f) = funMap f.

Русский

Для языков L1, L2 и типа S отображение funMap слева от инъекции Sum.inl удовлетворяет равенству (L1.sum L2).funMap (Sum.inl f) = funMap f.

LaTeX

$$${(L_1.sum L_2).\mathrm{funMap}}(\mathrm{Sum.inl} f) = \mathrm{funMap} f$$$

Lean4

@[simp]
theorem funMap_sumInr {n : ℕ} (f : L₂.Functions n) : @funMap (L₁.sum L₂) S _ n (Sum.inr f) = funMap f :=
  rfl

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