toPrenex — Mathlib

English

For any φ, φ.toPrenex is in prenex form.

Русский

Для любой φ формула toPrenex находится в пренексной форме.

LaTeX

$$$\forall \varphi\ (\varphi.toPrenex.IsPrenex)$$$

Lean4

/-- For any bounded formula `φ`, `φ.toPrenex` is a semantically-equivalent formula in prenex normal
  form. -/
def toPrenex : ∀ {n}, L.BoundedFormula α n → L.BoundedFormula α n
  | _, falsum => ⊥
  | _, equal t₁ t₂ => t₁.bdEqual t₂
  | _, rel R ts => rel R ts
  | _, imp f₁ f₂ => f₁.toPrenex.toPrenexImp f₂.toPrenex
  | _, all f => f.toPrenex.all

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