const' — Mathlib

English

The family of constant maps Y → C(X,Y) forms a continuous map; i.e., the map const' is continuous.

Русский

Семейство константных отображений Y → C(X,Y) образует непрерывное отображение; константность отображения непрерывна.

LaTeX

$$$\text{const'} : C(Y, C(X,Y)) \to C(Y, C(X,Y))$ is continuous; equivalently, $\text{const'} = \text{curry}(\text{fst})$$$

Lean4

/-- The family of constant maps: `Y → C(X, Y)` as a continuous map. -/
def const' : C(Y, C(X, Y)) :=
  curry ContinuousMap.fst

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