continuous_subst — Mathlib

English

The composition with an algebra morphism commutes with substitution: ε ∘ (substAlgHom ha) = aeval (ha.hasEval.map hε).

Русский

Сведение композиции с алгебра-морфизмом коммутирует с подстановкой: ε ∘ (substAlgHom ha) = aeval (ha.hasEval.map hε).

LaTeX

$$$\\varepsilon \\circ (\\operatorname{substAlgHom}(ha)) = \\operatorname{MvPowerSeries.aeval}(ha.hasEval.map\\ h\\varepsilon)$$$

Lean4

theorem continuous_subst (ha : HasSubst a) [UniformSpace R] [DiscreteUniformity R] [UniformSpace S]
    [DiscreteUniformity S] : Continuous (subst a : MvPowerSeries σ R → MvPowerSeries τ S) :=
  by
  rw [subst_eq_eval₂]
  exact continuous_eval₂ (continuous_algebraMap _ _) ha.hasEval

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