Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.relabel_all

∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ}
  (φ : L.BoundedFormula α (k + 1)),
  FirstOrder.Language.BoundedFormula.relabel g φ.all = (FirstOrder.Language.BoundedFormula.relabel g φ).all

Defined in

Mathlib.ModelTheory.Syntax

Cited by

2 results in Mathlib

Foundations

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