mem_of_models — Mathlib

English

If a sentence φ is true in all models of T under the constants embedding, then φ ∈ p.

Русский

Если предложение φ истинно во всех моделях T при отображении констант, то φ ∈ p.

LaTeX

$$$(L.lhomWithConstants α).onTheory T \\\\models\\\\ᵇ φ \\\\Rightarrow φ \\in p$$$

Lean4

theorem mem_of_models (p : T.CompleteType α) {φ : L[[α]].Sentence} (h : (L.lhomWithConstants α).onTheory T ⊨ᵇ φ) :
    φ ∈ p :=
  (p.mem_or_not_mem φ).resolve_right fun con =>
    ((models_iff_not_satisfiable _).1 h) (p.isMaximal.1.mono (union_subset p.subset (singleton_subset_iff.2 con)))

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