subst_comp_subst_apply — Mathlib

English

For ha, hb and f, the substituted f after applying b then a equals applying the composed substitution to f.

Русский

Для ha, hb и f заменённое f после применения b затем a равно применению композиции подстановок к f.

LaTeX

$$$\operatorname{subst}_b(\operatorname{subst}_a f) = \operatorname{subst}(\lambda s. \operatorname{subst}_b(a(s))) f$$$

Lean4

theorem subst_comp_subst_apply (ha : HasSubst a) (hb : HasSubst b) (f : MvPowerSeries σ R) :
    subst b (subst a f) = subst (fun s ↦ subst b (a s)) f :=
  congr_fun (subst_comp_subst (R := R) ha hb) f

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