realize_iExsUnique — Mathlib

English

For a bounded formula φ, φ.toFormula.Realize v corresponds to φ.Realize under the relabeled variables.

Русский

Для ограниченной формулы φ, реализование φ.toFormula.Realize v соответствует реализации φ при переназначении переменных.

LaTeX

$$$\varphi.toFormula.Realize v \iff \varphi.Realize (v \circ Sum.inl) (v \circ Sum.inr)$$$

Lean4

@[simp]
theorem realize_iExsUnique [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α → M} {v' : Fin 0 → M} :
    BoundedFormula.Realize (φ.iExsUnique γ) v v' ↔ ∃! (i : γ → M), φ.Realize (Sum.elim v i) := by
  rw [← Formula.realize_iExsUnique, iff_iff_eq]; congr; simp [eq_iff_true_of_subsingleton]

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