realize_toPrenex — Mathlib

English

The realization for toPrenex coincides with the realization of the original formula.

Русский

Реализация формулы toPrenex совпадает с реализацией исходной формулы.

LaTeX

$$$\forall φ\;Realize(φ.toPrenex) = Realize(φ)$$$

Lean4

@[simp]
theorem realize_toPrenex (φ : L.BoundedFormula α n) {v : α → M} :
    ∀ {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs := by
  induction φ with
  | falsum => exact Iff.rfl
  | equal => exact Iff.rfl
  | rel => exact Iff.rfl
  | imp f1 f2 h1 h2 =>
    intros
    rw [toPrenex, realize_toPrenexImp f1.toPrenex_isPrenex f2.toPrenex_isPrenex, realize_imp, realize_imp, h1, h2]
  | all _ h =>
    intros
    rw [realize_all, toPrenex, realize_all]
    exact forall_congr' fun a => h

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