English
If ha and hb are substitutions, then composing them yields a substitution with the composed rule.
Русский
Если существуют подстановки ha и hb, то композиция даёт подстановку с правилом ha.comp hb.
LaTeX
$$$\\text{ha : HasSubst } a \\ \\,\\text{and}\\ \\,\\text{hb : HasSubst } b \\Rightarrow \\text{HasSubst } (fun s \\mapsto \\operatorname{substAlgHom } hb (a\,s)).$$$
Lean4
theorem comp (ha : HasSubst a) (hb : HasSubst b) : HasSubst (fun s ↦ substAlgHom hb (a s))
where
const_coeff s := IsNilpotent_subst hb (ha.const_coeff s)
coeff_zero := by
letI : UniformSpace S := ⊥
letI : UniformSpace T := ⊥
rw [← coeff_zero_iff]
apply Filter.Tendsto.comp _ (ha.hasEval.tendsto_zero)
simpa [← map_zero (substAlgHom (R := S) hb)] using (continuous_subst hb).continuousAt
