coe_eval₂Hom — Mathlib

English

The underlying function of eval₂Hom equals eval₂ φ a.

Русский

Функция-основа eval₂Hom равна eval₂ φ a.

LaTeX

$$$\uparrow(\text{eval}_2\mathrm{Hom}(h_\phi, h_a)) = \text{eval}_2 φ a$$$

Lean4

theorem coe_eval₂Hom (hφ : Continuous φ) (ha : HasEval a) : ⇑(eval₂Hom hφ ha) = eval₂ φ a :=
  MvPowerSeries.coe_eval₂Hom hφ
    (hasEval ha)
      -- Note: this is still true without the `T2Space` hypothesis, by arguing that the case
      -- disjunction in the definition of `eval₂` only replaces some values by topologically
      -- inseparable ones.

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