realize_ex — Mathlib

English

For θ, the existential quantifier realized equals there exists an element a in M such that θ holds after appending a to the horizon.

Русский

Для θ реализация существования означает существование элемента a∈M, для которого θ истина после добавления a к горизонту переменных.

LaTeX

$$$ (\,\text{ex}\, \theta)^{\mathcal{M}}(v, xs) \iff \exists a \in M, \theta^{\mathcal{M}}(v, \mathrm{Fin.snoc}(xs, a)) $$$

Lean4

@[simp]
theorem realize_ex : θ.ex.Realize v xs ↔ ∃ a : M, θ.Realize v (Fin.snoc xs a) :=
  by
  rw [BoundedFormula.ex, realize_not, realize_all, not_forall]
  simp_rw [realize_not, Classical.not_not]

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