toModel

Mathlib.ModelTheory.Bundled

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

Lean4

/-- A structure that is elementarily equivalent to a model, bundled as a model. -/
def toModel {M : T.ModelType} {N : Type*} [LN : L.Structure N] (h : M ≅[L] N) : T.ModelType
    where
  Carrier := N
  struc := LN
  nonempty' := h.nonempty
  is_model := h.theory_model

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

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

Разделы

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

Аффилиация

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