nullhomotopic_of_constant

Mathlib.Topology.Homotopy.Contractible

URI: https://scilib.ai/kg/mathlib#ContinuousMap.nullhomotopic_of_constant

English

For every y in Y, the constant map X→Y at y is nullhomotopic.

Русский

Для каждого y в Y константное отображение X→Y в y является нулевой гомотопией.

LaTeX

$$$ \\forall y:\\,Y,\\ Nullhomotopic( ContinuousMap.const_X(y) )$$$

Lean4

theorem nullhomotopic_of_constant (y : Y) : Nullhomotopic (ContinuousMap.const X y) :=
  ⟨y, by rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru