Theorems · Definition · logic and foundations

FirstOrder.Language.BoundedFormula.liftAt

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

Raises all of the bound variables of a formula greater than or equal to m by n'.

Defined in

Mathlib.ModelTheory.Syntax

Cited by

14 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Quot.sound