continuous_const' — Mathlib

English

The map const' : Y → C(X,Y) is continuous; in particular, the family of constant maps varies continuously with the parameter y ∈ Y.

Русский

Отображение const' : Y → C(X,Y) непрерывно; константные отображения зависят непрерывно от параметра y ∈ Y.

LaTeX

$$$\text{continuous}(\text{const'})$$$

Lean4

theorem continuous_const' : Continuous (const X : Y → C(X, Y)) :=
  const'.continuous

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