comp_onTerm — Mathlib

English

Composition of language homomorphisms respects the underlying operation on terms, i.e., applying the composed homomorphism to a term is the same as applying each homomorphism in sequence to the term.

Русский

Композиция лингвистических гомоморфизмов сохраняет структуру терма: применение композиции к терму эквивалентно поочередному применению каждого гомоморфизма.

LaTeX

$$$((\\phi \\cdot \\psi).onTerm)(t) = (\\phi.onTerm) (\\psi.onTerm (t))$ for all terms t.$$

Lean4

@[simp]
theorem comp_onTerm {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
    ((φ.comp ψ).onTerm : L.Term α → L''.Term α) = φ.onTerm ∘ ψ.onTerm :=
  by
  ext t
  induction t with
  | var => rfl
  | func _ _ ih => simp_rw [onTerm, ih]; rfl

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