relMap_sumInr — Mathlib

English

In the disjoint sum of two languages, interpreting a relation coming from the second language via the right inclusion yields exactly the same relation as in the second language.

Русский

В дизъюнктивной сумме двух языков интерпретация отношения, взятого из второго языка через правую инъекцию, совпадает с интерпретацией этого отношения во втором языке.

LaTeX

$$$\operatorname{RelMap}_{L_1 \sqcup L_2}(\mathrm{Sum.inr}(R)) = \operatorname{RelMap}_{L_2}(R),$$$

Lean4

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

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