iff_toPrenex — Mathlib

English

For any bounded formula φ, φ is equivalent to its prenex normal form φ.toPrenex with respect to the empty theory: φ ⇔[∅] φ.toPrenex.

Русский

Для любой ограниченной формулы φ, φ эквивалентна своему пренекс-экземпляру φ.toPrenex по пустой теории: φ ⇔[∅] φ.toPrenex.

LaTeX

$$$\forall \varphi:\ L.BoundedFormula\alpha\,n, \varphi \iff[∅] \varphi.toPrenex$$

Lean4

theorem iff_toPrenex (φ : L.BoundedFormula α n) : φ ⇔[∅] φ.toPrenex := fun M v xs => by
  rw [realize_iff, realize_toPrenex]

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