isSatisfiable_onTheory_iff — Mathlib

English

For an injective language morphism φ, (φ.onTheory(T)) is satisfiable if and only if T is satisfiable.

Русский

Для инъективного гомоморфизма языков φ: (φ.onTheory(T)) удовлетворима тогда и только тогда T удовлетворима.

LaTeX

$$$φ: L \\to_L' L',\\ φ.Injective \\Rightarrow (φ.onTheory(T) IsSatisfiable) \\Leftrightarrow (T.IsSatisfiable)$$$

Lean4

theorem isSatisfiable_onTheory_iff {L' : Language.{w, w'}} {φ : L →ᴸ L'} (h : φ.Injective) :
    (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable := by
  classical
  refine ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => ?_⟩
  haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'
  exact Model.isSatisfiable (h'.some.defaultExpansion h)

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