sumInr_injective

Mathlib.ModelTheory.LanguageMap

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

English

If ϕ is injective, then its defaultExpansion is expansion-on for any M.

Русский

Если ϕ инъективна, то её defaultExpansion является expansion-on для любой M.

LaTeX

$$$\varphi.Injective \rightarrow \text{IsExpansionOn } \varphi.\text{defaultExpansion } M$$$

Lean4

theorem sumInr_injective : (LHom.sumInr : L' →ᴸ L.sum L').Injective :=
  ⟨fun h => Sum.inr_injective h, fun h => Sum.inr_injective h⟩

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

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

Разделы

Аффилиация

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