toPrenex_isPrenex — Mathlib

English

Every bounded formula, when transformed to prenex form, becomes prenex.

Русский

Любая ограниченная формула при преобразовании в пренексную форму становится пренексной.

LaTeX

$$$(\text{BoundedFormula}.toPrenex)(\varphi).IsPrenex$$$

Lean4

theorem toPrenex_isPrenex (φ : L.BoundedFormula α n) : φ.toPrenex.IsPrenex :=
  BoundedFormula.recOn φ isQF_bot.isPrenex (fun _ _ => (IsAtomic.equal _ _).isPrenex)
    (fun _ _ => (IsAtomic.rel _ _).isPrenex) (fun _ _ h1 h2 => isPrenex_toPrenexImp h1 h2) fun _ => IsPrenex.all

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