continuous_coev — Mathlib

English

The coevaluation map is a continuous map Y → C(X, Y×X).

Русский

Ковеирование отображает Y в пространство непрерывных отображений X → Y×X непрерывно.

LaTeX

$$$\text{continuous}(\operatorname{coev}): Y \to C(X, Y\times X)$$$

Lean4

/-- The coevaluation map `Y → C(X, Y × X)` is continuous (always). -/
theorem continuous_coev : Continuous (coev X Y) :=
  ((continuous_prodMk_const (X := Y) (Y := X) (Z := X)).comp
      (.prodMk continuous_id (continuous_const (y := ContinuousMap.id _))) :)

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