model_empty

Mathlib.ModelTheory.Semantics

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

English

For a theory T, and a structure M, the realization of onTheory T is equivalent to the realization of T.

Русский

Для теории T и структуры M реализация onTheory T равна реализации самой теории.

LaTeX

$$$ M \models \phi.onTheory T \iff M \models T $$$

Lean4

instance model_empty : M ⊨ (∅ : L.Theory) :=
  ⟨fun φ hφ => (Set.notMem_empty φ hφ).elim⟩

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

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

Разделы

Аффилиация

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