toPrenexImpRight — Mathlib

English

If ψ is quantifier-free, then φ.toPrenexImpRight ψ equals φ.imp ψ.

Русский

Если ψ квантитно-фри, то φ.toPrenexImpRight ψ равно φ.imp ψ.

LaTeX

$$$\forall φ \forall ψ\ (IsQF(ψ) \rightarrow (φ.toPrenexImpRight ψ)= (φ\.imp ψ))$$$

Lean4

/-- An auxiliary operation to `FirstOrder.Language.BoundedFormula.toPrenex`.
  If `φ` is quantifier-free and `ψ` is in prenex normal form, then `φ.toPrenexImpRight ψ`
  is a prenex normal form for `φ.imp ψ`. -/
def toPrenexImpRight : ∀ {n}, L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n
  | n, φ, BoundedFormula.ex ψ => ((φ.liftAt 1 n).toPrenexImpRight ψ).ex
  | n, φ, all ψ => ((φ.liftAt 1 n).toPrenexImpRight ψ).all
  | _n, φ, ψ => φ.imp ψ

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