realize_exs — Mathlib

English

For a bounded formula φ with n free variables, φ.exs.Realize v holds exactly when there exists a witness xs : Fin n → M with φ.Realize v xs.

Русский

Для ограниченной формулы φ с n свободными переменными, φ.exs.Realize v истинно тогда, когда существует свидетель xs : Fin n → M, такой что φ.Realize v xs.

LaTeX

$$$\varphi.exs.Realize v \iff \exists xs : \mathrm{Fin}~n \to M, \varphi.Realize v xs$$$

Lean4

@[simp]
theorem realize_exs {φ : L.BoundedFormula α n} {v : α → M} : φ.exs.Realize v ↔ ∃ xs : Fin n → M, φ.Realize v xs := by
  induction n with
  | zero => exact Unique.exists_iff.symm
  | succ n ih =>
    simp only [BoundedFormula.exs, ih, realize_ex]
    constructor
    · rintro ⟨xs, x, h⟩
      exact ⟨_, h⟩
    · rintro ⟨xs, h⟩
      rw [← Fin.snoc_init_self xs] at h
      exact ⟨_, _, h⟩

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