Theorems · Theorem · logic and foundations

FirstOrder.Language.LEquiv.onBoundedFormula_symm_apply

∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L') (a : L'.BoundedFormula α n),
  φ.onBoundedFormula.symm a = φ.invLHom.onBoundedFormula a

Defined in

Mathlib.ModelTheory.Syntax

Cited by

0 results in Mathlib

Foundations

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