coev — Mathlib

English

The coevaluation map sends a point y ∈ Y to the continuous map x ↦ (y, x) from X to Y×X.

Русский

Ковеирование отправляет точку y∈Y в непрерывное отображение x ↦ (y, x) из X в Y×X.

LaTeX

$$$\operatorname{coev}(b): X \to Y \times X,\; (\operatorname{coev}(b))(x) = (b,x)$$$

Lean4

/-- The coevaluation map `Y → C(X, Y × X)` sending a point `x : Y` to the continuous function
on `X` sending `y` to `(x, y)`. -/
@[simps -fullyApplied]
def coev (b : Y) : C(X, Y × X) :=
  { toFun := Prod.mk b }

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