relMap_sumInl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem relMap_sumInl {n : ℕ} (R : L₁.Relations n) : @RelMap (L₁.sum L₂) S _ n (Sum.inl R) = RelMap R :=
  rfl

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