English
For continuous φ and HasEval a, and any ε: S →+* T continuous, the composed evaluation equals eval₂ on the composed map.
Русский
Для непрерывного φ и HasEval a, и любого ε: S →+* T непрерывного, композиция оценки равна eval₂ на композицию.
LaTeX
$$$\epsilon \circ \text{eval}_2 φ a = \text{eval}_2 (\epsilon \circ φ) (\epsilon a)$$$
Lean4
theorem comp_eval₂ (hφ : Continuous φ) (ha : HasEval a) {T : Type*} [UniformSpace T] [CompleteSpace T] [T2Space T]
[CommRing T] [IsTopologicalRing T] [IsLinearTopology T T] [IsUniformAddGroup T] {ε : S →+* T} (hε : Continuous ε) :
ε ∘ eval₂ φ a = eval₂ (ε.comp φ) (ε a) :=
by
apply eval₂_unique _ (ha.map hε)
· exact Continuous.comp hε (continuous_eval₂ hφ ha)
· intro p
simp only [Function.comp_apply, eval₂_coe]
exact Polynomial.hom_eval₂ p φ ε a
· simp only [RingHom.coe_comp, Continuous.comp hε hφ]
