realize_formula — Mathlib

English

If φRealize relates to Sum.elim encoding, then φ.Realize v and φ.toFormula.Realize (Sum.elim v xs) correspond.

Русский

Если реализация формулы через кодировку Sum.elim соответствует реализации оригинальной формулы, тогда оба совпадают.

LaTeX

$$$\\forall φ, \\; (φ\\text{ Realize } v) \\iff (φ^{\\text{toFormula}}\\ Realize (\\operatorname{Sum.elim} v))$$$

Lean4

theorem realize_formula {φ : L.Formula α} (h : T ⊨ᵇ φ) (M : Type*) [L.Structure M] [M ⊨ T] [Nonempty M] {v : α → M} :
    φ.Realize v := by
  rw [models_formula_iff_onTheory_models_equivSentence] at h
  letI : (constantsOn α).Structure M := constantsOn.structure v
  have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance
  exact (Formula.realize_equivSentence _ _).1 (h.realize_sentence M)

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