English
Composition of language maps respects the action on bounded formulas: applying φ after ψ to a bounded formula is the same as applying φ to the result of applying ψ on the formula.
Русский
Сложение отображений языков сохраняет действие на ограниченные формулы: (φ ∘ ψ).onBoundedFormula = φ.onBoundedFormula ∘ ψ.onBoundedFormula.
LaTeX
$$$((\\phi.comp \\psi).onBoundedFormula) = (\\phi.onBoundedFormula) \\circ (\\psi.onBoundedFormula).$$$
Lean4
@[simp]
theorem comp_onBoundedFormula {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
((φ.comp ψ).onBoundedFormula : L.BoundedFormula α n → L''.BoundedFormula α n) =
φ.onBoundedFormula ∘ ψ.onBoundedFormula :=
by
ext f
induction f with
| falsum => rfl
| equal => simp [Term.bdEqual]
| rel => simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]; rfl
| imp _ _ ih1 ih2 => simp only [onBoundedFormula, Function.comp_apply, ih1, ih2]
| all _ ih3 => simp only [ih3, onBoundedFormula, Function.comp_apply]
