ofIsEmpty_isExpansionOn

Mathlib.ModelTheory.LanguageMap

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

← MathLib Explorer

English

An instance LHom.ofIsEmpty L L' is expansion-on for any M.

Русский

Инстанс LHom.ofIsEmpty L L' является expansion-on для любой M.

LaTeX

$$$(LHom.ofIsEmpty L L').IsExpansionOn M$$$

Lean4

instance ofIsEmpty_isExpansionOn (M : Type*) [L.Structure M] [L'.Structure M] [L.IsAlgebraic] [L.IsRelational] :
    IsExpansionOn (LHom.ofIsEmpty L L') M where

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

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

Разделы

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

Аффилиация

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