subst_comp_subst — Mathlib

English

Substituting by b after substituting by a equals substituting by the composed substitution.

Русский

Подстановка b после подстановки a равна подстановке по композиции подстановок.

LaTeX

$$$(\operatorname{subst} b) \circ (\operatorname{subst} a) = \operatorname{subst}(R := R)(\lambda s. \operatorname{subst} b (a(s)))$$$

Lean4

theorem subst_comp_subst (ha : HasSubst a) (hb : HasSubst b) :
    (subst b) ∘ (subst a) = subst (R := R) (fun s ↦ subst b (a s)) := by
  simpa [funext_iff, DFunLike.ext_iff] using substAlgHom_comp_substAlgHom (R := R) ha hb

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