onTheory_model — Mathlib

English

If M ⊨ T, then T is contained in the complete theory of M, i.e., every sentence in T is realized in M.

Русский

Если M моделирует T, тогда T ⊆ полнотеории M, то есть каждое предложение из T реализуется в M.

LaTeX

$$$ M \models T \Rightarrow T \subseteq \mathrm{Th}_{M} $$$

Lean4

@[simp]
theorem onTheory_model [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (T : L.Theory) : M ⊨ φ.onTheory T ↔ M ⊨ T :=
  by simp [Theory.model_iff, LHom.onTheory]

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