realize_boundedFormula — Mathlib

English

If T ⊨ᵇ φ, then for any nonempty M that models T, and any v, xs, φ.Realize v xs.

Русский

Если T ⊨ᵇ φ, то для любой ненулевой модели M, удовлетворяющей T, и любых функций v и xs, φ реализуется.

LaTeX

$$$T \\models^b φ \\Rightarrow \\forall M \\; [M \\models T] \\; \\forall v, \\forall xs, φ.Realize v xs$$$

Lean4

theorem realize_boundedFormula {φ : L.BoundedFormula α n} (h : T ⊨ᵇ φ) (M : Type*) [L.Structure M] [M ⊨ T] [Nonempty M]
    {v : α → M} {xs : Fin n → M} : φ.Realize v xs :=
  by
  have h' : φ.toFormula.Realize (Sum.elim v xs) := (models_toFormula_iff.2 h).realize_formula M
  simp only [BoundedFormula.realize_toFormula, Sum.elim_comp_inl, Sum.elim_comp_inr] at h'
  exact h'

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