eval — Mathlib

English

The evaluation-at-x map is an algebra morphism from the algebra of smooth maps to the base field 𝕜, i.e., it preserves sums, products, and scalar actions.

Русский

Оценка в точке x является алгебра-морфизмом от алгебры гладких отображений к полю 𝕜, она сохраняет операции сложения, умножения и скалярное умножение.

LaTeX

$$$$ \operatorname{eval}_x: C^∞\langle I,M;\mathbb{K}\rangle\langle x\rangle \to \mathbb{K} \quad \text{is an algebra homomorphism}. $$$$

Lean4

/-- With the `evalAlgebra` algebra structure evaluation is actually an algebra morphism. -/
def eval (x : M) : C^∞⟮I, M; 𝕜⟯ →ₐ[C^∞⟮I, M; 𝕜⟯⟨x⟩] 𝕜 :=
  Algebra.ofId C^∞⟮I, M; 𝕜⟯⟨x⟩ 𝕜

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