isPrenex_toPrenexImp — Mathlib

English

If φ is prenex and ψ is prenex, then φ.toPrenexImp ψ is prenex.

Русский

Если φ и ψ в пренексной форме, то φ.toPrenexImp ψ тоже пренексна.

LaTeX

$$$IsPrenex(\varphi.toPrenexImp \psi)$$$

Lean4

theorem isPrenex_toPrenexImp {φ ψ : L.BoundedFormula α n} (hφ : IsPrenex φ) (hψ : IsPrenex ψ) :
    IsPrenex (φ.toPrenexImp ψ) := by
  induction hφ with
  | of_isQF hφ => rw [hφ.toPrenexImp]; exact isPrenex_toPrenexImpRight hφ hψ
  | all _ ih1 => exact (ih1 hψ.liftAt).ex
  | ex _ ih2 => exact (ih2 hψ.liftAt).all

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