English
Let a be a substitution and ε a continuous AlgHom; for any multivariate power series f, applying ε after substituting a into f is the same as evaluating f with the induced evaluation after transporting along the substitution ha.
Русский
Пусть a — подстановка и ε — непрерывное алгебро-однозначное отображение; для любой многоменной степенной серии f применение ε после подстановки a в f равно оценке f с использованием индуцированного отображения оценки, полученного из ha.
LaTeX
$$$\varepsilon(\operatorname{subst}_a f) = \operatorname{aeval}_{R}(\mathrm{ha.hasEval.map}(h\varepsilon)) f$$$
Lean4
theorem comp_subst_apply [UniformSpace R] [DiscreteUniformity R] [UniformSpace S] [DiscreteUniformity S]
(ha : HasSubst a) (hε : Continuous ε) (f : MvPowerSeries σ R) :
ε (subst a f) = aeval (R := R) (ha.hasEval.map hε) f :=
congr_fun (comp_subst ha hε) f
