English
The underlying function of eval₂Hom equals the standard eval₂ φ a.
Русский
Функция, лежащая в основе eval₂Hom, совпадает с обычной eval₂ φ a.
LaTeX
$$$$\big(\operatorname{eval₂Hom}(h\phi,ha)\big)^{\uparrow} = \operatorname{eval₂}(\phi,a).$$$$
Lean4
theorem coe_eval₂Hom (hφ : Continuous φ) (ha : HasEval a) : ⇑(eval₂Hom hφ ha) = eval₂ φ a :=
by
ext f
simp only [eval₂Hom_eq_extend, eval₂]
split_ifs with h
· obtain ⟨p, rfl⟩ := h
simpa [MvPolynomial.coe_eval₂Hom] using
toMvPowerSeries_isDenseInducing.extend_eq (toMvPowerSeries_uniformContinuous hφ ha).continuous p
·
rw [← eval₂Hom_eq_extend hφ 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.
