continuous_aeval — Mathlib

English

Let a be a family a_s ∈ S indexed by σ satisfying HasEval a. Then the evaluation map aeval ha : MvPowerSeries σ R → S is continuous.

Русский

Пусть a — семейство элементов a_s ∈ S, индексируемое по σ, удовлетворяющее условию HasEval a. Тогда отображение эвалюации aeval ha: MvPowerSeries σ R → S непрерывно.

LaTeX

$$$ \operatorname{Continuous}(\mathrm{aeval}_{ha}) $$$

Lean4

theorem continuous_aeval (ha : HasEval a) : Continuous (aeval ha : MvPowerSeries σ R → S) :=
  by
  rw [coe_aeval]
  exact continuous_eval₂ (continuous_algebraMap R S) ha

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