withConstants_relMap_sumInl — Mathlib

English

In the constants-on language, interpreting Sum.inl R on x yields RelMap R x.

Русский

В языке с константами при интерпретации Sum.inl R на x получается RelMap R x.

LaTeX

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

Lean4

@[simp]
theorem withConstants_relMap_sumInl [L[[α]].Structure M] [(lhomWithConstants L α).IsExpansionOn M] {n}
    {R : L.Relations n} {x : Fin n → M} : @RelMap (L[[α]]) M _ n (Sum.inl R) x = RelMap R x :=
  (lhomWithConstants L α).map_onRelation R x

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