subst_eq_eval₂ — Mathlib

English

Under the given uniform structures, substitution coincides with evaluation: subst = eval₂(algebraMap).

Русский

При заданной униформной структуре подстановка совпадает с вычислением: subst = eval₂(algebraMap).

LaTeX

$$$[\\ UniformSpace R\\] [\\ DiscreteUniformity R] [\\ UniformSpace S] [\\ DiscreteUniformity S] \\Rightarrow (\\operatorname{subst} = \\operatorname{eval}_2(\\operatorname{algebraMap} R S)).$$$

Lean4

theorem subst_eq_eval₂ [UniformSpace R] [DiscreteUniformity R] [UniformSpace S] [DiscreteUniformity S] :
    (subst : (σ → MvPowerSeries τ S) → (MvPowerSeries σ R) → _) = eval₂ (algebraMap _ _) := by ext;
  simp [subst, DiscreteUniformity.eq_bot]

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