English
Substitution substitutes free variables by terms inside a bounded formula, leaving bound variables untouched. The operation is defined by mapping terms inside the formula according to a specified transformation.
Русский
Подстановка заменяет свободные переменные термами в ограниченной формуле, оставляя связные переменные без изменений. Операция задаётся отображением внутри формулы по заданному преобразованию.
LaTeX
$$$\\text{subst}(\\varphi, f) = \\varphi.mapTermRel\\big(\\lambda\\_ t. t.\\mathrm{subst}(\\mathrm{Sum.elim}(\\mathrm{Term.relabel}(\\mathrm{Sum.inl}\\circ f)) (\\mathrm{var}\\circ \\mathrm{Sum.inr}))\\big)\\; (\\lambda\\_\\_.id)\\; (\\lambda\\_\\_.id)$$$
Lean4
/-- Substitutes the free variables in a bounded formula with terms, leaving bound variables
unchanged. -/
def subst {n : ℕ} (φ : L.BoundedFormula α n) (f : α → L.Term β) : L.BoundedFormula β n :=
φ.mapTermRel (fun _ t => t.subst (Sum.elim (Term.relabel Sum.inl ∘ f) (var ∘ Sum.inr))) (fun _ => id) fun _ => id
