map_constants_inclusion_isExpansionOn

Mathlib.ModelTheory.LanguageMap

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

English

The inclusion of constants map via lhomWithConstantsMap is an expansion on M.

Русский

Расширение константного отображения через lhomWithConstantsMap существует на M.

LaTeX

$$$ (L.lhomWithConstantsMap (Set.inclusion h)).IsExpansionOn M $$$

Lean4

instance map_constants_inclusion_isExpansionOn : (L.lhomWithConstantsMap (Set.inclusion h)).IsExpansionOn M :=
  LHom.sumMap_isExpansionOn _ _ _

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

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

Разделы

Аффилиация

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