funMap_sumInr

Mathlib.ModelTheory.LanguageMap

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.LHom.funMap_sumInr

← MathLib Explorer

English

Injectivity of LHom.sumInr.

Русский

Инъективность LHom.sumInr.

LaTeX

$$$(LHom.sumInr : L \to_L' L'.sum L').Injective$$$

Lean4

@[simp]
theorem funMap_sumInr [(L'.sum L).Structure M] [(LHom.sumInr : L →ᴸ L'.sum L).IsExpansionOn M] {n} {f : L.Functions n}
    {x : Fin n → M} : @funMap (L'.sum L) M _ n (Sum.inr f) x = funMap f x :=
  (LHom.sumInr : L →ᴸ L'.sum L).map_onFunction f x

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru