realize_iExs — Mathlib

English

For [Finite γ], (φ.iExsUnique γ).Realize v is equivalent to ∃! i : γ → M, φ.Realize (Sum.elim v i).

Русский

Для [ конечного γ ], (φ.iExsUnique γ).Realize v эквивалентно существованию единственного i : γ → M, такого что φ.Realize (Sum.elim v i).

LaTeX

$$$(\varphi.iExsUnique \gamma).Realize v \iff \ ExistsUnique \; i : \gamma \to M, \varphi.Realize (Sum.elim v i)$$$

Lean4

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

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