toPrenexImpRight — Mathlib

English

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

Русский

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

LaTeX

$$$IsQF(\varphi) \rightarrow (\varphi.toPrenexImp ψ) = (\varphi.toPrenexImpRight ψ)$$$

Lean4

theorem toPrenexImpRight {φ : L.BoundedFormula α n} :
    ∀ {ψ : L.BoundedFormula α n}, IsQF ψ → φ.toPrenexImpRight ψ = φ.imp ψ
  | _, IsQF.falsum => rfl
  | _, IsQF.of_isAtomic (IsAtomic.equal _ _) => rfl
  | _, IsQF.of_isAtomic (IsAtomic.rel _ _) => rfl
  | _, IsQF.imp IsQF.falsum _ => rfl
  | _, IsQF.imp (IsQF.of_isAtomic (IsAtomic.equal _ _)) _ => rfl
  | _, IsQF.imp (IsQF.of_isAtomic (IsAtomic.rel _ _)) _ => rfl
  | _, IsQF.imp (IsQF.imp _ _) _ => rfl

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