models_toFormula_iff — Mathlib

English

A formula φ is realized in T iff its toFormula version is realized in T.

Русский

Формула φ реализуется в T тогда и только тогда, когда её версия toFormula реализуется в T.

LaTeX

$$$T \\models^b φ.toFormula \\iff T \\models^b φ$$$

Lean4

theorem models_toFormula_iff {φ : L.BoundedFormula α n} : T ⊨ᵇ φ.toFormula ↔ T ⊨ᵇ φ :=
  by
  refine ⟨fun h M v xs => ?_, ?_⟩
  · have h' : φ.toFormula.Realize (Sum.elim v xs) := h.realize_formula M
    simp only [BoundedFormula.realize_toFormula, Sum.elim_comp_inl, Sum.elim_comp_inr] at h'
    exact h'
  · simp only [models_formula_iff, BoundedFormula.realize_toFormula]
    exact fun h M v => h M _ _

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