const

Mathlib.Topology.Homotopy.HomotopyGroup

URI: https://scilib.ai/kg/mathlib#GenLoop.const

English

The constant generalized loop at x assigns to every point of I^N the constant value x.

Русский

Постоянный обобщённый цикл в точке x отправляет каждую точку куба в x.

LaTeX

$$$\\text{GenLoop.const} : Ω^N X x \\text{ is the constant map } x$$$

Lean4

/-- The constant `GenLoop` at `x`. -/
def const : Ω^ N X x :=
  ⟨ContinuousMap.const _ x, fun _ _ => rfl⟩

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

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

Разделы

Аффилиация

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