subst_comp_subst — Mathlib

English

For ha and hb substitutions, and any f, the composed substitution equals applying b after a: subst b (subst a f) = subst (subst b a) f.

Русский

Для подстановок ha, hb и любого f верно: подстановка b после подстановки a даёт ту же подстановку, что и подстановка ha.comp hb.

LaTeX

$$$\\operatorname{subst} b (\\operatorname{subst} a f) = \\operatorname{subst} (\\operatorname{subst} b a) f$$$

Lean4

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

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