coeff_subst_finite — Mathlib

English

The set of coefficients involved in substitution is finite when σ is finite and the substitution is applicable.

Русский

Набор коэффициентов, затрагиваемых подстановкой, конечен, если σ конечно и подстановка применима.

LaTeX

$$$\\operatorname{Finite}\\bigl( \\{ d \\mapsto \\text{coeff}_{d} f \\cdot \\text{coeff}_{e}(d\\text{.prod}(a_s)^e) \\} \\bigr)$$$

Lean4

theorem coeff_subst_finite (ha : HasSubst a) (f : MvPowerSeries σ R) (e : τ →₀ ℕ) :
    Set.Finite (fun d ↦ coeff d f • (coeff e (d.prod fun s e => (a s) ^ e))).support :=
  letI : UniformSpace R := ⊥
  letI : UniformSpace S := ⊥
  Summable.finite_support_of_discreteTopology _
    ((hasSum_aeval ha.hasEval f).map (coeff e) (continuous_coeff S e)).summable

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