aeval_continuousMap_apply — Mathlib

English

Let g ∈ R[X], f ∈ C(α,R). Then for every x ∈ α, (aeval f) g evaluated at x equals g.eval(f(x)); i.e. the algebra homomorphism aeval acts pointwise on x.

Русский

Пусть g ∈ R[X], f ∈ C(α,R). Тогда для каждого x ∈ α верно: (aeval f) g (x) = g(f(x)).

LaTeX

$$$(\\mathrm{aeval}\, f)\, g\\; x = g( f(x) ),\\; \\forall x.$$$

Lean4

@[simp]
theorem aeval_continuousMap_apply (g : R[X]) (f : C(α, R)) (x : α) : ((Polynomial.aeval f) g) x = g.eval (f x) :=
  by
  refine Polynomial.induction_on' g ?_ ?_
  · intro p q hp hq
    simp [hp, hq]
  · intro n a
    simp

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