realize_relabel — Mathlib

English

Relabeling the bound variables of a formula by a map g yields a realization equal to realizing the original formula after precomposing the valuation with g.

Русский

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

LaTeX

$$$ (\phi^{\mathrm{relabel}\, g})^M(v) \iff \phi^M(v \circ g) $$$

Lean4

@[simp]
theorem realize_relabel {φ : L.Formula α} {g : α → β} {v : β → M} : (φ.relabel g).Realize v ↔ φ.Realize (v ∘ g) :=
  by
  rw [Realize, Realize, relabel, BoundedFormula.realize_relabel, iff_eq_eq, Fin.castAdd_zero]
  exact congr rfl (funext finZeroElim)

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