paramsStructure

Mathlib.ModelTheory.LanguageMap

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

English

For any α and any subset A of α, the structure on α given by constantsOn A.Elem yields a valid structure.

Русский

Для любого α и подмножества A ⊆ α структура на α, заданная константами из A, является допустимой.

LaTeX

$$$ (constantsOn A.Elem).Structure α $$$

Lean4

instance paramsStructure (A : Set α) : (constantsOn A).Structure α :=
  constantsOn.structure (↑)

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

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

Разделы

Аффилиация

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