onFormula — Mathlib

English

The composition of language maps on bounded formulas commutes with the onBoundedFormula operation.

Русский

Сочетание отображений языка на ограниченных формулах коммутирует с операцией onBoundedFormula.

LaTeX

$$$((\\varphi .comp \u0027 \\psi).onBoundedFormula) = (\\varphi.onBoundedFormula) \\circ (\\psi.onBoundedFormula)$$$

Lean4

/-- Maps a formula's symbols along a language equivalence. -/
def onFormula (φ : L ≃ᴸ L') : L.Formula α ≃ L'.Formula α :=
  φ.onBoundedFormula

Похожие утверждения