evalMonoidHom — Mathlib

English

Evaluation at a point x induces a MonoidHom from LocallyConstant X Y to Y, given by f ↦ f(x).

Русский

Оценка в точке x задаёт моноид-гомоморфизм из LocallyConstant(X,Y) в Y, отображающий f ↦ f(x).

LaTeX

$$$\operatorname{evalMonoidHom} : X \to \operatorname{MonoidHom}(\operatorname{LocallyConstant}(X,Y), Y)$$$

Lean4

/-- Evaluation as a `MonoidHom` -/
@[to_additive (attr := simps!) /-- Evaluation as an `AddMonoidHom` -/
    ]
def evalMonoidHom [MulOneClass Y] (x : X) : LocallyConstant X Y →* Y :=
  (Pi.evalMonoidHom _ x).comp coeFnMonoidHom

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