model_singleton_iff

Mathlib.ModelTheory.Semantics

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

English

Model satisfaction of a singleton theory {φ} is equivalent to satisfying φ.

Русский

Удовлетворение единичной теории {φ} эквивалентно удовлетворению φ.

LaTeX

$$$ M \models \{\varphi\} \iff M \models \varphi $$$

Lean4

@[simp]
theorem model_singleton_iff {φ : L.Sentence} : M ⊨ ({ φ } : L.Theory) ↔ M ⊨ φ := by simp

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

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

Разделы

Аффилиация

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