English
Equivalences induced by a language equivalence commute with taking symmetries: the symmetry of the induced bounded formula equivalence equals the induced bounded formula of the symmetric equivalence.
Русский
Симметрия порожденной эквивалентности ограниченных формул совпадает с порожденной симметричной эквивалентностью.
LaTeX
$$$\\text{(φ.onBoundedFormula).symm} = φ.symm.onBoundedFormula$$$
Lean4
/-- Maps a bounded formula's symbols along a language equivalence. -/
@[simps]
def onBoundedFormula (φ : L ≃ᴸ L') : L.BoundedFormula α n ≃ L'.BoundedFormula α n
where
toFun := φ.toLHom.onBoundedFormula
invFun := φ.invLHom.onBoundedFormula
left_inv := by rw [Function.leftInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.left_inv, LHom.id_onBoundedFormula]
right_inv := by
rw [Function.rightInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.right_inv, LHom.id_onBoundedFormula]
