Nullhomotopic — Mathlib

English

A map is nullhomotopic if it is homotopic to a constant map.

Русский

Отображение нулевой гомотопии, если оно гомотопно к константному отображению.

LaTeX

$$$ Nullhomotopic(f) \\iff \\exists y:\\,Y,\\ Homotopic\ufeff(f,\\text{ContinuousMap.const } X y)$$$

Lean4

/-- A map is nullhomotopic if it is homotopic to a constant map. -/
def Nullhomotopic (f : C(X, Y)) : Prop :=
  ∃ y : Y, Homotopic f (ContinuousMap.const _ y)

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