Theorems · Definition · logic and foundations

FirstOrder.Language.BoundedFormula.subst

{L : FirstOrder.Language} →
  {α : Type u'} → {β : Type v'} → {n : ℕ} → L.BoundedFormula α n → (α → L.Term β) → L.BoundedFormula β n

Substitutes the free variables in a bounded formula with terms, leaving bound variables unchanged.

Defined in

Mathlib.ModelTheory.Syntax

Cited by

3 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms