realize_restrictFreeVar' — Mathlib

English

A variant of restrictFreeVar with a subset specified by a decision procedure; realization is preserved.

Русский

Вариант restrictFreeVar с подмножеством, заданным decidable, сохраняет реализацию.

LaTeX

$$$ [\DecidableEq α] \; (\phi.restrictFreeVar (Set.inclusion h)).Realize (v \circ (\uparrow)) xs \iff \phi.Realize v xs $$$

Lean4

/-- A special case of `realize_restrictFreeVar`, included because we can add the `simp` attribute
to it -/
@[simp]
theorem realize_restrictFreeVar' [DecidableEq α] {n : ℕ} {φ : L.BoundedFormula α n} {s : Set α}
    (h : ↑φ.freeVarFinset ⊆ s) {v : α → M} {xs : Fin n → M} :
    (φ.restrictFreeVar (Set.inclusion h)).Realize (v ∘ (↑)) xs ↔ φ.Realize v xs :=
  realize_restrictFreeVar _ (by simp)

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