models_of_models_theory — Mathlib

English

If every φ ∈ T' is modeled by T, then any φ with T' ⊨ᵇ φ is also modeled by T.

Русский

Если каждый φ ∈ T' моделируется T, то любое φ с T' ⊨ᵇ φ смоделировано и T.

LaTeX

$$$\\forall φ, (φ ∈ T' \\Rightarrow T \\models^b φ) \; \\Rightarrow \\; (T' ⊨^b φ) \\Rightarrow (T ⊨^b φ)$$$

Lean4

theorem models_of_models_theory {T' : L.Theory} (h : ∀ φ : L.Sentence, φ ∈ T' → T ⊨ᵇ φ) {φ : L.Formula α}
    (hφ : T' ⊨ᵇ φ) : T ⊨ᵇ φ := fun M =>
  by
  have hM : M ⊨ T' := T'.model_iff.2 (fun ψ hψ => (h ψ hψ).realize_sentence M)
  let M' : ModelType T' := ⟨M⟩
  exact hφ M'

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