realize_embedding — Mathlib

English

For any bounded formula φ, φ.Realize v xs equals the Realize of its prenex form realized via the Sum-type realization; i.e., Eq ((θ.ex).Realize v xs) (Exists a, θ.Realize v (Snoc xs a)).

Русский

Для любой ограниченной формулы φ, реализация φ.Realize эквивалентна реализации её пренексной формы, реализованной через операцию Ex; эквивалентность достигается через Exists и snoc.

LaTeX

$$$\forall φ:\ L.BoundedFormula α n, Eq ((φ.toPrenex).Realize v xs) (Exists a, (φ.Realize v (Snoc xs a)))$$$

Lean4

theorem realize_embedding {φ : L.BoundedFormula α n} (hE : φ.IsExistential) (f : F) {v : α → M} {xs : Fin n → M} :
    φ.Realize v xs → φ.Realize (f ∘ v) (f ∘ xs) := by
  induction hE with
  | of_isQF hQF => simp [hQF.realize_embedding]
  | ex _ ih =>
    simp only [realize_ex, Nat.succ_eq_add_one]
    refine fun ⟨a, ha⟩ => ⟨f a, ?_⟩
    rw [← Fin.comp_snoc]
    exact ih ha

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