realize_relabel — Mathlib

English

Relabeling the variables via g inside a bounded formula does not change its realization up to the appropriate postcomposition of the evaluation functions.

Русский

Переразметка переменных внутри ограниченной формулы не меняет реализацию формулы при подходящем преобразовании функций оценки.

LaTeX

$$$ (\phi.relabel g).Realize v xs \iff \phi.Realize (Sum.elim v (xs \circ Fin.castAdd n) \circ g) (xs \circ Fin.natAdd m) $$$

Lean4

@[simp]
theorem realize_relabel {m n : ℕ} {φ : L.BoundedFormula α n} {g : α → β ⊕ (Fin m)} {v : β → M} {xs : Fin (m + n) → M} :
    (φ.relabel g).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ Fin.castAdd n) ∘ g) (xs ∘ Fin.natAdd m) := by
  apply realize_mapTermRel_add_castLe <;> simp

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