theory_model_iff

Mathlib.ModelTheory.ElementaryMaps

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

English

For any elementary embedding f and theory T, M models T iff N models T.

Русский

Для любого элементарного вложения f и теории T выполняется: модель M T эквивалентна модели N T.

LaTeX

$$$M \models T \\Leftrightarrow N \models T$ via f.map_sentence.$$

Lean4

theorem theory_model_iff (f : M ↪ₑ[L] N) (T : L.Theory) : M ⊨ T ↔ N ⊨ T := by
  simp only [Theory.model_iff, f.map_sentence]

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

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

Разделы

Аффилиация

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