skolem₁_reduct_isElementary — Mathlib

English

The left projection of a Skolem-enhanced substructure is an elementary substructure.

Русский

Если S — подструктура языка со Skolem-ми, взятая внутри M, то редукция слева к языку L образует элементарную подструктуру M.

LaTeX

$$(LHom.sumInl.substructureReduct S).IsElementary$$

Lean4

theorem skolem₁_reduct_isElementary (S : (L.sum L.skolem₁).Substructure M) :
    (LHom.sumInl.substructureReduct S).IsElementary :=
  by
  apply (LHom.sumInl.substructureReduct S).isElementary_of_exists
  intro n φ x a h
  let φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ
  use ⟨funMap φ' ((↑) ∘ x), ?_⟩
  · exact Classical.epsilon_spec (p := fun a => BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)) ⟨a, h⟩
  · exact S.fun_mem (LHom.sumInr.onFunction φ) ((↑) ∘ x) (by exact fun i => (x i).2)

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